---

Step * of Lemma bag-member-parts'

∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)]. ∀[L:bag(T) List+].
    uiff(L ↓∈ bag-parts'(eq;bs;x);(¬x ↓∈ hd(L)) ∧ (∀x∈tl(L).¬(x = {} ∈ bag(T))) ∧ (bag-union(L) = bs ∈ bag(T))) 
  supposing valueall-type(T)
BY
{ ((UnivCD THENA Auto) THEN Unfold `bag-parts\'` 0 THEN AutoSplit)⋅ }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. x : T
5. bs : bag(T)
6. L : bag(T) List+
7. bs = {} ∈ bag(T)
⊢ uiff(L ↓∈ {[bs]};(¬x ↓∈ hd(L)) ∧ (∀x∈tl(L).¬(x = {} ∈ bag(T))) ∧ (bag-union(L) = bs ∈ bag(T)))

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. x : T
5. bs : bag(T)
6. ¬(bs = {} ∈ bag(T))
7. L : bag(T) List+
⊢ uiff(L ↓∈ let pts ⟵ bag-parts(eq;bs)
            in bag-map(λL.[{} / L];pts) + [L∈pts|((#x in hd(L)) =z 0)];(¬x ↓∈ hd(L))
∧ (∀x∈tl(L).¬(x = {} ∈ bag(T)))
∧ (bag-union(L) = bs ∈ bag(T)))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].  \mforall{}[L:bag(T)  List\msupplus{}].
        uiff(L  \mdownarrow{}\mmember{}  bag-parts'(eq;bs;x);(\mneg{}x  \mdownarrow{}\mmember{}  hd(L))  \mwedge{}  (\mforall{}x\mmember{}tl(L).\mneg{}(x  =  \{\}))  \mwedge{}  (bag-union(L)  =  bs)) 
    supposing  valueall-type(T)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `bag-parts\mbackslash{}'`  0  THEN  AutoSplit)\mcdot{}

---

Home Index