---

Step * 3 of Lemma bag-monad_wf


1. T : Type
2. S : Type
3. U : Type
4. m : (λT.bag(T)) T
5. f : T ⟶ ((λT.bag(T)) S)
6. g : S ⟶ ((λT.bag(T)) U)
⊢ ((λba,f. ⋃x∈ba.f x) ((λba,f. ⋃x∈ba.f x) m f) g) = ((λba,f. ⋃x∈ba.f x) m (λx.((λba,f. ⋃x∈ba.f x) (f x) g))) ∈ ((λT.bag(\000CT)) U)
BY
{ All Reduce THEN InstLemma `bag-combine-combine` [⌜T⌝;⌜S⌝;⌜U⌝;⌜m⌝;⌜f⌝;⌜g⌝] THEN Auto⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  U  :  Type
4.  m  :  (\mlambda{}T.bag(T))  T
5.  f  :  T  {}\mrightarrow{}  ((\mlambda{}T.bag(T))  S)
6.  g  :  S  {}\mrightarrow{}  ((\mlambda{}T.bag(T))  U)
\mvdash{}  ((\mlambda{}ba,f.  \mcup{}x\mmember{}ba.f  x)  ((\mlambda{}ba,f.  \mcup{}x\mmember{}ba.f  x)  m  f)  g)  =  ((\mlambda{}ba,f.  \mcup{}x\mmember{}ba.f  x)  m  (\mlambda{}x.((\mlambda{}ba,f.  \mcup{}x\mmember{}ba.f  x)  (f\000C  x)  g)))


By

---

Latex:
All  Reduce  THEN  InstLemma  `bag-combine-combine`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]  THEN  Auto\mcdot{}

---

Home Index