---

Step * 1 of Lemma locally-ranked-induction


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])
BY
{ (InstLemma `tcWO-induction` [⌜T⌝;⌜λ2x y.R[y;x]⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  Trans(T;x,y.R[y;x])
4.  k  :  \mBbbN{}
5.  rank  :  T  {}\mrightarrow{}  \mBbbN{}
6.  l  :  T  {}\mrightarrow{}  \mBbbN{}k
7.  \mforall{}x,y:T.    (((l  x)  =  (l  y))  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  rank  x  <  rank  y)
8.  tcWO(T;x,y.R[y;x])
\mvdash{}  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  TI(T;x,y.R[y;x];x.Q[x])


By

---

Latex:
(InstLemma  `tcWO-induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.R[y;x]\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index