(27steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: da-outlinks-join
  ltg:(IdLnkIdType{i}), i:Id, da1,da2:k:Knd fp-> Type{i}.
  (ltg  da-outlinks(da1  da2;i))
  
  (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i))
By: Auto THEN All (Unfold `da-outlinks`)
THEN
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(da1) }
;k.has-src(i;k)
;IdLnkIdType{i}
;k.da-outlink-f(da1;k)
;fpf-dom-list(da1)
;ltg]
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
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(da2) }
;k.has-src(i;k)
;IdLnkIdType{i}
;k.da-outlink-f(da2;k)
;fpf-dom-list(da2)
;ltg]
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
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(da1  da2) }
;k.has-src(i;k)
;IdLnkIdType{i}
;k.da-outlink-f(da1  da2;k)
;fpf-dom-list(da1  da2)
;ltg]
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
All Reduce

Generated subgoal:

1 1. ltg : IdLnkIdType
2. i : Id
3. da1 : k:Knd fp-> Type
4. da2 : k:Knd fp-> Type
5. (ltg  mapfilter(k.da-outlink-f(da1  da2;k);k.
5. has-src(i;k);fpf-dom-list(da1  da2)))
6. (ltg  mapfilter(k.da-outlink-f(da1;k);k.has-src(i;k);fpf-dom-list(da1)))
6. 
6. (y:{k:Knd| k  dom(da1) }. 
6. ((y  fpf-dom-list(da1))
6. (& has-src(i;y) & ltg = da-outlink-f(da1;y)  IdLnkIdType)
7. (ltg  mapfilter(k.da-outlink-f(da2;k);k.has-src(i;k);fpf-dom-list(da2)))
7. 
7. (y:{k:Knd| k  dom(da2) }. 
7. ((y  fpf-dom-list(da2))
7. (& has-src(i;y) & ltg = da-outlink-f(da2;y)  IdLnkIdType)
8. (ltg  mapfilter(k.da-outlink-f(da1  da2;k);k.
8. has-src(i;k);fpf-dom-list(da1  da2)))
8. 
8. (y:{k:Knd| k  dom(da1  da2) }. 
8. ((y  fpf-dom-list(da1  da2))
8. (& has-src(i;y) & ltg = da-outlink-f(da1  da2;y)  IdLnkIdType)
  (ltg  mapfilter(k.da-outlink-f(da1;k);k.has-src(i;k);fpf-dom-list(da1)))
   (ltg  mapfilter(k.da-outlink-f(da2;k);k.has-src(i;k);fpf-dom-list(da2)))
26 steps

About:
productlistboolassertsetlambdaapplyfunction
universeequalimpliesandorallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(27steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc