1. a : Id
2. i : Id
3. (loc.(once(loc;a;i)))  Dsys
4. D' : Dsys
5. loc.(once(loc;a;i))  D'
6. w : World
7. p : FairFifo
8. PossibleWorld(D';w)
9. @i: ma-single-pre-init1("done";;false;a;Unit;x,v.x)  Dsys
10. vartype(i;"done") r 
11. e:E. loc(e) = i  first(e)  ("done" when e) = false
12. e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r Unit)
13. e:E. loc(e) = i  kind(e) = locl(a)  ("done" when e)
14. e : E
15. loc(e) = i
16. kind(e) = locl(a)  (v:Unit. ("done" after e))
17. e@i.("done" after e) = ("done" when e)  kind(e) = locl(a)
  e:E. 
  loc(e) = i  Id
  
  (e':E. 
  (loc(e') = i  Id  kind(e) = locl(a)  kind(e') = locl(a)  e = e')

By:	Assert (e':E.  (loc(e') = i  (e:E. (e <loc e')  kind(e) = locl(a)  kind(e') = locl(a)))

1	e':E.    loc(e') = i  Id      (e:E. (e <loc e')  kind(e) = locl(a)  kind(e') = locl(a))	36 steps
2	18. e':E.  18. loc(e') = i  Id 18.  18. (e:E. (e <loc e')  kind(e) = locl(a)  kind(e') = locl(a))   e:E.    loc(e) = i  Id      (e':E.    (loc(e') = i  Id  kind(e) = locl(a)  kind(e') = locl(a)  e = e')	2 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html