Nuprl - Proof: finite-support-feasible 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-support-feasible 1 2

1. D : Dsys
2. L : Id List
3.

i:Id. (i

ma-is-empty(M(i))
4.

i:Id. Feasible(M(i))
5. (

L.(

ltg

ma-outlinks(M(i);i).(destination(1of(ltg))

L)
5. (

L.(

ltg

ma-outlinks(M(i);i).

5. interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
6. l : IdLnk
7. tg : Id
8.

(source(l)

M(source(l)).dout(l,tg)

r M(destination(l)).din(l,tg)

By:	Subst (M(source(l)) = ) 0

Generated subgoals:

1 M(source(l)) =
2 steps

2 .dout(l,tg) r M(destination(l)).din(l,tg)
1 step

About:

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

1	M(source(l)) =	2 steps
2	.dout(l,tg) r M(destination(l)).din(l,tg)	1 step