---

Step * of Lemma imax-list-strict-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 (Complete ((Auto THEN D 0 THEN Reduce 0 THEN Auto THEN BLemma `imax_assoc`  THEN Auto)))
                 THEN Try ((RWO "imax_strict_ub" 0 THEN Auto)))
          )
        THENM Try ((Fold `imax-list` (-1) THEN Trivial))
        )
   ) }

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List.  \mforall{}a:\mBbbZ{}.    a  <  imax-list(L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  a  <  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  <  b\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
                THENA  (Try  (Complete  (Auto))
                              THEN  Try  (Complete  ((Auto
                                                                        THEN  D  0
                                                                        THEN  Reduce  0
                                                                        THEN  Auto
                                                                        THEN  BLemma  `imax\_assoc` 
                                                                        THEN  Auto)))
                              THEN  Try  ((RWO  "imax\_strict\_ub"  0  THEN  Auto)))
                )
            THENM  Try  ((Fold  `imax-list`  (-1)  THEN  Trivial))
            )
  )

---

Home Index