---

Step * 1 2 1 2 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. p1 : coPath(a.B[a];w;n1)
9. t : coW-dom(a.B[a];w)
10. q2 : coPath(a.B[a];coW-item(w;t);n1)
11. (n1 + 1) ≤ n
12. coPathAgree(a.B[a];n1;w;p1;<t, q2>)
13. ¬((n1 + 1) = 0 ∈ ℤ)
14. ¬((n1 + 1) = 0 ∈ ℤ)
15. ¬((n1 + 1) = 1 ∈ ℤ)
⊢ ((fst(copath-last(coW-item(w;copath-hd(<n1 + 1, t, q2>));copath-tl(<n1 + 1, t, q2>)))) = coPath-at(n1;w;p1) ∈ coW(A;a.\000CB[a]))
∧ (coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;p1);snd(copath-last(coW-item(w;copath-hd(<n1 + 1, t, q2>));c\000Copath-tl(<n1 + 1, t, q2>)))) ∈ coW(A;a.B[a]))
BY
{ ((RepUR ``copath-hd copath-tl`` 0 THEN (Subst' (n1 + 1) - 1 ~ n1 0 THENA Auto))
   THEN (Assert ¬(n1 = 0 ∈ ℤ) BY
               Auto)
   THEN RepeatFor 3 (Thin (-2))) }

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. p1 : coPath(a.B[a];w;n1)
9. t : coW-dom(a.B[a];w)
10. q2 : coPath(a.B[a];coW-item(w;t);n1)
11. (n1 + 1) ≤ n
12. coPathAgree(a.B[a];n1;w;p1;<t, q2>)
13. ¬(n1 = 0 ∈ ℤ)
⊢ ((fst(copath-last(coW-item(w;t);<n1, q2>))) = coPath-at(n1;w;p1) ∈ coW(A;a.B[a]))
∧ (coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;p1);snd(copath-last(coW-item(w;t);<n1, q2>))) ∈ coW(A;a.B[a]\000C))

---

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.  p1  :  coPath(a.B[a];w;n1)
9.  t  :  coW-dom(a.B[a];w)
10.  q2  :  coPath(a.B[a];coW-item(w;t);n1)
11.  (n1  +  1)  \mleq{}  n
12.  coPathAgree(a.B[a];n1;w;p1;<t,  q2>)
13.  \mneg{}((n1  +  1)  =  0)
14.  \mneg{}((n1  +  1)  =  0)
15.  \mneg{}((n1  +  1)  =  1)
\mvdash{}  ((fst(copath-last(coW-item(w;copath-hd(<n1  +  1,  t,  q2>));copath-tl(<n1  +  1,  t,  q2>))))  =  coPath-at\000C(n1;w;p1))
\mwedge{}  (coPath-at(n1;coW-item(w;t);q2)
    =  coW-item(coPath-at(n1;w;p1);snd(copath-last(coW-item(w;copath-hd(<n1  +  1,  t,  q2>));copath-tl(<n1\000C  +  1,  t,  q2>)))))


By

---

Latex:
((RepUR  ``copath-hd  copath-tl``  0  THEN  (Subst'  (n1  +  1)  -  1  \msim{}  n1  0  THENA  Auto))
  THEN  (Assert  \mneg{}(n1  =  0)  BY
                          Auto)
  THEN  RepeatFor  3  (Thin  (-2)))

---

Home Index