a,i:Id.
  loc.(once(loc;a;i)) 
  realizes es.e@i.kind(e) = locl(a)
  realizes es.& e@i.e'@i.kind(e) = locl(a)
  realizes es.& e@i.e'@i.
  realizes es.& kind(e') = locl(a)  Knd  e = e'  E

By:	RealizerSetup THEN PreInitRule1 i a "done"  Unit false (x,v. x)

1

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  Id  first(e)  ("done" when e) = false 12. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r Unit) 13. e:E. loc(e) = i  Id  kind(e) = locl(a)  ("done" when e) 14. e : E 15. loc(e) = i  Id 16. kind(e) = locl(a)  (v:Unit. ("done" after e))   e@i.kind(e) = locl(a)   & e@i.e'@i.kind(e) = locl(a)  kind(e') = locl(a)  e = e'  E

57 steps

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