---

Step * of Lemma rel_plus_strongwellfounded

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (SWellFounded(x R y) ⇒ SWellFounded(x R+ y))
BY
{ (Unfold `strongwellfounded` 0
   THEN Auto
   THEN (ParallelOp (-1))
   THEN Auto
   THEN (Unfold `rel_plus` (-1))
   THEN (Reduce (-1))
   THEN ExRepD
   THEN (MoveToConcl (-1))
   THEN (MoveToConcl (-2))
   THEN (MoveToConcl (-2))
   THEN (MoveToConcl (-1))
   THEN InductionOnNat) }

1
.....basecase..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. f : T ⟶ ℕ
4. ∀x,y:T.  ((x R y) ⇒ f x < f y)
5. n : ℕ+
⊢ ∀x,y:T.  ((x R^1 y) ⇒ f x < f y)

2
.....upcase..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. f : T ⟶ ℕ
4. ∀x,y:T.  ((x R y) ⇒ f x < f y)
5. n : ℤ
6. 0 < n
7. ∀x,y:T.  ((x R^n y) ⇒ f x < f y)
⊢ ∀x,y:T.  ((x R^n + 1 y) ⇒ f x < f y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (SWellFounded(x  R  y)  {}\mRightarrow{}  SWellFounded(x  R\msupplus{}  y))


By

---

Latex:
(Unfold  `strongwellfounded`  0
  THEN  Auto
  THEN  (ParallelOp  (-1))
  THEN  Auto
  THEN  (Unfold  `rel\_plus`  (-1))
  THEN  (Reduce  (-1))
  THEN  ExRepD
  THEN  (MoveToConcl  (-1))
  THEN  (MoveToConcl  (-2))
  THEN  (MoveToConcl  (-2))
  THEN  (MoveToConcl  (-1))
  THEN  InductionOnNat)

---

Home Index