---

Step * of Lemma sv-bag-only-combine

∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)].
  (sv-bag-only(⋃x∈b.f[x]) = sv-bag-only(f[sv-bag-only(b)]) ∈ B) supposing 
     ((∀a:A. 0 < #(f[a])) and 
     (∀a:A. single-valued-bag(f[a];B)) and 
     0 < #(b) and 
     single-valued-bag(b;A))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `bag-member-sv-bag-only` [⌜A⌝;⌜b⌝]⋅ THENA Auto)
   THEN (FLemma `bag-member-implies-hd-append` [-1] THENA Auto)
   THEN SquashExRepD
   THEN (RW (AddrC [2;1;1] (HypC (-1))) 0 THENA Auto)
   THEN Try (Complete ((BLemma `single-valued-bag-combine` THEN Auto)))
   THEN Try (Complete ((InstLemma `bag-combine-size-bound2` [⌜A⌝;⌜B⌝;⌜f⌝;⌜b⌝;⌜sv-bag-only(b)⌝]⋅
                        THEN Auto
                        THEN Assert ⌜0 < #(f[sv-bag-only(b)])⌝⋅
                        THEN Auto)))
   THEN (RWO "bag-combine-append-left" 0 THENA Auto)
   THEN Try (Complete ((BLemma `single-valued-bag-combine` THEN Auto)))
   THEN Try (Complete ((InstLemma `bag-combine-size-bound2` [⌜A⌝;⌜B⌝;⌜f⌝;⌜{sv-bag-only(b)} + c⌝;⌜sv-bag-only(b)⌝]⋅
                        THEN Auto
                        THEN Assert ⌜0 < #(f[sv-bag-only(b)])⌝⋅
                        THEN Auto)))
   THEN (RWO "bag-combine-single-left" 0 THENA Auto)) }

1
1. A : Type
2. B : Type
3. b : bag(A)
4. f : A ⟶ bag(B)
5. single-valued-bag(b;A)
6. 0 < #(b)
7. ∀a:A. single-valued-bag(f[a];B)
8. ∀a:A. 0 < #(f[a])
9. sv-bag-only(b) ↓∈ b
10. c : bag(A)
11. b = ({sv-bag-only(b)} + c) ∈ bag(A)
⊢ sv-bag-only(f[sv-bag-only(b)] + ⋃x∈c.f[x]) = sv-bag-only(f[sv-bag-only(b)]) ∈ B

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `bag-member-sv-bag-only`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `bag-member-implies-hd-append`  [-1]  THENA  Auto)
  THEN  SquashExRepD
  THEN  (RW  (AddrC  [2;1;1]  (HypC  (-1)))  0  THENA  Auto)
  THEN  Try  (Complete  ((BLemma  `single-valued-bag-combine`  THEN  Auto)))
  THEN  Try  (Complete  ((InstLemma  `bag-combine-size-bound2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}sv-bag-only(b)\mkleeneclose{}]\mcdot{}
                                            THEN  Auto
                                            THEN  Assert  \mkleeneopen{}0  <  \#(f[sv-bag-only(b)])\mkleeneclose{}\mcdot{}
                                            THEN  Auto)))
  THEN  (RWO  "bag-combine-append-left"  0  THENA  Auto)
  THEN  Try  (Complete  ((BLemma  `single-valued-bag-combine`  THEN  Auto)))
  THEN  Try  (Complete  ((InstLemma  `bag-combine-size-bound2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}\{sv-bag-only(b)\}  +  c\mkleeneclose{};
                                            \mkleeneopen{}sv-bag-only(b)\mkleeneclose{}]\mcdot{}
                                            THEN  Auto
                                            THEN  Assert  \mkleeneopen{}0  <  \#(f[sv-bag-only(b)])\mkleeneclose{}\mcdot{}
                                            THEN  Auto)))
  THEN  (RWO  "bag-combine-single-left"  0  THENA  Auto))

---

Home Index