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)))))
  i:Id. 
  finite-type({l:IdLnk| destination(l) = i & M(source(l)) sends on link l })

By:	Auto THEN BackThru Thm* P:(TProp).  Thm* (x:T. Dec(P(x))) Thm*  Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))

1

6. i : Id   L:IdLnk List.    l:IdLnk. destination(l) = i & M(source(l)) sends on link l  (l  L)

10 steps

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