(8steps total) PrintForm Definitions mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: send-once realizes 1 1 1 1 1

1. T : Type
2. A : Type
3. a : Id
4. f : AT
5. tg : Id
6. l : IdLnk
7. x : Id
8. "done" = x
9. A
10. T
11. (loc.(send-once(loc;T;A;a;f;tg;l;x)))  Dsys
12. D' : Dsys
13. loc.(send-once(loc;T;A;a;f;tg;l;x))  D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. e : E
18. loc(e) = source(l)
19. kind(e) = locl(a)
20. e:E. 
20. loc(e) = source(l)
20. 
20. (e':E. 
20. (loc(e') = source(l kind(e) = locl(a kind(e') = locl(a e = e')
21. @source(l): ma-single-sends1(A; Unit; Tx; locl(a); ltg; (a,b. [(f(a))])
21. @source(l): ma-single-sends1()
21.  Dsys
22. vartype(source(l);xA
23. e:E. loc(e) = source(l kind(e) = locl(a (valtype(er Unit)
24. e:E. kind(e) = rcv(ltg (valtype(eT)
25. e:E. 
25. loc(e) = source(l)
25. 
25. kind(e) = locl(a)
25. 
25. (e':E. 
25. (kind(e') = rcv(ltg)
25. (& sender(e') = e
25. (& & (e'':E. kind(e'') = rcv(ltg sender(e'') = e  e'' = e')
25. (& & val(e') = f((x when e)))
26. e' : E
27. kind(e') = rcv(ltg)
28. sender(e') = e
29. e'':E. kind(e'') = rcv(ltg sender(e'') = e  e'' = e'
30. val(e') = f((x when e))
31. z : E
32. z = e
  vartype(loc(e);xA


By: AllHyps (h.NthHypEq h THEN Complete (Repeat Analyze))


Generated subgoals:

None

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

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