---

Step * 1 1 of Lemma strongwellfounded_rel_exp


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. f : T ⟶ ℕ
4. ∀x,y:T.  ((x R y) ⇒ f x < f y)
5. n : ℕ+@i
⊢ ∀x,y:T.  ((∃z:T. ((x R z) ∧ (z R^0 y))) ⇒ (((f x) + 1) ≤ (f y)))
BY
{ (RecUnfold `rel_exp` 0
   THEN Reduce 0
   THEN Auto
   THEN ExRepD
   THEN InstHyp [⌜x⌝;⌜z⌝] 4⋅
   THEN Auto
   THEN HypSubst' (-2) (-1)
   THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  f  :  T  {}\mrightarrow{}  \mBbbN{}
4.  \mforall{}x,y:T.    ((x  R  y)  {}\mRightarrow{}  f  x  <  f  y)
5.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  \mforall{}x,y:T.    ((\mexists{}z:T.  ((x  R  z)  \mwedge{}  (z  rel\_exp(T;  R;  0)  y)))  {}\mRightarrow{}  (((f  x)  +  1)  \mleq{}  (f  y)))


By

---

Latex:
(RecUnfold  `rel\_exp`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  4\mcdot{}
  THEN  Auto
  THEN  HypSubst'  (-2)  (-1)
  THEN  Auto')\mcdot{}

---

Home Index