diff options
Diffstat (limited to 'Test/dafny1/Induction.dfy')
-rw-r--r-- | Test/dafny1/Induction.dfy | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 0e4c58e0..2c90769b 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -24,8 +24,8 @@ class IntegerInduction { ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
- call Theorem0(n-1);
- call Lemma(n-1);
+ Theorem0(n-1);
+ Lemma(n-1);
}
}
@@ -33,7 +33,7 @@ class IntegerInduction { requires 0 <= n;
ensures 2 * Gauss(n) == n*(n+1);
{
- if (n != 0) { call Lemma(n-1); }
+ if (n != 0) { Lemma(n-1); }
}
// Here is another proof. It states the lemma as part of the theorem, and
@@ -45,7 +45,7 @@ class IntegerInduction { ensures 2 * Gauss(n) == n*(n+1);
{
if (n != 0) {
- call Theorem1(n-1);
+ Theorem1(n-1);
}
}
@@ -64,7 +64,7 @@ class IntegerInduction { ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
- call Theorem2(n-1);
+ Theorem2(n-1);
assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
}
@@ -84,7 +84,7 @@ class IntegerInduction { ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
{
if (n != 0) {
- call Theorem3(n-1);
+ Theorem3(n-1);
}
}
@@ -112,7 +112,7 @@ class IntegerInduction { if (*) {
assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
} else {
- call Theorem4();
+ Theorem4();
}
}
|