---

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


1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : T List
5. ¬(b = {} ∈ bag(T))
6. Comm(ℤ;λx,y. (x + y)) ∧ IsMonoid(ℤ;λx,y. (x + y);0)
7. ||b|| ≥ 1 
8. Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). -bag-moebius(eq;x)
= (-Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). bag-moebius(eq;x))
∈ ℤ
⊢ ((Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|0 <z (#hd(b) in x)]). bag-moebius(eq;x)
+ Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). bag-moebius(eq;x))
+ 0)
= 0
∈ ℤ
BY
{ Subst' Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|0 <z (#hd(b) in x)]). bag-moebius(eq;x)
= Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). -bag-moebius(eq;x)
∈ ℤ 0 }

1
.....equality..... 
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : T List
5. ¬(b = {} ∈ bag(T))
6. Comm(ℤ;λx,y. (x + y)) ∧ IsMonoid(ℤ;λx,y. (x + y);0)
7. ||b|| ≥ 1 
8. Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). -bag-moebius(eq;x)
= (-Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). bag-moebius(eq;x))
∈ ℤ
⊢ Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|0 <z (#hd(b) in x)]). bag-moebius(eq;x)
= Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). -bag-moebius(eq;x)
∈ ℤ

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : T List
5. ¬(b = {} ∈ bag(T))
6. Comm(ℤ;λx,y. (x + y)) ∧ IsMonoid(ℤ;λx,y. (x + y);0)
7. ||b|| ≥ 1 
8. Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). -bag-moebius(eq;x)
= (-Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). bag-moebius(eq;x))
∈ ℤ
⊢ ((Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). -bag-moebius(eq;x)
+ Σ(x∈[x∈[x∈sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|¬b0 <z (#hd(b) in x)]). bag-moebius(eq;x))
+ 0)
= 0
∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  eq  :  EqDecider(T)
4.  b  :  T  List
5.  \mneg{}(b  =  \{\})
6.  Comm(\mBbbZ{};\mlambda{}x,y.  (x  +  y))  \mwedge{}  IsMonoid(\mBbbZ{};\mlambda{}x,y.  (x  +  y);0)
7.  ||b||  \mgeq{}  1 
8.  \mSigma{}(x\mmember{}[x\mmember{}[x\mmember{}sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|\mneg{}\msubb{}0  <z  (\#hd(b)  in  x)]).  -bag-moebius(eq;x)
=  (-\mSigma{}(x\mmember{}[x\mmember{}[x\mmember{}sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|\mneg{}\msubb{}0  <z  (\#hd(b)  in  x)]).  bag-moebius(eq;x))
\mvdash{}  ((\mSigma{}(x\mmember{}[x\mmember{}[x\mmember{}sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|0  <z  (\#hd(b)  in  x)]).  bag-moebius(eq;x)
+  \mSigma{}(x\mmember{}[x\mmember{}[x\mmember{}sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|\mneg{}\msubb{}0  <z  (\#hd(b)  in  x)]).  bag-moebius(eq;x))
+  0)
=  0


By

---

Latex:
Subst'  \mSigma{}(x\mmember{}[x\mmember{}[x\mmember{}sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|0  <z  (\#hd(b)  in  x)]).  bag-moebius(eq;x)
=  \mSigma{}(x\mmember{}[x\mmember{}[x\mmember{}sub-bags(eq;b)|bag-has-no-repeats(eq;x)]|\mneg{}\msubb{}0  <z  (\#hd(b)  in  x)]).  -bag-moebius(eq;x)  0

---

Home Index