---

Step * 1 of Lemma KozenSilva-corollary2

.....basecase..... 
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℤ
⊢ ∀d:ℕ ⟶ ℕ. (Π(i∈upto(0)).(((0 - i)*atom(x)+atom(y)))^(d i)[bag-rep(Σ(d i | i < 0);x)] = Π((0 - i)^(d i) | i < 0) ∈ ℤ)
BY
{ TACTIC:(Auto
          THEN Reduce (-1)
          THEN RepUR ``fps-product fps-coeff bag-product bag-summation bag-accum int-prod fps-one`` 0
          THEN RWO "bag-null-rep" 0
          THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  Reduce  (-1)
                THEN  RepUR  ``fps-product  fps-coeff  bag-product  bag-summation  bag-accum  int-prod  fps-one``  0
                THEN  RWO  "bag-null-rep"  0
                THEN  Auto)\mcdot{}

---

Home Index