---

Step * of Lemma sv-bag-only-append

∀[A:Type]. ∀[as,bs:bag(A)].
  (sv-bag-only(as + bs) = sv-bag-only(as) ∈ A) supposing 
     (similar-bags(A;as;bs) and 
     0 < #(as) and 
     single-valued-bag(as;A) and 
     single-valued-bag(bs;A))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `bag_to_squash_list` [⌜A⌝;⌜as⌝]⋅ THENA Auto)
   THEN (SquashExRepD THENA Auto)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN (RWO "-3" 0 THENA Auto)
   THEN Try (Complete ((RWO "bag-size-append" 0 THEN Auto')))
   THEN Try (Complete ((BLemma `single-valued-bag-append` THEN Auto)))
   THEN ThinVar `as'
   THEN (UnivCD THENA Auto)
   THEN RepUR ``sv-bag-only bag-append`` 0
   THEN RWO "hd-append-sq" 0
   THEN Auto
   THEN RepUR ``bag-size`` (-2)
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN AllPushDown
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[as,bs:bag(A)].
    (sv-bag-only(as  +  bs)  =  sv-bag-only(as))  supposing 
          (similar-bags(A;as;bs)  and 
          0  <  \#(as)  and 
          single-valued-bag(as;A)  and 
          single-valued-bag(bs;A))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `bag\_to\_squash\_list`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (SquashExRepD  THENA  Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  Try  (Complete  ((RWO  "bag-size-append"  0  THEN  Auto')))
  THEN  Try  (Complete  ((BLemma  `single-valued-bag-append`  THEN  Auto)))
  THEN  ThinVar  `as'
  THEN  (UnivCD  THENA  Auto)
  THEN  RepUR  ``sv-bag-only  bag-append``  0
  THEN  RWO  "hd-append-sq"  0
  THEN  Auto
  THEN  RepUR  ``bag-size``  (-2)
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  AllPushDown
  THEN  Auto)

---

Home Index