---

Step * 1 of Lemma radd-rmax


1. x : ℝ
2. y : ℝ
3. z : ℝ
⊢ bdd-diff(λn.((x n) + (rmax(y;z) n));rmax(λn.((x n) + (y n));λn.((x n) + (z n))))
BY
{ (RepUR ``rmax`` 0 THEN BLemma `trivial-bdd-diff` THEN Auto THEN Reduce 0) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. n : ℕ+
⊢ ((x n) + imax(y n;z n)) = imax((x n) + (y n);(x n) + (z n)) ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  z  :  \mBbbR{}
\mvdash{}  bdd-diff(\mlambda{}n.((x  n)  +  (rmax(y;z)  n));rmax(\mlambda{}n.((x  n)  +  (y  n));\mlambda{}n.((x  n)  +  (z  n))))


By

---

Latex:
(RepUR  ``rmax``  0  THEN  BLemma  `trivial-bdd-diff`  THEN  Auto  THEN  Reduce  0)

---

Home Index