---

Step * of Lemma strongwf-implies

∀[T:Type]. ∀[R:T ⟶ T ⟶ Type].  (SWellFounded(R[x;y]) ⇒ WellFnd{i}(T;x,y.R[x;y]))
BY
{ (Unfolds ``wellfounded strongwellfounded`` 0 THEN Auto THEN ExRepD) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ Type
3. f : T ⟶ ℕ
4. ∀x,y:T.  (R[x;y] ⇒ f x < f y)
5. [P] : T ⟶ ℙ
6. ∀j:T. ((∀k:T. (R[k;j] ⇒ P[k])) ⇒ P[j])
⊢ ∀n:T. P[n]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  Type].    (SWellFounded(R[x;y])  {}\mRightarrow{}  WellFnd\{i\}(T;x,y.R[x;y]))


By

---

Latex:
(Unfolds  ``wellfounded  strongwellfounded``  0  THEN  Auto  THEN  ExRepD)

---

Home Index