---

Step * of Lemma cWO-rel-path-barred

∀[T:Type]
  ∀[R:T ⟶ T ⟶ ℙ]
    (∀f:ℕ ⟶ T. (↓∃m:ℕ. ∃n:ℕm. (¬R[f n;f m])))
    ⇒ (∀alpha:{f:ℕ ⟶ (T?)| ∀x:ℕ. (cWO-rel(R) x f (f x))} . (↓∃m:ℕ. (cWObar() m alpha))) 
    supposing ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c]) 
  supposing T
BY
{ TACTIC:(Auto THEN All (RepUR ``cWO-rel cWObar``)) }

1
1. T : Type
2. T
3. R : T ⟶ T ⟶ ℙ
4. ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
5. ∀f:ℕ ⟶ T. (↓∃m:ℕ. ∃n:ℕm. (¬R[f n;f m]))
6. alpha : {f:ℕ ⟶ (T?)| ∀x:ℕ. ((0 < x ∧ (↑isl(f x))) ⇒ ((↑isl(f (x - 1))) ∧ (R outl(f (x - 1)) outl(f x))))} @i
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
        (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}m.  (\mneg{}R[f  n;f  m])))
        {}\mRightarrow{}  (\mforall{}alpha:\{f:\mBbbN{}  {}\mrightarrow{}  (T?)|  \mforall{}x:\mBbbN{}.  (cWO-rel(R)  x  f  (f  x))\}  .  (\mdownarrow{}\mexists{}m:\mBbbN{}.  (cWObar()  m  alpha))) 
        supposing  \mforall{}a,b,c:T.    (R[a;b]  {}\mRightarrow{}  R[b;c]  {}\mRightarrow{}  R[a;c]) 
    supposing  T


By

---

Latex:
TACTIC:(Auto  THEN  All  (RepUR  ``cWO-rel  cWObar``))

---

Home Index