---

Step * 2 1 of Lemma KozenSilva-corollary2

.....equality..... 
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℤ
5. 0 < k
6. d : ℕ ⟶ ℕ
7. Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d (i + 1))[bag-rep(Σ(d (i + 1) | i < k - 1);x)]
= Π((k - 1 - i)^(d (i + 1)) | i < k - 1)
∈ ℤ
⊢ Π(i∈upto(k)).(((k - i)*atom(x)+atom(y)))^(d i)
= ((((k)*atom(x)+atom(y)))^(d 0)*Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(ℤ-rng)
BY
{ TACTIC:(RW (AddrC [2] (LemmaC `fps-product-upto`)) 0
          THEN Try (Complete (Auto))
          THEN GenConcl ⌜upto(k - 1) = b ∈ bag(ℕk - 1)⌝⋅
          THEN Auto
          THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  Atom
2.  y  :  Atom
3.  \mneg{}(x  =  y)
4.  k  :  \mBbbZ{}
5.  0  <  k
6.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
7.  \mPi{}(i\mmember{}upto(k  -  1)).(((k  -  1  -  i)*atom(x)+atom(y)))\^{}(d  (i  +  1))[bag-rep(\mSigma{}(d  (i  +  1)  |  i  <  k  -  1);x)]
=  \mPi{}((k  -  1  -  i)\^{}(d  (i  +  1))  |  i  <  k  -  1)
\mvdash{}  \mPi{}(i\mmember{}upto(k)).(((k  -  i)*atom(x)+atom(y)))\^{}(d  i)
=  ((((k)*atom(x)+atom(y)))\^{}(d  0)*\mPi{}(i\mmember{}upto(k  -  1)).(((k  -  1  -  i)*atom(x)+atom(y)))\^{}(d  (i  +  1)))


By

---

Latex:
TACTIC:(RW  (AddrC  [2]  (LemmaC  `fps-product-upto`))  0
                THEN  Try  (Complete  (Auto))
                THEN  GenConcl  \mkleeneopen{}upto(k  -  1)  =  b\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index