Verification timeout, not sure how to fix.

Mar 15, 2013 at 4:06 PM
I'm working towards a verification of Floyd's tortoise and hare algorithm, but Dafny is timing out trying to verify one of the sub lemmas:

I'm not sure how to fix this and make the proof go through, particularly since I've found it can't get past the first line of the proof, viz. this also times out: