From 0c77817fae2b4743820c47634dfbe8fd9036a533 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 22 Mar 2013 10:30:27 -0700
Subject: Updated two test files.

---
 Test/dafny1/Rippling.dfy | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 835c3043..4aaa9a38 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -204,7 +204,7 @@ function insort(n: Nat, xs: List): List
   case Cons(y, ys) =>
     if leq(n, y) == True
     then Cons(n, Cons(y, ys))
-    else Cons(y, ins(n, ys))
+    else Cons(y, insort(n, ys))
 }
 
 function ins(n: Nat, xs: List): List
@@ -397,11 +397,8 @@ ghost method P19()
 ghost method P20()
   ensures forall xs :: len(sort(xs)) == len(xs);
 {
-  P15();  // use the statement of problem 15 as a lemma
-  // ... and manually introduce a case distinction:
-  assert forall ys ::
-           sort(ys) == Nil ||
-           exists z, zs :: sort(ys) == Cons(z, zs);
+  // the proof of this theorem requires a lemma about "insort"
+  assert forall x, xs :: len(insort(x, xs)) == Suc(len(xs));
 }
 
 ghost method P21()
-- 
cgit v1.2.3