diff --git a/dafny/submission.dfy b/dafny/submission.dfy
index 31bc50c..ee6bfe6 100644
--- a/dafny/submission.dfy
+++ b/dafny/submission.dfy
@@ -93,32 +93,36 @@ method binarysearch_iter(A:array<int>, v:int) returns (result:bool)
 method partition(A:array<int>, lo:int, hi:int) returns (pivot:int)
   requires 0 <= lo < hi <= A.Length;
   ensures 0 <= lo <= pivot < hi <= A.Length;
+  requires hi < A.Length ==> forall k :: lo <= k < hi ==> A[k] < A[hi];
+  ensures  hi < A.Length ==> forall k :: lo <= k < hi ==> A[k] < A[hi];
+  requires 0 < lo ==> forall k :: lo <= k < hi ==> A[lo-1] <= A[k];
+  ensures  0 < lo ==> forall k :: lo <= k < hi ==> A[lo-1] <= A[k];
   ensures forall k :: (0 <= k < lo || hi <= k < A.Length) ==> old(A[k]) == A[k];
-  ensures forall k :: lo <= k < pivot ==> A[k] <= A[pivot];
-  ensures forall k :: pivot <= k < hi ==> A[pivot] <= A[k];
+  ensures forall k :: lo <= k < pivot ==> A[k] < A[pivot];
+  ensures forall k :: pivot < k < hi ==> A[pivot] <= A[k];
   modifies A;
 {
   pivot := lo;
   var i := lo+1;
   while i < hi
-    invariant 0 <= lo <= pivot < i <= hi
-    invariant forall k :: (0 <= k < lo || hi <= k < A.Length) ==> old(A[k]) == A[k]
-    invariant forall k :: (k==pivot) ==> A[k] == old(A[lo])
-    invariant forall k :: (lo <= k <= pivot) ==> A[k] <= A[pivot]
-    invariant forall k :: (pivot <= k < i) ==> A[k] >= A[pivot]
-    decreases hi - i
+    invariant 0 <= lo <= pivot < i <= hi;
+    invariant forall k :: (0 <= k < lo || hi <= k < A.Length) ==> old(A[k]) == A[k];
+    invariant forall k :: (lo <= k < pivot) ==> A[k] < A[pivot];
+    invariant forall k :: (pivot < k < i)   ==> A[pivot] <= A[k];
+    invariant hi < A.Length ==> forall k :: lo <= k < hi ==> A[k] < A[hi];
+    invariant 0  < lo       ==> forall k :: lo <= k < hi ==> A[lo-1] <= A[k];
   {
     if A[i] < A[pivot] {
       var j := i-1;
       var tmp := A[i];
       A[i] := A[j];
       while pivot < j
-        invariant forall k :: (0 <= k < lo || hi <= k < A.Length) ==> old(A[k]) == A[k]
-        invariant forall k :: (k==pivot) ==> A[k] == old(A[lo])
-        invariant forall k :: (pivot <= k <= i) ==> A[k] >= A[pivot]
-        invariant forall k :: (lo <= k <= pivot) ==> A[k] <= A[pivot]
-        invariant A[pivot] > tmp
-        decreases j
+        invariant forall k :: (0 <= k < lo || hi <= k < A.Length) ==> old(A[k]) == A[k];
+        invariant forall k :: (pivot < k <= i)  ==> A[pivot] <= A[k];
+        invariant forall k :: (lo <= k < pivot) ==> A[k] < A[pivot];
+        invariant A[pivot] > tmp;
+        invariant hi < A.Length ==> forall k :: lo <= k < hi ==> A[k] < A[hi];
+        invariant 0  < lo       ==> forall k :: lo <= k < hi ==> A[lo-1] <= A[k];
       {
         A[j+1] := A[j];
         j := j-1;
@@ -131,53 +135,42 @@ method partition(A:array<int>, lo:int, hi:int) returns (pivot:int)
   }
 }
 
-predicate sorted_seq(A:seq<int>)
+predicate sorted_between(A: array<int>, lo: int, hi: int)
+  reads A;
+  requires 0 <= lo <= hi <= A.Length;
 {
-  forall m,n :: 0 <= m < n < |A| ==> A[m] <= A[n]
+  forall m, n :: lo <= m < n < hi ==> A[m] <= A[n]
 }
 
 method quicksort_between(A:array<int>, lo:int, hi:int)
-  requires A.Length == 2;
   requires 0 <= lo <= hi <= A.Length;
+  requires hi < A.Length ==> forall k :: lo <= k < hi ==> A[k] < A[hi];
+  ensures  hi < A.Length ==> forall k :: lo <= k < hi ==> A[k] < A[hi];
+  requires 0 < lo ==> forall k :: lo <= k < hi ==> A[lo-1] <= A[k];
+  ensures  0 < lo ==> forall k :: lo <= k < hi ==> A[lo-1] <= A[k];
   ensures forall k :: (0 <= k < lo || hi <= k < A.Length) ==> old(A[k]) == A[k];
   // old(A[k]) evaluates to the value of A[k] on entry to the method, so this
   // checkes that only values in A[lo..hi] can be modified by this method
-  // ensures sorted_seq(A[lo..hi]);
+  ensures sorted_between(A, lo, hi);
   modifies A;
   decreases hi - lo;
 {
   if lo+1 >= hi { return; }
   var pivot := partition(A, lo, hi);
-  assert forall a :: a in A[lo..pivot] ==> a <= A[pivot];
-  assert forall a :: a in A[pivot..hi] ==> A[pivot] <= a;
   quicksort_between(A, lo, pivot);
-  // assert sorted_seq(A[lo..pivot]);
-  // assert sorted_seq(A[pivot..hi]);
-  assert forall a :: a in A[lo..pivot] ==> a <= A[pivot];
-  assert forall a :: a in A[pivot..hi] ==> A[pivot] <= a;
   quicksort_between(A, pivot+1, hi);
-  // assert sorted_seq(A[lo..pivot]);
-  // assert sorted_seq(A[pivot..hi]);
-  // assert forall a :: a in A[lo..pivot] ==> a <= A[pivot];
-  // assert forall a :: a in A[pivot..hi] ==> A[pivot] <= a;
-
 }
 
 method quicksort(A:array<int>)
   modifies A;
-  requires A.Length == 2;
-  // ensures sorted(A);
+  ensures sorted(A);
 {
   quicksort_between(A, 0, A.Length);
 }
 
 method Main() {
-  // var A:array<int> := new int[7] [4,0,1,9,7,1,2];
-  // print "Before: ", A[0], A[1], A[2], A[3], A[4], A[5], A[6], "\n";
-  // quicksort(A);
-  // print "After:  ", A[0], A[1], A[2], A[3], A[4], A[5], A[6], "\n";
-  var A:array<int> := new int[2] [1040, -197];
-  print "Before: ", A[0], " ", A[1], "\n";
+  var A:array<int> := new int[7] [4,0,1,9,7,1,2];
+  print "Before: ", A[0], A[1], A[2], A[3], A[4], A[5], A[6], "\n";
   quicksort(A);
-  print "After:  ", A[0], " ", A[1], "\n";
+  print "After:  ", A[0], A[1], A[2], A[3], A[4], A[5], A[6], "\n";
 }