---

Step * of Lemma imax-bag-lb

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

---

Latex:

---

Latex:
\mforall{}[bs:bag(\mBbbZ{})].  (0  <  \#(bs)  {}\mRightarrow{}  imax-bag(bs)  \mdownarrow{}\mmember{}  bs)


By

---

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

---

Home Index