---

Step * 1 2 of Lemma imax_ge_left


1. a : @i
2. b : @i
3. (a  b)
 imax(a;b)  a 
BY
{ ((Unfold `imax` 0  THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) THEN Auto) }

---

Latex:



1.  a  :  \mBbbZ{}@i
2.  b  :  \mBbbZ{}@i
3.  \mneg{}(a  \mleq{}  b)
\mvdash{}  imax(a;b)  \mgeq{}  a 


By

((Unfold  `imax`  0    THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))  THEN  Auto)\mcdot{}

---

Home Index