M1,M2:MsgA.
  M1  M2
  
  (a:Id, s:M2.state, v:M2.da(locl(a)). M2.pre(a,s,v)  M1.pre(a,s,v))

By:	RepeatFor 6 (Analyze 0 THENA Complete Auto) THEN Unfold_MsgA -6 THEN Unfold_MsgA -5 THEN SplitAndHyps THEN Unfold `fpf-val` 0 THEN AllHyps (h.Unfold `fpf-sub` h THEN InstHyp [a] h THENA Complete Auto) THEN ExRepD THEN ThinTrivial

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. Top 10. d1 : x:Id fp-> Type 11. d2 : a:Knd fp-> Type 12. i1 : x:Id fp-> d1(x)?Void 13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp 14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void 15. s1 :  15. kl:KndIdLnk fp-> (tg:Id 15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top 15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List 16. f1 : x:Id fp-> Knd List 17. s2 : ltg:IdLnkId fp-> Knd List 18. Top 19. ds  d1 20. da  d2 21. init  i1 22. x:Id.  22. x  dom(pre) 22.  22. x  dom(p1) & pre(x) = p1(x)  State(d1)d2(locl(x))?TopProp 23. ef  e1 24. send  s1 25. frame  f1 26. sframe  s2 27. a : Id 28. s : State(d1) 29. v : d2(locl(a))?Top 30. a  dom(pre) 31. a  dom(p1) 32. pre(a) = p1(a)  State(d1)d2(locl(a))?TopProp 33. p1(a)(s,v)   pre(a)(s,v)

1 step

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