---

Step * 1 of Lemma strongwellfounded_rel_exp


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. swf : SWellFounded(x R y)
4. n : ℕ+
5. x : T
6. y : T
7. x R^n y
⊢ (((fst(swf)) x) + n) ≤ ((fst(swf)) y)
BY
{ (RepeatFor 4 (MoveToConcl (-1))
   THEN D -1
   THEN Reduce 0
   THEN RenameVar `%1' (-1)
   THEN InductionOnNat
   THEN RecUnfold `rel_exp` 0
   THEN Reduce 0) }

1
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)))

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. f : T ⟶ ℕ
4. ∀x,y:T.  ((x R y) ⇒ f x < f y)
5. n : ℤ@i
6. 0 < n
7. ∀x,y:T.  ((x R^n y) ⇒ (((f x) + n) ≤ (f y)))
⊢ ∀x,y:T.
    ((x if (n + 1 =z 0) then λx,y. (x = y ∈ T) else λx,y. ∃z:T. ((x R z) ∧ (z R^(n + 1) - 1 y)) fi  y)
    ⇒ (((f x) + n + 1) ≤ (f y)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  swf  :  SWellFounded(x  R  y)
4.  n  :  \mBbbN{}\msupplus{}
5.  x  :  T
6.  y  :  T
7.  x  rel\_exp(T;  R;  n)  y
\mvdash{}  (((fst(swf))  x)  +  n)  \mleq{}  ((fst(swf))  y)


By

---

Latex:
(RepeatFor  4  (MoveToConcl  (-1))
  THEN  D  -1
  THEN  Reduce  0
  THEN  RenameVar  `\%1'  (-1)
  THEN  InductionOnNat
  THEN  RecUnfold  `rel\_exp`  0
  THEN  Reduce  0)

---

Home Index