Yes, from left in left.repr and left.repr < repr , it follows that
left in repr . However, where does left in left.repr come from? It can only come from
left.Valid() and the definition of Valid . But to prove that the call to
left.Valid() terminates, you must prove the decreases clause of the call
left.Valid() (which is left.repr + {left}  since no explicit
decreases clause is provided, Dafny constructs this one from the
reads clause) to be a strict subset of the decreases clause of
Valid() (which is repr + {this}  hint: if you're unsure of what these automatically constructed
decreases clauses are, inspect the hover text in the Visual Studio or emacs IDE). That, in turn, is true only if
left in left.repr ! So, there is a circularity you need to break.
The standard way to break this circularity is to write the line above as:
left != null ==> left in repr && left.repr <= repr && this !in left.repr && left.Valid()
I would recommend doing this. (That's also what you get if you make use of the
{:autocontracts} attribute.)
Note, there's one other difference in what I wrote and what you wrote, namely that I wrote
left.repr <= repr instead of left.repr < repr . It's really the latter that is of interest. However, it usually comes up that you need
this !in left.repr as well, in which case left.repr <= repr implies
left.repr < repr . The logical encoding of left.repr < repr in Dafny is
left.repr <= repr && exists x :: x !in left.repr && x in repr . That's a rather clumsy encoding, so since
<= is good enough here, I suggest using left.repr <= repr && this !in repr .
I have two more comments. One is that I suggest you add a conjunct null !in repr as part of the definition of
Valid() . Before I got into the habit of doing this, I several times found myself very confused about why some particular proof obligation didn't hold, only to find that it didn't hold for the value
null . You can avoid such confusion by always including null !in repr (unless you have some strong reason to believe it would be convenient to allow
null in repr ).
The other thing is that the form of the body of your Valid() is overly complicated. After the conjunct
this in repr , you have written something of the form:
(L && R) 
((!L ==> P) && (!R ==> Q))
Note that the first disjunct (that is, L && R ) is stronger than the second. Therefore, you might as well just write:
(!L ==> P) && (!R ==> Q)
Rustan
