Step
*
1
1
1
2
1
1
1
of Lemma
fps-moebius-eq
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℤ
6. 0 < n
7. ∀b:bag(X). (#(b) < n - 1 ⇒ (fps-div-coeff(eq;r;1;λb.1;1;b) = int-to-ring(r;bag-moebius(eq;b)) ∈ |r|))
8. b : bag(X)
9. ¬(b = {} ∈ bag(X))
10. #(b) < n
11. Assoc(ℤ;λx,y. (x + y))
12. Comm(ℤ;λx,y. (x + y))
13. bag-moebius(eq;b) = (-Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(p))) ∈ ℤ
14. Σ(x∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). int-to-ring(r;bag-moebius(eq;snd(x)))
= int-to-ring(r;Σ(x∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(x)))
∈ |r|
⊢ Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))])
fps-div-coeff(eq;r;λb.if bag-null(b) then 1 else 0 fi ;λb.1;1;snd(p))
= Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). int-to-ring(r;bag-moebius(eq;snd(p)))
∈ |r|
BY
{ TACTIC:(GenConcl ⌜[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))] = bb ∈ bag({p:bag(X) × bag(X)| #(snd(p)) < n - 1} )⌝⋅
THENA Auto
) }
1
.....wf.....
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℤ
6. 0 < n
7. ∀b:bag(X). (#(b) < n - 1 ⇒ (fps-div-coeff(eq;r;1;λb.1;1;b) = int-to-ring(r;bag-moebius(eq;b)) ∈ |r|))
8. b : bag(X)
9. ¬(b = {} ∈ bag(X))
10. #(b) < n
11. Assoc(ℤ;λx,y. (x + y))
12. Comm(ℤ;λx,y. (x + y))
13. bag-moebius(eq;b) = (-Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(p))) ∈ ℤ
14. Σ(x∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). int-to-ring(r;bag-moebius(eq;snd(x)))
= int-to-ring(r;Σ(x∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(x)))
∈ |r|
⊢ [p∈bag-partitions(eq;b)|¬bbag-null(fst(p))] ∈ bag({p:bag(X) × bag(X)| #(snd(p)) < n - 1} )
2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℤ
6. 0 < n
7. ∀b:bag(X). (#(b) < n - 1 ⇒ (fps-div-coeff(eq;r;1;λb.1;1;b) = int-to-ring(r;bag-moebius(eq;b)) ∈ |r|))
8. b : bag(X)
9. ¬(b = {} ∈ bag(X))
10. #(b) < n
11. Assoc(ℤ;λx,y. (x + y))
12. Comm(ℤ;λx,y. (x + y))
13. bag-moebius(eq;b) = (-Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(p))) ∈ ℤ
14. Σ(x∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). int-to-ring(r;bag-moebius(eq;snd(x)))
= int-to-ring(r;Σ(x∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(x)))
∈ |r|
15. bb : bag({p:bag(X) × bag(X)| #(snd(p)) < n - 1} )
16. [p∈bag-partitions(eq;b)|¬bbag-null(fst(p))] = bb ∈ bag({p:bag(X) × bag(X)| #(snd(p)) < n - 1} )
⊢ Σ(p∈bb). fps-div-coeff(eq;r;λb.if bag-null(b) then 1 else 0 fi ;λb.1;1;snd(p))
= Σ(p∈bb). int-to-ring(r;bag-moebius(eq;snd(p)))
∈ |r|
Latex:
Latex:
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : \mBbbZ{}
6. 0 < n
7. \mforall{}b:bag(X). (\#(b) < n - 1 {}\mRightarrow{} (fps-div-coeff(eq;r;1;\mlambda{}b.1;1;b) = int-to-ring(r;bag-moebius(eq;b))))
8. b : bag(X)
9. \mneg{}(b = \{\})
10. \#(b) < n
11. Assoc(\mBbbZ{};\mlambda{}x,y. (x + y))
12. Comm(\mBbbZ{};\mlambda{}x,y. (x + y))
13. bag-moebius(eq;b) = (-\mSigma{}(p\mmember{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]). bag-moebius(eq;snd(p)))
14. \mSigma{}(x\mmember{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]). int-to-ring(r;bag-moebius(eq;snd(x)))
= int-to-ring(r;\mSigma{}(x\mmember{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]). bag-moebius(eq;snd(x)))
\mvdash{} \mSigma{}(p\mmember{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]). fps-div-coeff(eq;r;\mlambda{}b.if bag-null(b)
then 1
else 0
fi ;\mlambda{}b.1;1;snd(p))
= \mSigma{}(p\mmember{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]). int-to-ring(r;bag-moebius(eq;snd(p)))
By
Latex:
TACTIC:(GenConcl \mkleeneopen{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))] = bb\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index