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)
  v = init(x)  ds(x)?Void

1

ds(x)?Void = d1(x)?Void  Type

6 steps

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