(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 2 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. 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. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
  (<l,tg,da(rcv(l; tg))>  mapfilter(k.da-outlink-f(da;k);k.
  has-src(source(l);k);fpf-dom-list(da)))
By: Inst
Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'.
Thm* (x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y))
[lexpr{i'}
;{k:Knd| k  dom(da) }
;k.has-src(source(l);k)
;IdLnkIdType{i}
;k.da-outlink-f(da;k)
;fpf-dom-list(da)
;<l,tg,da(rcv(l; tg))>]
THENA
(Reduce 0 THEN DVar `k' THEN DVar `k'
(THEN
(RWO Thm* i:Id, k:Knd. has-src(i;k)  isrcv(k) & source(lnk(k)) = i -1
(THEN
(ExRepD)
THEN
Analyze -1
THEN
Thin -2
THEN
Analyze -1
THEN
Try Trivial
THEN
Reduce 0
THEN
InstConcl [rcv(l; tg)]

Generated subgoals:

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. 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. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
  rcv(l; tg)  {k:Knd| k  dom(da) }
1 step
2 1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
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. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
  (rcv(l; tg)  fpf-dom-list(da))
5 steps
3 1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
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. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
  has-src(source(l);rcv(l; tg))
1 step
4 1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
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. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
  <l,tg,da(rcv(l; tg))> = da-outlink-f(da;rcv(l; tg))  IdLnkIdType
1 step
5 1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
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. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
21. y : {k:Knd| k  dom(da) }
22. has-src(source(l);y)
  y  {k:Knd| k  dom(da) & isrcv(k) }
1 step

About:
pairproductproductlistboolassertvoidsetlambdaapplyfunction
universeequalmembertoppropimpliesandorallexists
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