Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to a previous lemma

1 files changed, 2 insertions, 3 deletions

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);