Nuprl - Proof: finite-support-feasible 1 1 1 2 1

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

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

i:Id. (i

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

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

i:Id.
5. (i

L)
5.

5. (

ltg:(IdLnk

Type).
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)))))

1of(2of(M(source(l))))(rcv(l; tg))

Type

By:	MoveToConcl -1 THEN GenConclMsgA THEN Unfold_MsgA -2

Generated subgoals:

None

About:

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