predicate sorted(s: seq<int>) {
  forall i,j: int :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

predicate sameElements(sa: seq<int>, sb: seq<int>) {
  multiset(sa) == multiset(sb)
}

lemma SubSort(s: seq<int>, i: int, j: int)
  requires sorted(s)
  requires 0 <= i < j <= |s|
  ensures sorted(s[i..j])
{
}

method SlowSortHelper(a: array<int>, startIdx: int, endIdx: int)
  requires 0 <= startIdx <= endIdx < a.Length
  modifies a
  ensures a[..startIdx] == old(a[..startIdx])
  ensures endIdx < a.Length ==> a[endIdx + 1..] == old(a[endIdx + 1..])
  ensures sorted(a[startIdx..endIdx + 1])
  ensures multiset(a[startIdx..endIdx + 1]) == multiset(old(a[startIdx..endIdx + 1]))
  decreases endIdx - startIdx
{
  if (endIdx == startIdx) {
    return;
  }
  
  var middleIdx: int := (startIdx + endIdx) / 2;
  assert sameElements(a[startIdx..endIdx + 1], old(a[startIdx..endIdx + 1]));

  SlowSortHelper(a, startIdx, middleIdx);     
  SlowSortHelper(a, middleIdx + 1, endIdx);

  assert 0 <= startIdx <= middleIdx < endIdx;   
  assert a[..startIdx] == old(a[..startIdx]);   
  assert endIdx < a.Length ==> a[endIdx + 1..] == old(a[endIdx + 1..]);   
  
  assert sorted(a[startIdx..middleIdx + 1]);  
  assert sorted(a[middleIdx + 1..endIdx + 1]);

  if (a[endIdx] < a[middleIdx]) {
    a[endIdx], a[middleIdx] := a[middleIdx], a[endIdx];
  }

  assert a[middleIdx] <= a[endIdx];
  assert forall j: int :: startIdx <= j <= endIdx ==> a[j] <= a[endIdx];

  SlowSortHelper(a, startIdx, endIdx - 1);

  assert 0 <= startIdx <= middleIdx < endIdx;   
  assert sorted(a[startIdx..endIdx]);
  assert multiset(a[startIdx..endIdx]) == multiset(old(a[startIdx..endIdx]));
  assert forall j: int :: startIdx <= j <= endIdx ==> old(a[j]) <= a[endIdx];


//  assert 0 <= startIdx < middleIdx + 1 <= endIdx;  
//  assert sorted(a[startIdx..endIdx]);  
 
//  assert a[..startIdx] == old(a[..startIdx]);   
//  assert endIdx < a.Length ==> a[endIdx + 1..] == old(a[endIdx + 1..]);   
  
//  assert sorted(a[startIdx..endIdx]);
//  assert middleIdx <= endIdx ==> a[middleIdx] < a[endIdx];

//  assert forall j: int :: startIdx <= j < endIdx ==> a[j] <= a[endIdx];

}

method SlowSort(a: array<int>)
modifies a
ensures sorted(a[..])
ensures sameElements(a[..], old(a[..]))
{
  if (a.Length > 1) {
    SlowSortHelper(a, 0, a.Length - 1);
  }
}