---

Step * 2 2 2 1 1 of Lemma KozenSilva-corollary2


1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℤ
5. 0 < k
6. d : ℕ ⟶ ℕ
7. X : PowerSeries(ℤ-rng)
8. Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d (i + 1)) = X ∈ PowerSeries(ℤ-rng)
9. N : ℕ
10. Σ(d (i + 1) | i < k - 1) = N ∈ ℕ
11. Π((k - x)^(d x) | x < k) = (Π((k - x)^(d x) | x < 1) * Π((k - x + 1)^(d (x + 1)) | x < k - 1)) ∈ ℤ
⊢ Π((k - x)^(d x) | x < 1) = k^(d 0) ∈ ℤ
BY
{ (RepUR ``int-prod`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Atom
2.  y  :  Atom
3.  \mneg{}(x  =  y)
4.  k  :  \mBbbZ{}
5.  0  <  k
6.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
7.  X  :  PowerSeries(\mBbbZ{}-rng)
8.  \mPi{}(i\mmember{}upto(k  -  1)).(((k  -  1  -  i)*atom(x)+atom(y)))\^{}(d  (i  +  1))  =  X
9.  N  :  \mBbbN{}
10.  \mSigma{}(d  (i  +  1)  |  i  <  k  -  1)  =  N
11.  \mPi{}((k  -  x)\^{}(d  x)  |  x  <  k)  =  (\mPi{}((k  -  x)\^{}(d  x)  |  x  <  1)  *  \mPi{}((k  -  x  +  1)\^{}(d  (x  +  1))  |  x  <  k  -  1))
\mvdash{}  \mPi{}((k  -  x)\^{}(d  x)  |  x  <  1)  =  k\^{}(d  0)


By

---

Latex:
(RepUR  ``int-prod``  0  THEN  Auto)

---

Home Index