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. M8 : 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,M8> =   MsgA

By:	Subst (M8 = ) 0

1	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)     M8 =   Top	1 step
2	<ds,da,init,pre,ef,send,frame,sframe,> =   MsgA	1 step
3	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	1 step

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