---

Step * 1 1 1 1 of Lemma fps-mul-coeff-bag-rep-simple


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. x1 : bag(X)
12. x2 : bag(X)
13. n = (#(x1) + #(x2)) ∈ ℤ
14. x1 = bag-rep(#(x1);x) ∈ bag(X)
15. x2 = bag-rep(#(x2);x) ∈ bag(X)
⊢ (<x1, x2> = <bag-rep(k;x), bag-rep(n - k;x)> ∈ (bag(X) × bag(X))) ∨ ((* f[fst(<x1, x2>)] g[snd(<x1, x2>)]) = 0 ∈ |r|)
BY
{ xxx(Reduce 0 THEN Decide ⌜#(x1) = k ∈ ℤ⌝⋅ THEN Auto)xxx }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. x1 : bag(X)
12. x2 : bag(X)
13. n = (#(x1) + #(x2)) ∈ ℤ
14. x1 = bag-rep(#(x1);x) ∈ bag(X)
15. x2 = bag-rep(#(x2);x) ∈ bag(X)
16. #(x1) = k ∈ ℤ
⊢ (<x1, x2> = <bag-rep(k;x), bag-rep(n - k;x)> ∈ (bag(X) × bag(X))) ∨ ((* f[x1] g[x2]) = 0 ∈ |r|)

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. x1 : bag(X)
12. x2 : bag(X)
13. n = (#(x1) + #(x2)) ∈ ℤ
14. x1 = bag-rep(#(x1);x) ∈ bag(X)
15. x2 = bag-rep(#(x2);x) ∈ bag(X)
16. ¬(#(x1) = k ∈ ℤ)
⊢ (<x1, x2> = <bag-rep(k;x), bag-rep(n - k;x)> ∈ (bag(X) × bag(X))) ∨ ((* f[x1] g[x2]) = 0 ∈ |r|)

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  n  :  \mBbbN{}
5.  k  :  \mBbbN{}n  +  1
6.  r  :  CRng
7.  f  :  PowerSeries(X;r)
8.  g  :  PowerSeries(X;r)
9.  x  :  X
10.  \mforall{}i:\mBbbN{}n  +  1.  ((\mneg{}(i  =  k))  {}\mRightarrow{}  (f[bag-rep(i;x)]  =  0))
11.  x1  :  bag(X)
12.  x2  :  bag(X)
13.  n  =  (\#(x1)  +  \#(x2))
14.  x1  =  bag-rep(\#(x1);x)
15.  x2  =  bag-rep(\#(x2);x)
\mvdash{}  (<x1,  x2>  =  <bag-rep(k;x),  bag-rep(n  -  k;x)>)  \mvee{}  ((*  f[fst(<x1,  x2>)]  g[snd(<x1,  x2>)])  =  0)


By

---

Latex:
xxx(Reduce  0  THEN  Decide  \mkleeneopen{}\#(x1)  =  k\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index