---

Step * of Lemma strongwellfounded_rel_exp

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[swf:SWellFounded(x R y)]. ∀[n:ℕ+]. ∀[x,y:T].
  (((fst(swf)) x) + n) ≤ ((fst(swf)) y) supposing x R^n y
BY
{ TACTIC:UniformUnivCD Auto }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[swf:SWellFounded(x  R  y)].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x,y:T].
    (((fst(swf))  x)  +  n)  \mleq{}  ((fst(swf))  y)  supposing  x  rel\_exp(T;  R;  n)  y


By

---

Latex:
TACTIC:UniformUnivCD  Auto

---

Home Index