---

Step * of Lemma imax-list-strict-lb

∀[L:ℤ List]. ∀[a:ℤ].  uiff(imax-list(L) < a;(∀b∈L.b < a)) supposing 0 < ||L||
BY
{ (InstLemma `imax-list-lb` []
   THEN ParallelLast'
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstHyp [⌜a - 1⌝] (-3)⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto'
   THEN RepeatFor 2 (ParallelLast⋅)
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}[a:\mBbbZ{}].    uiff(imax-list(L)  <  a;(\mforall{}b\mmember{}L.b  <  a))  supposing  0  <  ||L||


By

---

Latex:
(InstLemma  `imax-list-lb`  []
  THEN  ParallelLast'
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}a  -  1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto'
  THEN  RepeatFor  2  (ParallelLast\mcdot{})
  THEN  Auto')

---

Home Index