(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 1 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)) & has-src(i;y) & ltg = da-outlink-f(da1;y))
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)) & has-src(i;y) & ltg = da-outlink-f(da2;y))
8. y : {k:Knd| k  dom(da1  da2) }
9. (y  fpf-dom-list(da1  da2))
10. has-src(i;y)
11. ltg = da-outlink-f(da1  da2;y)
  (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)))
By: Analyze -4 THEN AssertBY y  dom(da1  da2) Unhide THEN Decide y  dom(da1)

Generated subgoals:

1 8. y : Knd
9. y  dom(da1  da2)  [not for witness]
10. (y  fpf-dom-list(da1  da2))
11. has-src(i;y)
12. ltg = da-outlink-f(da1  da2;y)  IdLnkIdType
13. y  dom(da1  da2)
14. y  dom(da1)
  (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)))
10 steps
2 8. y : Knd
9. y  dom(da1  da2)  [not for witness]
10. (y  fpf-dom-list(da1  da2))
11. has-src(i;y)
12. ltg = da-outlink-f(da1  da2;y)  IdLnkIdType
13. y  dom(da1  da2)
14. y  dom(da1)
  (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)))
14 steps

About:
productassertsetlambdauniverseequalandorexists
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