---

Step * 1 2 of Lemma KozenSilva-corollary0


1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. d : ℕ ⟶ ℕ
6. k : ℕ
7. b : bag(ℕk)
8. upto(k) = b ∈ bag(ℕk)
⊢ Π(i∈b).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d i)
= (1*Π(i∈b).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(if (i + 1 =z 0) then 0 else d ((i + 1) - 1) fi ))
∈ PowerSeries(r)
BY
{ xxx(RWO "mul_one_fps.2" 0 THEN Try (Complete (Auto)))xxx }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. d : ℕ ⟶ ℕ
6. k : ℕ
7. b : bag(ℕk)
8. upto(k) = b ∈ bag(ℕk)
⊢ Π(i∈b).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d i)
= Π(i∈b).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(if (i + 1 =z 0) then 0 else d ((i + 1) - 1) fi )
∈ PowerSeries(r)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  \mneg{}(x  =  y)
5.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
6.  k  :  \mBbbN{}
7.  b  :  bag(\mBbbN{}k)
8.  upto(k)  =  b
\mvdash{}  \mPi{}(i\mmember{}b).((((k  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  i)
=  (1*\mPi{}(i\mmember{}b).((((k  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(if  (i  +  1  =\msubz{}  0)  then  0  else  d  ((i  +  1)  -  1)  fi  ))


By

---

Latex:
xxx(RWO  "mul\_one\_fps.2"  0  THEN  Try  (Complete  (Auto)))xxx

---

Home Index