---

Step * of Lemma rmax_functionality_wrt_bdd-diff

∀[x1,x2,y1,y2:ℕ+ ⟶ ℤ].  (bdd-diff(y1;y2) ⇒ bdd-diff(x1;x2) ⇒ bdd-diff(rmax(x1;y1);rmax(x2;y2)))
BY
{ (Auto
   THEN D -2
   THEN D -1
   THEN RepUR ``rmax`` 0
   THEN With ⌜imax(B;B1)⌝ (D 0)⋅
   THEN Auto
   THEN Reduce 0
   THEN (RWO "absval-imax-difference" 0 THENA Auto)
   THEN BLemma `imax_lb` 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x1,x2,y1,y2:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].    (bdd-diff(y1;y2)  {}\mRightarrow{}  bdd-diff(x1;x2)  {}\mRightarrow{}  bdd-diff(rmax(x1;y1);rmax(x2;y2)))


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  D  -1
  THEN  RepUR  ``rmax``  0
  THEN  With  \mkleeneopen{}imax(B;B1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  (RWO  "absval-imax-difference"  0  THENA  Auto)
  THEN  BLemma  `imax\_lb` 
  THEN  Auto)

---

Home Index