1 files changed, 19 insertions, 1 deletions
diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index 4205035d..60506a33 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
@@ -92,6 +92,21 @@ class DoublyLinkedList {
     }
     Nodes := nodes;
   }
+
+  function PopMiddle<T>(s: seq<T>, k: nat) : seq<T>
+    requires k < |s| {
+      s[..k] + s[k+1..]
+  }
+
+  predicate Injective<T>(s: seq<T>) {
+    forall j, k :: 0 <= j < k < |s| ==> s[j] != s[k]
+  }
+
+  lemma InjectiveAfterPop<T>(s: seq<T>, k: nat)
+    requires k < |s|
+    requires Injective(s)
+    ensures  Injective(PopMiddle(s, k)) { }
+
   method Remove(x: Node) returns (ghost k: int)
     requires Valid()
     requires x in Nodes && x != Nodes[0] && x != Nodes[|Nodes|-1]  // not allowed to remove end nodes; you may think of them as a sentinel nodes
@@ -103,8 +118,11 @@ class DoublyLinkedList {
     k :| 1 <= k < |Nodes|-1 && Nodes[k] == x;
     x.R.L := x.L;
     x.L.R := x.R;
+
+    InjectiveAfterPop(Nodes, k);
     Nodes := Nodes[..k] + Nodes[k+1..];
   }
+
   // One might consider have a precondition that says there exists a "k" with the properties given here.
   // However, we want to be able to refer to "k" in the postcondition as well, so it's convenient to
   // burden the client with having to pass in "k" as a ghost parameter.  This, however, is really no