(5steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-send-sub
  M1,M2:MsgA.
  M1  M2
  
  (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id
  (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i
  (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg))
  (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List.
  (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i))
By: RepeatFor 9 (Analyze 0 THENA Complete Auto) THEN Unfold_MsgA -9
THEN
Unfold_MsgA -8
THEN
SplitAndHyps
THEN
Unfold `fpf-val` 0
THEN
SplitOnConclITE

Generated subgoals:

1 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. Top
19. ds  d1
20. da  d2
21. init  i1
22. pre  p1
23. ef  e1
24. send  s1
25. frame  f1
26. sframe  s2
27. k : Knd
28. l : IdLnk
29. s : State(d1)
30. v : d2(k)?Top
31. i : Id
32. ms : (tg:Idif source(l) = i d2(rcv(l; tg))?Top else Top fi) List
33. source(l) = i
  (<k,l>  dom(s1)
  (
  (ms
  (=
  (concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));s1(<k,l>)))
  ( (tg:Idd2(rcv(l; tg))?Top) List)
  
  <k,l>  dom(send)
  
  ms
  =
  concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));send(<k,l>)))
   (tg:Idda(rcv(l; tg))?Top) List
3 steps
2 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. Top
19. ds  d1
20. da  d2
21. init  i1
22. pre  p1
23. ef  e1
24. send  s1
25. frame  f1
26. sframe  s2
27. k : Knd
28. l : IdLnk
29. State(d1)
30. d2(k)?Top
31. i : Id
32. ms : (tg:Idif source(l) = i d2(rcv(l; tg))?Top else Top fi) List
33. source(l) = i
  (<k,l>  dom(s1)  ms = nil  (IdTop) List)
  
  <k,l>  dom(send)  ms = nil  (IdTop) List
1 step

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

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