Step * 1 of Lemma locally-ranked-induction


1. [T] Type
2. [R] T ⟶ T ⟶ ℙ
3. Trans(T;x,y.R[y;x])
4. : ℕ
5. rank T ⟶ ℕ
6. 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⌝;⌜λ2y.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