---

Step * 1 of Lemma reg-seq-mul_wf2

.....equality..... 
1. x : ℝ
2. y : ℝ
⊢ imax(|x 1|;|y 1|) + 4 ~ imax(canon-bnd(x);canon-bnd(y)) + 1
BY
{ (Unfold `canon-bnd` 0 THEN RWO  "imax_unfold" 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
\mvdash{}  imax(|x  1|;|y  1|)  +  4  \msim{}  imax(canon-bnd(x);canon-bnd(y))  +  1


By

---

Latex:
(Unfold  `canon-bnd`  0  THEN  RWO    "imax\_unfold"  0  THEN  Auto)

---

Home Index