(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 2 1 2 1 1 1
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
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
12. (source(l)  L)
  l1:IdLnk List. 
  (l1  map(i.map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(i)))))))));L))
  & (l  l1)
By: RWO
Thm* a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))
0
THEN
Reduce 0
THEN
InstConcl [map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(source(l))))))))))]
THEN
Try BackThruSomeHyp

Generated subgoals:

1   y:Id. 
  (y  L)
  & map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(source(l))))))))))
  & =
  & map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(y)))))))))
  &  IdLnk List
1 step
2   (l  map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M(source(l)))))))))))
1 step

About:
productlistassertlambdaapplyfunctionuniverseequal
memberimpliesandorallexists
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