The general method in Dafny for proving something by contradiction is:
lemma X()
ensures Q(x)
{
if !Q(x)
{
// derive contradiction
assert false;
}
} |
The general method in Dafny for proving something by contradiction is:
lemma X()
ensures Q(x)
{
if !Q(x)
{
// derive contradiction
assert false;
}
} |