---

Step * 2 1 of Lemma coPathAgree_le


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 ))
BY
{ ((D -2 THEN D -1 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  n  :  \mBbbZ{}
4.  n  \mneq{}  0
5.  [\%1]  :  0  <  n
6.  \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))))
7.  [w]  :  coW(A;a.B[a])
8.  p  :  t:coW-dom(a.B[a];w)  \mtimes{}  coPath(a.B[a];coW-item(w;t);n  -  1)
9.  q  :  t:coW-dom(a.B[a];w)  \mtimes{}  coPath(a.B[a];coW-item(w;t);n  -  1)
\mvdash{}  let  t,p'  =  p 
    in  let  t',q'  =  q 
          in  (t  =  t')  \mwedge{}  coPathAgree(a.B[a];n  -  1;coW-item(w;t);p';q')
{}\mRightarrow{}  (\mforall{}m:\mBbbN{}
            ((m  \mleq{}  n)
            {}\mRightarrow{}  if  (m  =\msubz{}  0)
                  then  True
                  else  let  t,p'  =  p 
                            in  let  t',q'  =  q 
                                  in  (t  =  t')  \mwedge{}  coPathAgree(a.B[a];m  -  1;coW-item(w;t);p';q')
                  fi  ))


By

---

Latex:
((D  -2  THEN  D  -1  THEN  Reduce  0)  THEN  Auto)

---

Home Index