---

Step * 1 1 1 1 1 of Lemma cosetTC_functionality_subset


1. n : ℤ
2. [%1] : 0 < n
3. 0 < n - 1
⇒ (∀a,b:coW(Type;x.x).
      ((∀x:coW(Type;x.x). (coWmem(T.T;x;a) ⇒ coWmem(T.T;x;b)))
      ⇒ (∀t1:coPath(T.T;a;n - 1). ∃p:coPath(T.T;b;n - 1). coW-equiv(T.T;coPath-at(n - 1;a;t1);coPath-at(n - 1;b;p)))))
4. 0 < n
5. a : coW(Type;x.x)
6. b : coW(Type;x.x)
7. ∀x:coW(Type;x.x). (coWmem(T.T;x;a) ⇒ coWmem(T.T;x;b))
8. t1 : coPath(T.T;a;n)
⊢ ∃p:coPath(T.T;b;n). coW-equiv(T.T;coPath-at(n;a;t1);coPath-at(n;b;p))
BY
{ (MoveToConcl (-1)
   THEN Unfold `coPath-at` 0
   THEN Unfold `coPath` 0
   THEN SplitOnConclITE
   THEN Auto
   THEN D -1
   THEN Reduce 0) }

1
1. n : ℤ
2. [%1] : 0 < n
3. 0 < n - 1
⇒ (∀a,b:coW(Type;x.x).
      ((∀x:coW(Type;x.x). (coWmem(T.T;x;a) ⇒ coWmem(T.T;x;b)))
      ⇒ (∀t1:coPath(T.T;a;n - 1). ∃p:coPath(T.T;b;n - 1). coW-equiv(T.T;coPath-at(n - 1;a;t1);coPath-at(n - 1;b;p)))))
4. 0 < n
5. a : coW(Type;x.x)
6. b : coW(Type;x.x)
7. ∀x:coW(Type;x.x). (coWmem(T.T;x;a) ⇒ coWmem(T.T;x;b))
8. ¬(n = 0 ∈ ℤ)
9. t : coW-dom(T.T;a)
10. t2 : coPath(T.T;coW-item(a;t);n - 1)
⊢ ∃p:t:coW-dom(T.T;b) × coPath(T.T;coW-item(b;t);n - 1)
   coW-equiv(T.T;coPath-at(n - 1;coW-item(a;t);t2);let t,q = p 
                                                   in coPath-at(n - 1;coW-item(b;t);q))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  [\%1]  :  0  <  n
3.  0  <  n  -  1
{}\mRightarrow{}  (\mforall{}a,b:coW(Type;x.x).
            ((\mforall{}x:coW(Type;x.x).  (coWmem(T.T;x;a)  {}\mRightarrow{}  coWmem(T.T;x;b)))
            {}\mRightarrow{}  (\mforall{}t1:coPath(T.T;a;n  -  1)
                        \mexists{}p:coPath(T.T;b;n  -  1).  coW-equiv(T.T;coPath-at(n  -  1;a;t1);coPath-at(n  -  1;b;p)))))
4.  0  <  n
5.  a  :  coW(Type;x.x)
6.  b  :  coW(Type;x.x)
7.  \mforall{}x:coW(Type;x.x).  (coWmem(T.T;x;a)  {}\mRightarrow{}  coWmem(T.T;x;b))
8.  t1  :  coPath(T.T;a;n)
\mvdash{}  \mexists{}p:coPath(T.T;b;n).  coW-equiv(T.T;coPath-at(n;a;t1);coPath-at(n;b;p))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  Unfold  `coPath-at`  0
  THEN  Unfold  `coPath`  0
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index