---

Step * 1 2 1 2 1 1 of Lemma copathAgree-last


1. n1 : ℕ
2. A : 𝕌'
3. B : A ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
     (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
        ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
        ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
        copathAgree(a.B[a];w;p;q) and 
        (copath-length(q) ≤ (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) ≤ n
13. (t1 = t ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
14. ¬(n1 = 0 ∈ ℤ)
⊢ ((fst(copath-last(coW-item(w;t);<n1, q2>))) = coPath-at(n1;w;<t1, p2>) ∈ coW(A;a.B[a]))
∧ (coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;<t1, p2>);snd(copath-last(coW-item(w;t);<n1, q2>))) ∈ coW(A;\000Ca.B[a]))
BY
{ ((InstHyp [⌜coW-item(w;t)⌝;⌜<n1 - 1, p2>⌝;⌜<n1, q2>⌝] 6⋅
    THENA (Auto
           THEN RepUR ``copath-length`` 0
           THEN Auto
           THEN RepUR ``copathAgree`` 0
           THEN LessCases 0
           THEN Auto
           THEN NthHypEq (-3)
           THEN EqCD
           THEN Auto)
    )
   THEN D -1
   THEN D 0) }

1
1. n1 : ℕ
2. A : 𝕌'
3. B : A ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
     (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
        ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
        ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
        copathAgree(a.B[a];w;p;q) and 
        (copath-length(q) ≤ (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) ≤ n
13. (t1 = t ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
14. ¬(n1 = 0 ∈ ℤ)
15. (fst(copath-last(coW-item(w;t);<n1, q2>))) = copath-at(coW-item(w;t);<n1 - 1, p2>) ∈ coW(A;a.B[a])
16. copath-at(coW-item(w;t);<n1, q2>) = coW-item(copath-at(coW-item(w;t);<n1 - 1, p2>);snd(copath-last(coW-item(w;t);<n1\000C, q2>))) ∈ coW(A;a.B[a])
⊢ (fst(copath-last(coW-item(w;t);<n1, q2>))) = coPath-at(n1;w;<t1, p2>) ∈ coW(A;a.B[a])

2
1. n1 : ℕ
2. A : 𝕌'
3. B : A ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
     (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
        ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
        ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
        copathAgree(a.B[a];w;p;q) and 
        (copath-length(q) ≤ (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) ≤ n
13. (t1 = t ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
14. ¬(n1 = 0 ∈ ℤ)
15. (fst(copath-last(coW-item(w;t);<n1, q2>))) = copath-at(coW-item(w;t);<n1 - 1, p2>) ∈ coW(A;a.B[a])
16. copath-at(coW-item(w;t);<n1, q2>) = coW-item(copath-at(coW-item(w;t);<n1 - 1, p2>);snd(copath-last(coW-item(w;t);<n1\000C, q2>))) ∈ coW(A;a.B[a])
⊢ coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;<t1, p2>);snd(copath-last(coW-item(w;t);<n1, q2>))) ∈ coW(A;a\000C.B[a])

---

Latex:

---

Latex:

1.  n1  :  \mBbbN{}
2.  A  :  \mBbbU{}'
3.  B  :  A  {}\mrightarrow{}  Type
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p,q:copath(a.B[a];w)].
          (((fst(copath-last(w;q)))  =  copath-at(w;p))
                \mwedge{}  (copath-at(w;q)  =  coW-item(copath-at(w;p);snd(copath-last(w;q)))))  supposing 
                ((copath-length(q)  =  (copath-length(p)  +  1))  and 
                copathAgree(a.B[a];w;p;q)  and 
                (copath-length(q)  \mleq{}  (n  -  1)))
7.  w  :  coW(A;a.B[a])
8.  t1  :  coW-dom(a.B[a];w)
9.  p2  :  coPath(a.B[a];coW-item(w;t1);n1  -  1)
10.  t  :  coW-dom(a.B[a];w)
11.  q2  :  coPath(a.B[a];coW-item(w;t);n1)
12.  (n1  +  1)  \mleq{}  n
13.  (t1  =  t)  \mwedge{}  coPathAgree(a.B[a];n1  -  1;coW-item(w;t1);p2;q2)
14.  \mneg{}(n1  =  0)
\mvdash{}  ((fst(copath-last(coW-item(w;t);<n1,  q2>)))  =  coPath-at(n1;w;<t1,  p2>))
\mwedge{}  (coPath-at(n1;coW-item(w;t);q2)  =  coW-item(coPath-at(n1;w;<t1,  p2>);snd(copath-last(coW-item(w;t);\000C<n1,  q2>))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}coW-item(w;t)\mkleeneclose{};\mkleeneopen{}<n1  -  1,  p2>\mkleeneclose{};\mkleeneopen{}<n1,  q2>\mkleeneclose{}]  6\mcdot{}
    THENA  (Auto
                  THEN  RepUR  ``copath-length``  0
                  THEN  Auto
                  THEN  RepUR  ``copathAgree``  0
                  THEN  LessCases  0
                  THEN  Auto
                  THEN  NthHypEq  (-3)
                  THEN  EqCD
                  THEN  Auto)
    )
  THEN  D  -1
  THEN  D  0)

---

Home Index