---

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

.....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])
BY
{ (RW (AddrC [3] UnfoldTopAbC) 0 THEN SplitOnConclITE THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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(n1  -  1;coW-item(w;t);p2)
\mvdash{}  coPath-at(n1  -  1;coW-item(w;t);p2)  =  coPath-at(n1;w;<t1,  p2>)


By

---

Latex:
(RW  (AddrC  [3]  UnfoldTopAbC)  0  THEN  SplitOnConclITE  THEN  Reduce  0  THEN  Auto)

---

Home Index