---

Step * 1 2 1 2 1 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 ∈ ℤ)
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])
BY
{ (Thin (-1) THEN Unfold `copath-at` -1 THEN Reduce -1 THEN NthHypEqTrans (-1)) }

1
.....assertion..... 
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(n1 - 1;coW-item(w;t);p2) ∈ coW(A;a.B[a])
⊢ coPath-at(n1 - 1;coW-item(w;t);p2) = coPath-at(n1;w;<t1, p2>) ∈ coW(A;a.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)
15.  (fst(copath-last(coW-item(w;t);<n1,  q2>)))  =  copath-at(coW-item(w;t);<n1  -  1,  p2>)
16.  copath-at(coW-item(w;t);<n1,  q2>)  =  coW-item(copath-at(coW-item(w;t);<n1  -  1,  p2>);snd(copath-la\000Cst(coW-item(w;t);<n1,  q2>)))
\mvdash{}  (fst(copath-last(coW-item(w;t);<n1,  q2>)))  =  coPath-at(n1;w;<t1,  p2>)


By

---

Latex:
(Thin  (-1)  THEN  Unfold  `copath-at`  -1  THEN  Reduce  -1  THEN  NthHypEqTrans  (-1))

---

Home Index