---

Step * 1 of Lemma absval-sqequal-imax


1. a : ℤ
⊢ imax(a;-a) = |a| ∈ ℤ
BY
{ (RepUR ``imax absval`` 0 THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto)) THEN Repeat (AutoSplit) THEN Auto') }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
\mvdash{}  imax(a;-a)  =  |a|


By

---

Latex:
(RepUR  ``imax  absval``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto))
  THEN  Repeat  (AutoSplit)
  THEN  Auto')

---

Home Index