From 34bd565010ed0608c8f4e870df297deadf4544c5 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 4 Nov 2011 16:00:43 -0700
Subject: Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a
 call to a previous lemma

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

(limited to 'Test')

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 4a1c4bbe..c9a9f3b7 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -397,9 +397,8 @@ ghost method P19()
 ghost method P20()
   ensures forall xs :: len(sort(xs)) == len(xs);
 {
-  // proving this theorem requires an additional lemma:
-  assert forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks));
-  // ...and one manually introduced case study:
+  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);
-- 
cgit v1.2.3