---

Step * 1 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. ¬(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))
BY
{ ((InstHyp [⌜coW-item(a;t)⌝] (-4)⋅ THENA Auto) THEN D -1 THEN RenameVar `z' (-2)) }

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)
11. z : coW-dom(T.T;b)
12. coW-equiv(T.T;coW-item(a;t);coW-item(b;z))
⊢ ∃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.  \mneg{}(n  =  0)
9.  t  :  coW-dom(T.T;a)
10.  t2  :  coPath(T.T;coW-item(a;t);n  -  1)
\mvdash{}  \mexists{}p:t:coW-dom(T.T;b)  \mtimes{}  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))


By

---

Latex:
((InstHyp  [\mkleeneopen{}coW-item(a;t)\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  RenameVar  `z'  (-2))

---

Home Index