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. fpf-is-empty(ds)
11. fpf-is-empty(da)
12. fpf-is-empty(init)
13. fpf-is-empty(pre)
14. fpf-is-empty(ef)
15. fpf-is-empty(send)
16. fpf-is-empty(frame)
17. fpf-is-empty(sframe)
18. fpf-is-empty(ds)  
19. fpf-is-empty(da)  
20. fpf-is-empty(init)  
21. fpf-is-empty(pre)  
22. fpf-is-empty(ef)  
23. fpf-is-empty(send)  
24. fpf-is-empty(frame)  
25. fpf-is-empty(sframe)  
26. z : Top
  <ds,da,init,pre,ef,send,frame,sframe,z>  MsgA

None

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