---

Step * of Lemma imax_add_r

∀[a,b,c:ℤ].  ((imax(a;b) + c) = imax(a + c;b + c) ∈ ℤ)
BY
{ (Unfolds ``imax`` 0
   THEN Auto
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN RepeatFor 2 (AutoSplit)
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbZ{}].    ((imax(a;b)  +  c)  =  imax(a  +  c;b  +  c))


By

---

Latex:
(Unfolds  ``imax``  0
  THEN  Auto
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Auto')

---

Home Index