---

Step * 1 2 of Lemma copathAgree-last


1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ
4. 0 < n
5. ∀[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)))
6. [w] : coW(A;a.B[a])
7. [p] : copath(a.B[a];w)
8. [q] : copath(a.B[a];w)
9. [%2] : copath-length(q) ≤ n
10. [%3] : copathAgree(a.B[a];w;p;q)
11. [%4] : copath-length(q) = (copath-length(p) + 1) ∈ ℤ
⊢ ((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]))
BY
{ ((Unhide THENA Auto)
   THEN DVar `p'
   THEN DVar `q'
   THEN RepUR ``copathAgree`` -2
   THEN RepUR ``copath-length`` -3
   THEN RepUR ``copath-length`` -1
   THEN Eliminate ⌜n2⌝⋅
   THEN ThinVar `n2'
   THEN (LessCases (-1) THENA Auto)
   THEN ((D -1 THEN Auto) ORELSE Thin (-1))) }

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. q1 : coPath(a.B[a];w;n1 + 1)
10. (n1 + 1) ≤ n
11. coPathAgree(a.B[a];n1;w;p1;q1)
⊢ ((fst(copath-last(w;<n1 + 1, q1>))) = copath-at(w;<n1, p1>) ∈ coW(A;a.B[a])) ∧ (copath-at(w;<n1 + 1, q1>) = coW-item(c\000Copath-at(w;<n1, p1>);snd(copath-last(w;<n1 + 1, q1>))) ∈ coW(A;a.B[a]))

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \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)))
6.  [w]  :  coW(A;a.B[a])
7.  [p]  :  copath(a.B[a];w)
8.  [q]  :  copath(a.B[a];w)
9.  [\%2]  :  copath-length(q)  \mleq{}  n
10.  [\%3]  :  copathAgree(a.B[a];w;p;q)
11.  [\%4]  :  copath-length(q)  =  (copath-length(p)  +  1)
\mvdash{}  ((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))))


By

---

Latex:
((Unhide  THENA  Auto)
  THEN  DVar  `p'
  THEN  DVar  `q'
  THEN  RepUR  ``copathAgree``  -2
  THEN  RepUR  ``copath-length``  -3
  THEN  RepUR  ``copath-length``  -1
  THEN  Eliminate  \mkleeneopen{}n2\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `n2'
  THEN  (LessCases  (-1)  THENA  Auto)
  THEN  ((D  -1  THEN  Auto)  ORELSE  Thin  (-1)))

---

Home Index