(12steps total) PrintForm Definitions mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-init-sub
  V:(IdType), M1,M2:MsgA.
  (x:Id. V(x) r M2.ds(x))
  
  M1  M2  (x:Id, v:V(x). M2.init(x,v)  M1.init(x,v))
By: Repeat (Analyze 0 THENA Complete Auto) THEN Unfold_MsgA -6 THEN Unfold_MsgA -5
THEN
SplitAndHyps
THEN
Unfold `fpf-val` 0
THEN
Try (DoSubsume THEN BackThruSomeHyp)
THEN
AllHyps (h.Unfold `fpf-sub` h THEN InstHyp [x] h THENA Complete Auto)
THEN
ExRepD
THEN
ThinTrivial

Generated subgoals:

1 1. V : IdType
2. ds : x:Id fp-> Type
3. da : a:Knd fp-> Type
4. init : x:Id fp-> ds(x)?Void
5. pre : a:Id fp-> State(ds)ma-valtype(da; locl(a))Prop
6. ef : kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void
7. send : 
7. kl:KndIdLnk fp-> (tg:Id
7. kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl))
7. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
8. frame : x:Id fp-> Knd List
9. sframe : ltg:IdLnkId fp-> Knd List
10. Top
11. d1 : x:Id fp-> Type
12. d2 : a:Knd fp-> Type
13. i1 : x:Id fp-> d1(x)?Void
14. p1 : a:Id fp-> State(d1)ma-valtype(d2; locl(a))Prop
15. e1 : kx:KndId fp-> State(d1)ma-valtype(d2; 1of(kx))d1(2of(kx))?Void
16. s1 : 
16. kl:KndIdLnk fp-> (tg:Id
16. kl:KndIdLnk fp-> (State(d1)ma-valtype(d2; 1of(kl))
16. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
17. f1 : x:Id fp-> Knd List
18. s2 : ltg:IdLnkId fp-> Knd List
19. Top
20. x:Id. V(x) r d1(x)?Top
21. ds  d1
22. da  d2
23. x:Id. x  dom(init)  x  dom(i1) & init(x) = i1(x)  d1(x)?Void
24. pre  p1
25. ef  e1
26. send  s1
27. frame  f1
28. sframe  s2
29. x : Id
30. v : V(x)
31. x  dom(init)
32. x  dom(i1)
33. init(x) = i1(x)  d1(x)?Void
34. v = i1(x)  d1(x)?Void
  v = init(x)  ds(x)?Void
7 steps
2 1. V : IdType
2. ds : x:Id fp-> Type
3. da : a:Knd fp-> Type
4. init : x:Id fp-> ds(x)?Void
5. pre : a:Id fp-> State(ds)ma-valtype(da; locl(a))Prop
6. ef : kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void
7. send : 
7. kl:KndIdLnk fp-> (tg:Id
7. kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl))
7. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
8. frame : x:Id fp-> Knd List
9. sframe : ltg:IdLnkId fp-> Knd List
10. Top
11. d1 : x:Id fp-> Type
12. d2 : a:Knd fp-> Type
13. i1 : x:Id fp-> d1(x)?Void
14. p1 : a:Id fp-> State(d1)ma-valtype(d2; locl(a))Prop
15. e1 : kx:KndId fp-> State(d1)ma-valtype(d2; 1of(kx))d1(2of(kx))?Void
16. s1 : 
16. kl:KndIdLnk fp-> (tg:Id
16. kl:KndIdLnk fp-> (State(d1)ma-valtype(d2; 1of(kl))
16. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
17. f1 : x:Id fp-> Knd List
18. s2 : ltg:IdLnkId fp-> Knd List
19. Top
20. x:Id. V(x) r d1(x)?Top
21. ds  d1
22. da  d2
23. init  i1
24. pre  p1
25. ef  e1
26. send  s1
27. frame  f1
28. sframe  s2
29. x : Id
30. v : V(x)
31. x  dom(i1)
  v  d1(x)?Void
4 steps

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

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