M:MsgA, a:Id, s:M.state, v:M.da(locl(a)). M.pre(a,s,v)  Prop

1

1. ds : x:Id fp-> Type 2. da : a:Knd fp-> Type 3. x:Id fp-> ds(x)?Void 4. pre : a:Id fp-> State(ds)ma-valtype(da; locl(a))Prop 5. kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void 6. kl:KndIdLnk fp-> (tg:Id 6. kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) 6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List 7. x:Id fp-> Knd List 8. ltg:IdLnkId fp-> Knd List 9. Top 10. a : Id 11. State(ds) 12. v : da(locl(a))?Top 13. a  dom(pre)   v  ma-valtype(da; locl(a))

1 step

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