Dafny: Method times out when unrelated conditions are added

I've created a verified SortedMap in Dafny. It is a sequence of (key, value) pairs. The keys are sorted, distinct integers. When I use this simple definition for KeySetWithoutExtraPost, the Insert method verifies:

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}
function KeySetWithoutExtraPost(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
{
  set i | i in sorted_seq :: i.0
}
method Insert(sorted_seq: seq<(int, int)>, pair: (int,int)) returns (r: seq<(int, int)>)
  requires SortedSeq(sorted_seq)
  ensures SortedSeq(r)
  ensures KeySetWithoutExtraPost(r) == KeySetWithoutExtraPost(sorted_seq) + {pair.0}
  ensures pair in r
{
  var i := IndexBefore(sorted_seq, pair.0);
  r :=
    if i < |sorted_seq| && sorted_seq[i].0 == pair.0
    then
      sorted_seq[..i] + [pair] + sorted_seq[i+1..]
    else
      sorted_seq[..i] + [pair] + sorted_seq[i..];
}
method IndexBefore(sorted_seq:  seq<(int, int)>, x: int) returns (i: int)
  requires SortedSeq(sorted_seq)
  ensures 0 <= i <= |sorted_seq|
  ensures forall j | 0 <= j < i :: sorted_seq[j].0 < x
  ensures forall j | i <= j < |sorted_seq| :: x <= sorted_seq[j].0
  ensures sorted_seq[..i] + sorted_seq[i..] == sorted_seq
{
  i := 0;
  while i < |sorted_seq| && sorted_seq[i].0 < x
    invariant 0 <= i <= |sorted_seq|
    invariant forall j | 0 <= j < i :: sorted_seq[j].0 < x
  {
    i := i + 1;
  }
}

However, when I swap in this fancier definition (based on this answer), the verification times out.

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
  ensures KeySet(sorted_seq) == set i | i in sorted_seq :: i.0
{
  if sorted_seq == [] then
    {}
  else
    {sorted_seq[0].0} + KeySet(sorted_seq[1..])
}

function KeySetWithoutExtraPost(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  KeySet(sorted_seq)
}

Is there a way to get it to validate? Interestingly, the Delete method (not shown) works fine.

-- Carl

I got this working. First, I used some "assume false;"'s as recommended in the Dafny Reference.

I ended up creating both a simple KeySet that just turns a sequence into a set and more complicated SortedKeySet that knows the length of a set created from a sorted & distinct sequence is the length of the sequence.

Here is the example, working:

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function SortedKeySetWithExtra(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |SortedKeySetWithExtra(sorted_seq)| == |sorted_seq|
  ensures SortedKeySetWithExtra(sorted_seq) == KeySet(sorted_seq)
{
  if sorted_seq == [] then
    {}
  else
    {sorted_seq[0].0} + SortedKeySetWithExtra(sorted_seq[1..])
}

function SortedKeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |SortedKeySetWithExtra(sorted_seq)| == |sorted_seq|
{
  SortedKeySetWithExtra(sorted_seq)
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
{
  set i | i in sorted_seq :: i.0
}


method Insert(sorted_seq: seq<(int, int)>, pair: (int,int)) returns (r: seq<(int, int)>)
  requires SortedSeq(sorted_seq)
  ensures SortedSeq(r)
  ensures KeySet(r) == KeySet(sorted_seq) + {pair.0}
  ensures pair in r
  ensures | SortedKeySet(r) | == | r |
{
  var i := IndexBefore(sorted_seq, pair.0);
  if i < |sorted_seq| && sorted_seq[i].0 == pair.0
  {
    r:=sorted_seq[..i] + [pair] + sorted_seq[i+1..];
  }
  else
  {
    r:= sorted_seq[..i] + [pair] + sorted_seq[i..];
  }
}

method IndexBefore(sorted_seq:  seq<(int, int)>, x: int) returns (i: int)
  requires SortedSeq(sorted_seq)
  ensures 0 <= i <= |sorted_seq|
  ensures forall j | 0 <= j < i :: sorted_seq[j].0 < x
  ensures forall j | i <= j < |sorted_seq| :: x <= sorted_seq[j].0
  ensures sorted_seq[..i] + sorted_seq[i..] == sorted_seq
{
  i := 0;
  while i < |sorted_seq| && sorted_seq[i].0 < x
    invariant 0 <= i <= |sorted_seq|
    invariant forall j | 0 <= j < i :: sorted_seq[j].0 < x
  {
    i := i + 1;
  }
}


method Main()
{
  var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
  print SortedKeySet(s);

}