---

Step * 2 of Lemma coPathAgree_le

.....upcase..... 
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. n : ℤ
4. [%1] : 0 < n
5. ∀[w:coW(A;a.B[a])]
     ∀p,q:coPath(a.B[a];w;n - 1).
       (coPathAgree(a.B[a];n - 1;w;p;q) ⇒ (∀m:ℕ. ((m ≤ (n - 1)) ⇒ coPathAgree(a.B[a];m;w;p;q))))
⊢ ∀[w:coW(A;a.B[a])]
    ∀p,q:coPath(a.B[a];w;n).  (coPathAgree(a.B[a];n;w;p;q) ⇒ (∀m:ℕ. ((m ≤ n) ⇒ coPathAgree(a.B[a];m;w;p;q))))
BY
{ ((Unfold `coPathAgree` 0 THEN Unfold `coPath` 0) THEN AutoSplit THEN RepeatFor 3 ((D 0 THENA Auto))) }

1
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. n : ℤ
4. n ≠ 0
5. [%1] : 0 < n
6. ∀[w:coW(A;a.B[a])]
     ∀p,q:coPath(a.B[a];w;n - 1).
       (coPathAgree(a.B[a];n - 1;w;p;q) ⇒ (∀m:ℕ. ((m ≤ (n - 1)) ⇒ coPathAgree(a.B[a];m;w;p;q))))
7. [w] : coW(A;a.B[a])
8. p : t:coW-dom(a.B[a];w) × coPath(a.B[a];coW-item(w;t);n - 1)
9. q : t:coW-dom(a.B[a];w) × coPath(a.B[a];coW-item(w;t);n - 1)
⊢ let t,p' = p 
  in let t',q' = q 
     in (t = t' ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n - 1;coW-item(w;t);p';q')
⇒ (∀m:ℕ
      ((m ≤ n)
      ⇒ if (m =z 0)
         then True
         else let t,p' = p 
              in let t',q' = q 
                 in (t = t' ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];m - 1;coW-item(w;t);p';q')
         fi ))

---

Latex:

---

Latex:
.....upcase..... 
1.  [A]  :  \mBbbU{}'
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  n  :  \mBbbZ{}
4.  [\%1]  :  0  <  n
5.  \mforall{}[w:coW(A;a.B[a])]
          \mforall{}p,q:coPath(a.B[a];w;n  -  1).
              (coPathAgree(a.B[a];n  -  1;w;p;q)  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  ((m  \mleq{}  (n  -  1))  {}\mRightarrow{}  coPathAgree(a.B[a];m;w;p;q))))
\mvdash{}  \mforall{}[w:coW(A;a.B[a])]
        \mforall{}p,q:coPath(a.B[a];w;n).
            (coPathAgree(a.B[a];n;w;p;q)  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  ((m  \mleq{}  n)  {}\mRightarrow{}  coPathAgree(a.B[a];m;w;p;q))))


By

---

Latex:
((Unfold  `coPathAgree`  0  THEN  Unfold  `coPath`  0)  THEN  AutoSplit  THEN  RepeatFor  3  ((D  0  THENA  Auto)))

---

Home Index