---

Step * 2 2 of Lemma absval-sqequal-imax


1. ∀[a:ℤ]. (imax(a;-a) ~ |a|)
2. a : Base
3. is-exception(eval b = -a in
                if a ≤z b then b else a fi )
4. (a)↓
⊢ imax(a;-a) ≤ |a|
BY
{ (ExceptionCases (-2)
   THEN ((HasValueD (-1) THEN RWO "1" 0 THEN Auto) ORELSE (ExceptionCases (-1) THEN Try (ComputeSameException 200⋅)))
   ) }

---

Latex:

---

Latex:

1.  \mforall{}[a:\mBbbZ{}].  (imax(a;-a)  \msim{}  |a|)
2.  a  :  Base
3.  is-exception(eval  b  =  -a  in
                                if  a  \mleq{}z  b  then  b  else  a  fi  )
4.  (a)\mdownarrow{}
\mvdash{}  imax(a;-a)  \mleq{}  |a|


By

---

Latex:
(ExceptionCases  (-2)
  THEN  ((HasValueD  (-1)  THEN  RWO  "1"  0  THEN  Auto)
            ORELSE  (ExceptionCases  (-1)  THEN  Try  (ComputeSameException  200\mcdot{}))
            )
  )

---

Home Index