---

Step * 1 2 1 2 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. 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))
BY
{ (Unfold `coPath` -6
   THEN (SplitOnHypITE -6  THENA Auto)
   THEN Try (Trivial)
   THEN Thin (-1)
   THEN D -6
   THEN Unfold `coPathAgree` -2
   THEN (SplitOnHypITE -2  THENA Auto)
   THEN (Trivial ORELSE Thin (-1))
   THEN Reduce -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. 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]))

---

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  =  0)
\mvdash{}  ((fst(copath-last(coW-item(w;t);<n1,  q2>)))  =  coPath-at(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;t);<n1,  q2>))))


By

---

Latex:
(Unfold  `coPath`  -6
  THEN  (SplitOnHypITE  -6    THENA  Auto)
  THEN  Try  (Trivial)
  THEN  Thin  (-1)
  THEN  D  -6
  THEN  Unfold  `coPathAgree`  -2
  THEN  (SplitOnHypITE  -2    THENA  Auto)
  THEN  (Trivial  ORELSE  Thin  (-1))
  THEN  Reduce  -2)

---

Home Index