---

Step * of Lemma locally-ranked-is-well-founded

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Trans(T;x,y.R[y;x])
  ⇒ (∀k:ℕ. ∀rank:T ⟶ ℕ. ∀l:T ⟶ ℕk.
        ((∀x,y:T.  (((l x) = (l y) ∈ ℤ) ⇒ R[x;y] ⇒ rank x < rank y)) ⇒ tcWO(T;x,y.R[y;x]))))
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.R[y;x])
4. k : ℕ
5. rank : T ⟶ ℕ
6. l : T ⟶ ℕk
7. ∀x,y:T.  (((l x) = (l y) ∈ ℤ) ⇒ R[x;y] ⇒ rank x < rank y)
8. f : ℕ ⟶ T
⊢ ↓∃i,j:ℕ. (i < j ∧ (¬R[f j;f i]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T;x,y.R[y;x])
    {}\mRightarrow{}  (\mforall{}k:\mBbbN{}.  \mforall{}rank:T  {}\mrightarrow{}  \mBbbN{}.  \mforall{}l:T  {}\mrightarrow{}  \mBbbN{}k.
                ((\mforall{}x,y:T.    (((l  x)  =  (l  y))  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  rank  x  <  rank  y))  {}\mRightarrow{}  tcWO(T;x,y.R[y;x]))))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index