IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-match-exists212121 1. the_w : World
2. e : E
3. i:Id, t:, l:IdLnk. source(l) = i onlnk(l;m(i;t)) = nil
4. i:Id, t:. isnull(a(i;t)) (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
5. i:Id, t:, l:IdLnk.
5. isrcv(l;a(i;t))
5. 5. destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))
6. l:IdLnk, t:.
6. t':. tt' & isrcv(l;a(destination(l);t')) queue(l;t') = nil
7. isrcv(kind(e))
8. isrcv(lnk(kind(e));a(loc(e);time(e)))
9. destination(lnk(kind(e))) = loc(e)
10. r : 11. ||rcvs(lnk(kind(e));time(e))|| = r 12. ms : Msg
13. msg(a(loc(e);time(e))) = ms 14. l : IdLnk
15. lnk(kind(e)) = l 16. t' : 17. time(e) = t' r<||snds(l;t')||
snds(l;t')[r] = ms Msg
(t:t'. (||snds(l;t)||r)(r<||snds(l;t)||+||onlnk(l;m(source(l);t))||))
By:
AssertBY (t:t'. ||onlnk(l;m(source(l);t))|| )
(Auto THEN GenConclAtAddr [2;1;2] THEN Fold `w-Msg` -2 THEN Unfold `w-Msg` -1)
THEN
RW assert_pushdownC 0
THEN
Try BackThruSomeHyp