1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
5. i:Id. 
5. (i  L)
5. 
5. (ltg:(IdLnkIdType). 
5. ((ltg  ma-outlinks(M(i);i))
5. (
5. ((destination(1of(ltg))  L)
5. (
5. (interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg))))
6. l : IdLnk
7. tg : Id
8. (source(l)  L)
9. (destination(l)  L)
10. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
  rcv(l; tg)  {k:Knd| k  dom(da) }

None

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