---

Step * 2 of Lemma absval-sqequal-imax


1. ∀[a:ℤ]. (imax(a;-a) ~ |a|)
⊢ ∀[a:Top]. (imax(a;-a) ~ |a|)
BY
{ SqReasoning }

1
1. ∀[a:ℤ]. (imax(a;-a) ~ |a|)
2. a : Base
3. (imax(a;-a))↓
⊢ imax(a;-a) ≤ |a|

2
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|

3
1. ∀[a:ℤ]. (imax(a;-a) ~ |a|)
2. a : Base
3. (|a|)↓
⊢ |a| ≤ imax(a;-a)

4
1. ∀[a:ℤ]. (imax(a;-a) ~ |a|)
2. a : Base
3. is-exception(if (0) < (a)  then a  else (-a))
4. (a)↓
⊢ |a| ≤ imax(a;-a)

---

Latex:

---

Latex:

1.  \mforall{}[a:\mBbbZ{}].  (imax(a;-a)  \msim{}  |a|)
\mvdash{}  \mforall{}[a:Top].  (imax(a;-a)  \msim{}  |a|)


By

---

Latex:
SqReasoning

---

Home Index