1. M : MsgA
2. ma-is-empty(M)
  M =   MsgA

By:

Unfold_MsgA -2 THEN All (Unfold `ma-is-empty`) THEN All Reduce THEN AssertBY (fpf-is-empty(ds)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN AssertBY (fpf-is-empty(da)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN AssertBY (fpf-is-empty(init)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN AssertBY (fpf-is-empty(pre)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN AssertBY (fpf-is-empty(ef)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN AssertBY (fpf-is-empty(send)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN AssertBY (fpf-is-empty(frame)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN AssertBY (fpf-is-empty(sframe)  ) (Unfold `fpf-is-empty` 0 THEN AllHyps (h.Analyze h THEN Reduce 0)) THEN All (i.RW assert_pushdownC i)

1

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

4 steps

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