---

Step * of Lemma bag-combine-eq-out

∀[A,B,C:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[f:A ⟶ bag(C)]. ∀[g:B ⟶ bag(C)]. ∀[h:A ⟶ B].
  (⋃a∈as.f[a] = ⋃b∈bs.g[b] ∈ bag(C)) supposing 
     ((∀a:A. (a ↓∈ as ⇒ (g[h[a]] = f[a] ∈ bag(C)))) and 
     (bs = bag-map(h;as) ∈ bag(B)))
BY
{ ((UnivCD THENA Auto)
   THEN (HypSubst' (-2) 0 THENA Auto)
   THEN (RWO "bag-combine-map" 0 THENA Auto)
   THEN Using [`A',⌜{a:A| a ↓∈ as} ⌝] MemCD⋅
   THEN Auto
   THEN Try (Complete ((BLemma `bag-subtype` THEN Auto)))
   THEN D (-1)
   THEN Symmetry
   THEN BHyp (-3) 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].  \mforall{}[f:A  {}\mrightarrow{}  bag(C)].  \mforall{}[g:B  {}\mrightarrow{}  bag(C)].  \mforall{}[h:A  {}\mrightarrow{}  B].
    (\mcup{}a\mmember{}as.f[a]  =  \mcup{}b\mmember{}bs.g[b])  supposing 
          ((\mforall{}a:A.  (a  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (g[h[a]]  =  f[a])))  and 
          (bs  =  bag-map(h;as)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (HypSubst'  (-2)  0  THENA  Auto)
  THEN  (RWO  "bag-combine-map"  0  THENA  Auto)
  THEN  Using  [`A',\mkleeneopen{}\{a:A|  a  \mdownarrow{}\mmember{}  as\}  \mkleeneclose{}]  MemCD\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `bag-subtype`  THEN  Auto)))
  THEN  D  (-1)
  THEN  Symmetry
  THEN  BHyp  (-3) 
  THEN  Auto)

---

Home Index