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

(40steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-support-feasible 1 1 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)

L)
9. (destination(l)

L)
10. rcv(l; tg)

dom(1of(2of(M(source(l)))))

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

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

By:	Unfold `l_all` 5 THEN InstHyp [source(l);<l,tg,1of(2of(M(source(l))))(rcv(l; tg))>] 5 THEN All Reduce

Generated subgoals:

1 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)))))
  1of(2of(M(source(l))))(rcv(l; tg))  Type
1 step

2 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)))
12 steps

3 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)))))
11. interface-check(D;l;tg;1of(2of(M(source(l))))(rcv(l; tg)))
  1of(2of(M(source(l))))(rcv(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

(40steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc

1	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))))) 1of(2of(M(source(l))))(rcv(l; tg)) Type	1 step
2	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)))	12 steps
3	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))))) 11. interface-check(D;l;tg;1of(2of(M(source(l))))(rcv(l; tg))) 1of(2of(M(source(l))))(rcv(l; tg)) r M(destination(l)).din(l,tg)	1 step