---

Step * of Lemma imax-bag-ub

∀[bs:bag(ℤ)]. ∀[x:ℤ].  (x ↓∈ bs ⇒ (x ≤ imax-bag(bs)))
BY
{ (Auto
   THEN Try (((BLemma `bag-size-bag-member` THENM D 0) THEN Auto THEN With ⌜x⌝ (D 0)⋅ THEN Auto))
   THEN MoveToConcl (-1)
   THEN BagToList 1
   THEN Try (Complete ((Auto THEN (BLemma `bag-size-bag-member` THENM D 0) THEN Auto THEN With ⌜x⌝ (D 0)⋅ THEN Auto)))
   THEN RepUR ``imax-bag`` 0
   THEN Auto
   THEN (BLemma `imax-list-ub`  THENA Auto)) }

1
1. bs : ℤ List
2. x : ℤ
3. x ↓∈ bs
⊢ 0 < ||bs||

2
1. bs : ℤ List
2. x : ℤ
3. x ↓∈ bs
⊢ (∃b∈bs. x ≤ b)

---

Latex:

---

Latex:
\mforall{}[bs:bag(\mBbbZ{})].  \mforall{}[x:\mBbbZ{}].    (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (x  \mleq{}  imax-bag(bs)))


By

---

Latex:
(Auto
  THEN  Try  (((BLemma  `bag-size-bag-member`  THENM  D  0)  THEN  Auto  THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  BagToList  1
  THEN  Try  (Complete  ((Auto
                                            THEN  (BLemma  `bag-size-bag-member`  THENM  D  0)
                                            THEN  Auto
                                            THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}
                                            THEN  Auto)))
  THEN  RepUR  ``imax-bag``  0
  THEN  Auto
  THEN  (BLemma  `imax-list-ub`    THENA  Auto))

---

Home Index