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)
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)
34. v = i1(x)
35. x  dom(ds)
36. x  dom(d1)
  ds(x) = d1(x)  Type

By:	AllHyps (h.Unfold `fpf-sub` h THEN InstHyp [x] h THENA Complete Auto)

1

21. x:Id. x  dom(ds)  x  dom(d1) & ds(x) = d1(x)  Type 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 35. x  dom(ds) 36. x  dom(d1) 37. x  dom(d1) & ds(x) = d1(x)  Type   ds(x) = d1(x)  Type

1 step

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