---

Step * of Lemma imax-list-ub

∀L:ℤ List. ∀a:ℤ.  a ≤ imax-list(L) ⇐⇒ (∃b∈L. a ≤ b) supposing 0 < ||L||
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN ((InstLemma `combine-list-rel-or` 
          [⌜ℤ⌝;⌜λ2x y.imax(x;y)⌝;⌜λ2a b.a ≤ b⌝;⌜L⌝;⌜a⌝]⋅
          THENA (Try (Complete (Auto))
                 THEN Try ((RWO "imax_ub" 0 THEN Auto))
                 THEN Auto
                 THEN D 0
                 THEN Reduce 0
                 THEN Auto
                 THEN BLemma `imax_assoc` 
                 THEN Auto)
          )
        THENM Try ((Fold `imax-list` (-1) THEN Trivial))
        )
   ) }

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List.  \mforall{}a:\mBbbZ{}.    a  \mleq{}  imax-list(L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  a  \mleq{}  b)  supposing  0  <  ||L||


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  ((InstLemma  `combine-list-rel-or` 
                [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.imax(x;y)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a  b.a  \mleq{}  b\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
                THENA  (Try  (Complete  (Auto))
                              THEN  Try  ((RWO  "imax\_ub"  0  THEN  Auto))
                              THEN  Auto
                              THEN  D  0
                              THEN  Reduce  0
                              THEN  Auto
                              THEN  BLemma  `imax\_assoc` 
                              THEN  Auto)
                )
            THENM  Try  ((Fold  `imax-list`  (-1)  THEN  Trivial))
            )
  )

---

Home Index