---

Step * of Lemma imax_strict_lb

∀[a,b,c:ℤ].  uiff(imax(a;b) < c;a < c ∧ b < c)
BY
{ (((InstLemma `imax_lb` []) THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (D 0 THENA Auto)
   THEN (InstHyp [⌜c - 1⌝] (-2))⋅
   THEN Auto
   THEN D (-3)
   THEN Auto
   THEN All (Unfold `guard`)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbZ{}].    uiff(imax(a;b)  <  c;a  <  c  \mwedge{}  b  <  c)


By

---

Latex:
(((InstLemma  `imax\_lb`  [])  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}c  -  1\mkleeneclose{}]  (-2))\mcdot{}
  THEN  Auto
  THEN  D  (-3)
  THEN  Auto
  THEN  All  (Unfold  `guard`)
  THEN  Auto)

---

Home Index