---

Step * of Lemma bag-split

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(T)].  (as = ([x∈as|p[x]] + [x∈as|¬bp[x]]) ∈ bag(T))
BY
{ (Auto THEN D -1 THEN Auto THEN Subst ⌜a1 = a2 ∈ bag(T)⌝ 0⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[as:bag(T)].    (as  =  ([x\mmember{}as|p[x]]  +  [x\mmember{}as|\mneg{}\msubb{}p[x]]))


By

---

Latex:
(Auto  THEN  D  -1  THEN  Auto  THEN  Subst  \mkleeneopen{}a1  =  a2\mkleeneclose{}  0\mcdot{})

---

Home Index