---

Step * 1 1 1 1 1 2 1 1 of Lemma subset-co-regext


1. T : Type
2. f : T ⟶ coSet{i:l}
3. ∀i:T. ∀i@0:set-dom(f i).  ∃b:T. seteq(set-item(f i;i@0);f b)
4. b : T@i
5. G : i:T ⟶ i@0:set-dom(f i) ⟶ T
6. ∀i:T. ∀i@0:set-dom(f i).  seteq(set-item(f i;i@0);f (G i i@0))
7. p1 : copath(T.T;f b)@i
8. p2 : copath(T.T;regextfun(f;regextW(G;b)))@i
9. q1 : copath(T.T;f b)@i
10. q2 : copath(T.T;regextfun(f;regextW(G;b)))@i
11. g1 : copath-length(p1) = copath-length(p2) ∈ ℤ@i
12. b' : T@i
13. g4 : seteq(copath-at(f b;p1);f b')@i
14. g5 : seteq(copath-at(regextfun(f;regextW(G;b));p2);regextfun(f;regextW(G;b')))@i
15. copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ
16. copathAgree(T.T;f b;p1;q1)
17. p2 = q2 ∈ copath(T.T;regextfun(f;regextW(G;b)))
⊢ ∃r:{r:copath(T.T;f b) × copath(T.T;regextfun(f;regextW(G;b)))| 
      let u',v' = r 
      in (((copath-length(u') = (copath-length(q1) + 1) ∈ ℤ)
         ∧ copathAgree(T.T;f b;q1;u')
         ∧ (q2 = v' ∈ copath(T.T;regextfun(f;regextW(G;b)))))
         ∨ ((q1 = u' ∈ copath(T.T;f b))
           ∧ (copath-length(v') = (copath-length(q2) + 1) ∈ ℤ)
           ∧ copathAgree(T.T;regextfun(f;regextW(G;b));q2;v')))
         ∧ (copath-length(u') = copath-length(v') ∈ ℤ)} 
   ((copath-length(fst(r)) = copath-length(snd(r)) ∈ ℤ)
   ∧ (∃b':T
       (seteq(copath-at(f b;fst(r));f b')
       ∧ seteq(copath-at(regextfun(f;regextW(G;b));snd(r));regextfun(f;regextW(G;b'))))))
BY
{ ((InstLemma `copath-last_wf` [⌜Type⌝;⌜λ2T.T⌝;⌜f b⌝;⌜q1⌝]⋅ THENA Auto)
   THEN (InstLemma `copathAgree-last` [⌜Type⌝;⌜λ2T.T⌝;⌜f b⌝;⌜p1⌝;⌜q1⌝]⋅ THENA Auto)
   ) }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. ∀i:T. ∀i@0:set-dom(f i).  ∃b:T. seteq(set-item(f i;i@0);f b)
4. b : T@i
5. G : i:T ⟶ i@0:set-dom(f i) ⟶ T
6. ∀i:T. ∀i@0:set-dom(f i).  seteq(set-item(f i;i@0);f (G i i@0))
7. p1 : copath(T.T;f b)@i
8. p2 : copath(T.T;regextfun(f;regextW(G;b)))@i
9. q1 : copath(T.T;f b)@i
10. q2 : copath(T.T;regextfun(f;regextW(G;b)))@i
11. g1 : copath-length(p1) = copath-length(p2) ∈ ℤ@i
12. b' : T@i
13. g4 : seteq(copath-at(f b;p1);f b')@i
14. g5 : seteq(copath-at(regextfun(f;regextW(G;b));p2);regextfun(f;regextW(G;b')))@i
15. copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ
16. copathAgree(T.T;f b;p1;q1)
17. p2 = q2 ∈ copath(T.T;regextfun(f;regextW(G;b)))
18. copath-last(f b;q1) ∈ w':coW(Type;a.a) × coW-dom(a.a;w')
19. ((fst(copath-last(f b;q1))) = copath-at(f b;p1) ∈ coW(Type;a.a))
∧ (copath-at(f b;q1) = coW-item(copath-at(f b;p1);snd(copath-last(f b;q1))) ∈ coW(Type;a.a))
⊢ ∃r:{r:copath(T.T;f b) × copath(T.T;regextfun(f;regextW(G;b)))| 
      let u',v' = r 
      in (((copath-length(u') = (copath-length(q1) + 1) ∈ ℤ)
         ∧ copathAgree(T.T;f b;q1;u')
         ∧ (q2 = v' ∈ copath(T.T;regextfun(f;regextW(G;b)))))
         ∨ ((q1 = u' ∈ copath(T.T;f b))
           ∧ (copath-length(v') = (copath-length(q2) + 1) ∈ ℤ)
           ∧ copathAgree(T.T;regextfun(f;regextW(G;b));q2;v')))
         ∧ (copath-length(u') = copath-length(v') ∈ ℤ)} 
   ((copath-length(fst(r)) = copath-length(snd(r)) ∈ ℤ)
   ∧ (∃b':T
       (seteq(copath-at(f b;fst(r));f b')
       ∧ seteq(copath-at(regextfun(f;regextW(G;b));snd(r));regextfun(f;regextW(G;b'))))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  \mforall{}i:T.  \mforall{}i@0:set-dom(f  i).    \mexists{}b:T.  seteq(set-item(f  i;i@0);f  b)
4.  b  :  T@i
5.  G  :  i:T  {}\mrightarrow{}  i@0:set-dom(f  i)  {}\mrightarrow{}  T
6.  \mforall{}i:T.  \mforall{}i@0:set-dom(f  i).    seteq(set-item(f  i;i@0);f  (G  i  i@0))
7.  p1  :  copath(T.T;f  b)@i
8.  p2  :  copath(T.T;regextfun(f;regextW(G;b)))@i
9.  q1  :  copath(T.T;f  b)@i
10.  q2  :  copath(T.T;regextfun(f;regextW(G;b)))@i
11.  g1  :  copath-length(p1)  =  copath-length(p2)@i
12.  b'  :  T@i
13.  g4  :  seteq(copath-at(f  b;p1);f  b')@i
14.  g5  :  seteq(copath-at(regextfun(f;regextW(G;b));p2);regextfun(f;regextW(G;b')))@i
15.  copath-length(q1)  =  (copath-length(p1)  +  1)
16.  copathAgree(T.T;f  b;p1;q1)
17.  p2  =  q2
\mvdash{}  \mexists{}r:\{r:copath(T.T;f  b)  \mtimes{}  copath(T.T;regextfun(f;regextW(G;b)))| 
            let  u',v'  =  r 
            in  (((copath-length(u')  =  (copath-length(q1)  +  1))  \mwedge{}  copathAgree(T.T;f  b;q1;u')  \mwedge{}  (q2  =  v'))
                  \mvee{}  ((q1  =  u')
                      \mwedge{}  (copath-length(v')  =  (copath-length(q2)  +  1))
                      \mwedge{}  copathAgree(T.T;regextfun(f;regextW(G;b));q2;v')))
                  \mwedge{}  (copath-length(u')  =  copath-length(v'))\} 
      ((copath-length(fst(r))  =  copath-length(snd(r)))
      \mwedge{}  (\mexists{}b':T
              (seteq(copath-at(f  b;fst(r));f  b')
              \mwedge{}  seteq(copath-at(regextfun(f;regextW(G;b));snd(r));regextfun(f;regextW(G;b'))))))


By

---

Latex:
((InstLemma  `copath-last\_wf`  [\mkleeneopen{}Type\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}T.T\mkleeneclose{};\mkleeneopen{}f  b\mkleeneclose{};\mkleeneopen{}q1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `copathAgree-last`  [\mkleeneopen{}Type\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}T.T\mkleeneclose{};\mkleeneopen{}f  b\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}q1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index