---

Step * 2 of Lemma KozenSilva-corollary2

.....upcase..... 
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℤ
5. 0 < k
6. ∀d:ℕ ⟶ ℕ
     (Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d i)[bag-rep(Σ(d i | i < k - 1);x)]
     = Π((k - 1 - i)^(d i) | i < k - 1)
     ∈ ℤ)
⊢ ∀d:ℕ ⟶ ℕ. (Π(i∈upto(k)).(((k - i)*atom(x)+atom(y)))^(d i)[bag-rep(Σ(d i | i < k);x)] = Π((k - i)^(d i) | i < k) ∈ ℤ)
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN (InstHyp [⌜λi.(d (i + 1))⌝] (-2)⋅ THENA Auto)
          THEN Thin (-3)
          THEN Reduce (-1)
          THEN Subst' Π(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) 0)⋅ }

1
.....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)

2
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)
∈ ℤ
⊢ ((((k)*atom(x)+atom(y)))^(d 0)*Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d (i + 1)))[bag-rep(Σ(d 
                                                                                                         i | i < k);x)]
= Π((k - i)^(d i) | i < k)
∈ ℤ

3
.....wf..... 
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)
∈ ℤ
8. z : PowerSeries(ℤ-rng)
⊢ z[bag-rep(Σ(d i | i < k);x)] = Π((k - i)^(d i) | i < k) ∈ ℤ ∈ ℙ

---

Latex:

---

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


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.(d  (i  +  1))\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                THEN  Thin  (-3)
                THEN  Reduce  (-1)
                THEN  Subst'  \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)))  0)
\mcdot{}

---

Home Index