---

Step * 2 1 1 1 1 2 1 1 of Lemma bag-moebius-property


1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : bag(T)
5. ¬(b = {} ∈ bag(T))
⊢ bag-map(λ2x.snd(x);[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]) = [x∈sub-bags(eq;b)|¬b(#(x) =z #(b))] ∈ bag(bag(T))
BY
{ xxx(BLemma `bag-extensionality-no-repeats` THEN Auto)xxx }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : bag(T)
5. ¬(b = {} ∈ bag(T))
⊢ bag-no-repeats(bag(T);bag-map(λ2x.snd(x);[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]))

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : bag(T)
5. ¬(b = {} ∈ bag(T))
6. bag-no-repeats(bag(T);bag-map(λ2x.snd(x);[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]))
⊢ bag-no-repeats(bag(T);[x∈sub-bags(eq;b)|¬b(#(x) =z #(b))])

3
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : bag(T)
5. ¬(b = {} ∈ bag(T))
6. x : bag(T)
7. x ↓∈ bag-map(λ2x.snd(x);[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))])
⊢ x ↓∈ [x∈sub-bags(eq;b)|¬b(#(x) =z #(b))]

4
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : bag(T)
5. ¬(b = {} ∈ bag(T))
6. x : bag(T)
7. x ↓∈ [x∈sub-bags(eq;b)|¬b(#(x) =z #(b))]
⊢ x ↓∈ bag-map(λ2x.snd(x);[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))])

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  eq  :  EqDecider(T)
4.  b  :  bag(T)
5.  \mneg{}(b  =  \{\})
\mvdash{}  bag-map(\mlambda{}\msubtwo{}x.snd(x);[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))])
=  [x\mmember{}sub-bags(eq;b)|\mneg{}\msubb{}(\#(x)  =\msubz{}  \#(b))]


By

---

Latex:
xxx(BLemma  `bag-extensionality-no-repeats`  THEN  Auto)xxx

---

Home Index