---

Step * of Lemma single-valued-bag-is-rep

∀[A:Type]. ∀[as:bag(A)].  ∀a:A. (a ↓∈ as ⇒ (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)
BY
{ (Auto
   THEN (BagToList 2 THENA Auto)
   THEN RepUR ``bag-size`` 0
   THEN (FLemma `bag-member-sq-list-member` [-1] THENA Auto)
   THEN Thin (-2)
   THEN D (-1)
   THEN (FLemma `single-valued-bag-list` [-3] THENA Auto)
   THEN Thin (-4)
   THEN SubsumeC ⌜A List⌝⋅
   THEN Auto
   THEN BLemma `list_extensionality`
   THEN Auto
   THEN Try (Complete ((Fold `bag-size` 0 THEN RWO "bag-size-rep" 0 THEN Auto)))
   THEN ((RWO "select-bag-rep" 0 THENA Auto)
         THEN Unfold `single-valued-list` (-3)
         THEN InstHyp [⌜as[i]⌝;⌜a⌝] (-3)⋅
         THEN Auto
         THEN GenListD 0)⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[as:bag(A)].
    \mforall{}a:A.  (a  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (as  =  bag-rep(\#(as);a)))  supposing  single-valued-bag(as;A)


By

---

Latex:
(Auto
  THEN  (BagToList  2  THENA  Auto)
  THEN  RepUR  ``bag-size``  0
  THEN  (FLemma  `bag-member-sq-list-member`  [-1]  THENA  Auto)
  THEN  Thin  (-2)
  THEN  D  (-1)
  THEN  (FLemma  `single-valued-bag-list`  [-3]  THENA  Auto)
  THEN  Thin  (-4)
  THEN  SubsumeC  \mkleeneopen{}A  List\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  BLemma  `list\_extensionality`
  THEN  Auto
  THEN  Try  (Complete  ((Fold  `bag-size`  0  THEN  RWO  "bag-size-rep"  0  THEN  Auto)))
  THEN  ((RWO  "select-bag-rep"  0  THENA  Auto)
              THEN  Unfold  `single-valued-list`  (-3)
              THEN  InstHyp  [\mkleeneopen{}as[i]\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (-3)\mcdot{}
              THEN  Auto
              THEN  GenListD  0)\mcdot{})

---

Home Index