---

Step * of Lemma sv-bag-only-map

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)].
  (sv-bag-only(bag-map(f;b)) = f[sv-bag-only(b)] ∈ B) supposing (0 < #(b) and single-valued-bag(b;A))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN BagToList (-1)
   THEN Auto
   THEN Try (Complete (ProveSingleVal))
   THEN Try (Complete ((RWO "bag-size-map" 0 THEN Auto)))
   THEN All (RepUR ``sv-bag-only bag-map so_apply bag-size``)⋅
   THEN RWO "hd_map" 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN AllPushDown
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[b:bag(A)].
    (sv-bag-only(bag-map(f;b))  =  f[sv-bag-only(b)])  supposing  (0  <  \#(b)  and  single-valued-bag(b;A))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  BagToList  (-1)
  THEN  Auto
  THEN  Try  (Complete  (ProveSingleVal))
  THEN  Try  (Complete  ((RWO  "bag-size-map"  0  THEN  Auto)))
  THEN  All  (RepUR  ``sv-bag-only  bag-map  so\_apply  bag-size``)\mcdot{}
  THEN  RWO  "hd\_map"  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  AllPushDown
  THEN  Auto)

---

Home Index