(58steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: once realizes 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") 
11. e:E. loc(e) = i  first(e ("done" when e) = false
12. e:E. loc(e) = i  kind(e) = locl(a (valtype(er 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))
  e@i.kind(e) = locl(a)
  e@i.e'@i.kind(e) = locl(a kind(e') = locl(a e = e'  E


By: Assert e@i.("done" after e) = ("done" when e kind(e) = locl(a)


Generated subgoals:

1   e@i.("done" after e) = ("done" when e   kind(e) = locl(a)
1 step
2 17. e@i.("done" after e) = ("done" when e   kind(e) = locl(a)
  e@i.kind(e) = locl(a)
  e@i.e'@i.kind(e) = locl(a kind(e') = locl(a e = e'  E

55 steps

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

(58steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc