(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. 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@source(l).kind(e) = locl(a)
18. e@source(l).e'@source(l).kind(e) = locl(a)  kind(e') = locl(a)  e = e'
19. @source(l): ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))])
19. @source(l): ma-single-sends1()
19.  Dsys
20. vartype(source(l);x) r A
21. e:E. loc(e) = source(l)  kind(e) = locl(a)  (valtype(e) r Unit)
22. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
23. e:E. 
23. loc(e) = source(l)
23. 
23. kind(e) = locl(a)
23. 
23. (e':E. 
23. (kind(e') = rcv(l; tg)
23. (& sender(e') = e
23. (& & (e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  e'' = e')
23. (& & val(e') = f((x when e)))
  (vartype(source(l);x) r A)
  & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))
  & (e:E. 
  & (kind(e) = rcv(l; tg)
  & (& val(e) = f((x when sender(e)))  T
  & (& & kind(sender(e)) = locl(a)
  & (& & (e':E. 
  & (& & (kind(e') = rcv(l; tg)  kind(sender(e')) = locl(a)  e' = e))
By: BetterSplitAndConcl THEN Try Trivial THEN Thin -1
THEN
All (Unfolds [`alle-at`;`existse-at`])
THEN
ExRepD
THEN
AllHyps
(h.
(InstHyp [e] h THENA Complete Auto THEN ParallelOp -1 THEN ExRepD THEN MaAuto)

Generated subgoals:

1 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; T; x; locl(a); l; tg; (a,b. [(f(a))])
21. @source(l): ma-single-sends1()
21.  Dsys
22. vartype(source(l);x) r A
23. e:E. loc(e) = source(l)  kind(e) = locl(a)  (valtype(e) r Unit)
24. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
25. e:E. 
25. loc(e) = source(l)
25. 
25. kind(e) = locl(a)
25. 
25. (e':E. 
25. (kind(e') = rcv(l; tg)
25. (& sender(e') = e  E
25. (& & (e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e')
25. (& & val(e') = f((x when e))  T)
26. e' : E
27. kind(e') = rcv(l; tg)
28. sender(e') = e  E
29. e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e'
30. val(e') = f((x when e))  T
  val(e') = f((x when sender(e')))  T
3 steps
2 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; T; x; locl(a); l; tg; (a,b. [(f(a))])
21. @source(l): ma-single-sends1()
21.  Dsys
22. vartype(source(l);x) r A
23. e:E. loc(e) = source(l)  kind(e) = locl(a)  (valtype(e) r Unit)
24. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
25. e:E. 
25. loc(e) = source(l)
25. 
25. kind(e) = locl(a)
25. 
25. (e':E. 
25. (kind(e') = rcv(l; tg)
25. (& sender(e') = e  E
25. (& & (e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e')
25. (& & val(e') = f((x when e))  T)
26. e' : E
27. kind(e') = rcv(l; tg)
28. sender(e') = e  E
29. e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e'
30. val(e') = f((x when e))  T
31. e'@0 : E
32. kind(e'@0) = rcv(l; tg)
33. kind(sender(e'@0)) = locl(a)
  e'@0 = e'
2 steps

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