---

Step * of Lemma locally-ranked-induction

∀[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)) ⇒ (∀[Q:T ⟶ ℙ]. TI(T;x,y.R[y;x];x.Q[x])))))
BY
{ (InstLemma `locally-ranked-is-well-founded` [] THEN RepeatFor 7 ((ParallelLast' THENA 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. tcWO(T;x,y.R[y;x])
⊢ ∀[Q:T ⟶ ℙ]. TI(T;x,y.R[y;x];x.Q[x])

---

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{}  (\mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  TI(T;x,y.R[y;x];x.Q[x])))))


By

---

Latex:
(InstLemma  `locally-ranked-is-well-founded`  []  THEN  RepeatFor  7  ((ParallelLast'  THENA  Auto)))

---

Home Index