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)
10. & fpf-is-empty(da)
10. & fpf-is-empty(init)
10. & fpf-is-empty(pre)
10. & fpf-is-empty(ef)
10. & fpf-is-empty(send)
10. & fpf-is-empty(frame)
10. & fpf-is-empty(sframe)
11. fpf-is-empty(ds)  
12. fpf-is-empty(da)  
13. fpf-is-empty(init)  
14. fpf-is-empty(pre)  
15. fpf-is-empty(ef)  
16. fpf-is-empty(send)  
17. fpf-is-empty(frame)  
18. fpf-is-empty(sframe)  
  <ds,da,init,pre,ef,send,frame,sframe,> =   MsgA

By:	Fold `mk-ma` 0 THEN Unfold `ma-empty` 0 THEN Analyze THEN Try (BackThru (Thm* B:(AType), f:x:A fp-> B(x). fpf-is-empty(f)  f =   x:A fp-> B(x)) THEN Try (Unfold `ma-valtype` 0)

None

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