---

Step * 1 1 of Lemma imax_ge_right


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

---

Latex:



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


By

((Unfold  `imax`  0    THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))  THEN  Auto)

---

Home Index