---

Step * of Lemma bag-map-union2

∀[A,B:Type]. ∀[g:A ⟶ B]. ∀[x:bag(bag(A))].  (bag-map(g;bag-union(x)) = bag-union(bag-map(λz.bag-map(g;z);x)) ∈ bag(B))
BY
{ xxx(Auto THEN (InstLemma `bag-map-union` [⌜A⌝;⌜B⌝;⌜λa.{g a}⌝;⌜x⌝]⋅ THENA Auto))xxx }

1
1. A : Type
2. B : Type
3. g : A ⟶ B
4. x : bag(bag(A))
5. bag-map(λa.{g a};bag-union(x)) = bag-union(bag-map(λb.bag-map(λa.{g a};b);x)) ∈ bag(bag(B))
⊢ bag-map(g;bag-union(x)) = bag-union(bag-map(λz.bag-map(g;z);x)) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[g:A  {}\mrightarrow{}  B].  \mforall{}[x:bag(bag(A))].
    (bag-map(g;bag-union(x))  =  bag-union(bag-map(\mlambda{}z.bag-map(g;z);x)))


By

---

Latex:
xxx(Auto  THEN  (InstLemma  `bag-map-union`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}\mlambda{}a.\{g  a\}\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))xxx

---

Home Index