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. rcv(l; tg)  dom(1of(2of(M(source(l)))))
  (<l
  (,tg
  (,1of(2of(M(source(l))))(rcv(l; tg))>  ma-outlinks(M(source(l));source(l)))

1

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)   (<l,tg,da(rcv(l; tg))>  da-outlinks(da;source(l)))

11 steps

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