1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
5. (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L)
5. (iL.(ltgma-outlinks(M(i);i).
5. interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
6. i : Id
7. i:Id. map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(i)))))))))  IdLnk List
  L:IdLnk List. 
  l:IdLnk. destination(l) = i & M(source(l)) sends on link l  (l  L)

By:	AssertBY ((i.map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(i))))))))))  Id(IdLnk List)) (Auto THEN BackThruSomeHyp) THEN InstConcl [concat(map(i.map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(i)))))))));L))]

1

8. (i.map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(i)))))))))) 8.  Id(IdLnk List) 9. l : IdLnk 10. destination(l) = i 11. M(source(l)) sends on link l   (l  concat(map(i.map(p.   2of(p);1of(1of(2of(2of(2of(2of(2of(M(i)))))))));L)))

7 steps

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