diff options
Diffstat (limited to 'Test/dafny3/WideTrees.dfy')
| -rw-r--r-- | Test/dafny3/WideTrees.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy index e381726e..3fa99256 100644 --- a/Test/dafny3/WideTrees.dfy +++ b/Test/dafny3/WideTrees.dfy @@ -36,12 +36,12 @@ function SmallTrees(n: nat): Stream<Tree> if n == 0 then SNil else SCons(SmallTree(n-1), SmallTrees(n))
}
// prove that the tree returned by SmallTree is finite
-ghost method Theorem(n: nat)
+lemma Theorem(n: nat)
ensures HasBoundedHeight(SmallTree(n));
{
Lemma(n);
}
-comethod Lemma(n: nat)
+colemma Lemma(n: nat)
ensures LowerThan(SmallTrees(n), n);
{
if 0 < n {
|