IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-send wf2111 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. x:Id fp-> ds(x)?Void
4. a:Id fp-> State(ds)da(locl(a))?TopProp
5. 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. x:Id fp-> Knd List
8. ltg:IdLnkId fp-> Knd List
9. Top
10. k : Knd
11. l : IdLnk
12. State(ds)
13. ma-valtype(da; k)
14. i : Id
15. (tg:Idif source(l) = ida(rcv(l; tg))?Top else Top fi) List
16. <k,l> dom(send)
17. source(l) = i 18. tg:IdState(ds)da(k)?Top(da(rcv(l; tg))?Void List)
ma-valtype(da; k) r da(k)?Top
By:
Unfold `ma-valtype` 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html