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)
18. e1 : E
19. loc(e1) = i
20. kind(e1) = locl(a)
21. WellFnd{i}(E;x,y.(x <loc y))
22. j : E
23. k:E. (k <loc j)  (e1 <loc k)  ("done" when k)
24. first(j)
25. (e1 <loc pred(j))
26. "done"  Id
27. ("done" when j) = ("done" after pred(j))
28. ("done" when pred(j))
29. ("done" after pred(j))
  False

By:	Unfold `es-locl` -5 THEN AllHyps (h.Unfold `alle-at` h THEN InstHyp [pred(j)] h)

1	17. e:E.  17. loc(e) = i  Id 17.  17. ("done" after e) = ("done" when e)    kind(e) = locl(a) 18. e1 : E 19. loc(e1) = i  Id 20. kind(e1) = locl(a) 21. WellFnd{i}(E;x,y.(x <loc y)) 22. j : E 23. k:E. (k <loc j)  (e1 <loc k)  ("done" when k) 24. first(j) 25. loc(e1) = loc(pred(j))  Id 26. (e1 < pred(j)) 27. "done"  Id 28. ("done" when j) = ("done" after pred(j))  vartype(loc(j);"done") 29. ("done" when pred(j)) 30. ("done" after pred(j))   ("done" after pred(j)) = ("done" when pred(j))	3 steps
2	17. e:E.  17. loc(e) = i  Id 17.  17. ("done" after e) = ("done" when e)    kind(e) = locl(a) 18. e1 : E 19. loc(e1) = i  Id 20. kind(e1) = locl(a) 21. WellFnd{i}(E;x,y.(x <loc y)) 22. j : E 23. k:E. (k <loc j)  (e1 <loc k)  ("done" when k) 24. first(j) 25. loc(e1) = loc(pred(j))  Id 26. (e1 < pred(j)) 27. "done"  Id 28. ("done" when j) = ("done" after pred(j))  vartype(loc(j);"done") 29. ("done" when pred(j)) 30. ("done" after pred(j)) 31. kind(pred(j)) = locl(a)   False	1 step

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