---

Step * 2 2 of Lemma KozenSilva-corollary2


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)
∈ ℤ
BY
{ TACTIC:(MoveToConcl (-1)
          THEN (GenConcl ⌜Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d (i + 1)) = X ∈ PowerSeries(ℤ-rng)⌝⋅
                THENA (Assert ⌜upto(k - 1) ∈ bag(ℕk)⌝⋅ THEN Auto)
                )
          THEN (Subst ⌜Σ(d i | i < k) ~ (d 0) + Σ(d (i + 1) | i < k - 1)⌝ 0⋅
          THENM (GenConcl ⌜Σ(d (i + 1) | i < k - 1) = N ∈ ℕ⌝⋅
                 THENA (Auto THEN (MemTypeCD THEN Auto) THEN BLemma `non_neg_sum` THEN Auto)
                 )
          )) }

1
.....equality..... 
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)
⊢ Σ(d i | i < k) ~ (d 0) + Σ(d (i + 1) | i < k - 1)

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

---

Latex:

---

Latex:

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{}  ((((k)*atom(x)+atom(y)))\^{}(d  0)*\mPi{}(i\mmember{}upto(k  -  1)).(((k  -  1  -  i)*atom(x)
                                                                                                        +atom(y)))\^{}(d  (i  +  1)))[bag-rep(\mSigma{}(d 
                                                                                                                                                                            i  |  i  <  k);x)]
=  \mPi{}((k  -  i)\^{}(d  i)  |  i  <  k)


By

---

Latex:
TACTIC:(MoveToConcl  (-1)
                THEN  (GenConcl  \mkleeneopen{}\mPi{}(i\mmember{}upto(k  -  1)).(((k  -  1  -  i)*atom(x)+atom(y)))\^{}(d  (i  +  1))  =  X\mkleeneclose{}\mcdot{}
                            THENA  (Assert  \mkleeneopen{}upto(k  -  1)  \mmember{}  bag(\mBbbN{}k)\mkleeneclose{}\mcdot{}  THEN  Auto)
                            )
                THEN  (Subst  \mkleeneopen{}\mSigma{}(d  i  |  i  <  k)  \msim{}  (d  0)  +  \mSigma{}(d  (i  +  1)  |  i  <  k  -  1)\mkleeneclose{}  0\mcdot{}
                THENM  (GenConcl  \mkleeneopen{}\mSigma{}(d  (i  +  1)  |  i  <  k  -  1)  =  N\mkleeneclose{}\mcdot{}
                              THENA  (Auto  THEN  (MemTypeCD  THEN  Auto)  THEN  BLemma  `non\_neg\_sum`  THEN  Auto)
                              )
                ))

---

Home Index