---

Step * 1 of Lemma imax-list-lb


1. Assoc(ℤ;λx,y. imax(x;y))
⊢ ∀[L:ℤ List]. ∀[a:ℤ].  uiff(imax-list(L) ≤ a;(∀b∈L.b ≤ a)) supposing 0 < ||L||
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN ((InstLemma `combine-list-rel-and` 
          [⌜ℤ⌝;⌜λ2x y.imax(x;y)⌝;⌜λ2a b.b ≤ a⌝;⌜L⌝;⌜a⌝]⋅
          THENA (Try (Complete (Auto)) THEN (RWO "imax_lb" 0 THEN Auto) THEN All (Unfold `guard`) THEN Auto)
          )
        THENM (Fold `imax-list` (-1) THEN Auto)
        )
   ) }

---

Latex:

---

Latex:

1.  Assoc(\mBbbZ{};\mlambda{}x,y.  imax(x;y))
\mvdash{}  \mforall{}[L:\mBbbZ{}  List].  \mforall{}[a:\mBbbZ{}].    uiff(imax-list(L)  \mleq{}  a;(\mforall{}b\mmember{}L.b  \mleq{}  a))  supposing  0  <  ||L||


By

---

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

---

Home Index