---

Step * 2 2 2 2 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. u : ℤ
12. Π((k - 1 - i)^(d (i + 1)) | i < k - 1) = u ∈ ℤ
13. m : ℕ
14. (d 0) = m ∈ ℕ
15. X[bag-rep(N;x)] = u ∈ ℤ
⊢ ((((k)*atom(x)+atom(y)))^(m)*X)[bag-rep(m + N;x)] = (k^m * u) ∈ ℤ
BY
{ TACTIC:((InstLemma `fps-mul-coeff-bag-rep-simple` [⌜Atom⌝;⌜AtomDeq⌝;⌜m + N⌝;⌜m⌝]⋅ THENA Auto)
          THEN RWO "-1" 0
          THEN Auto) }

1
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. u : ℤ
12. Π((k - 1 - i)^(d (i + 1)) | i < k - 1) = u ∈ ℤ
13. m : ℕ
14. (d 0) = m ∈ ℕ
15. X[bag-rep(N;x)] = u ∈ ℤ
16. ∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[x:Atom].
      (f*g)[bag-rep(m + N;x)] = (* f[bag-rep(m;x)] g[bag-rep((m + N) - m;x)]) ∈ |r| 
      supposing ∀i:ℕ(m + N) + 1. ((¬(i = m ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
17. i : ℕ(m + N) + 1
18. ¬(i = m ∈ ℤ)
⊢ (((k)*atom(x)+atom(y)))^(m)[bag-rep(i;x)] = 0 ∈ |ℤ-rng|

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 ∈ ℕ
11. u : ℤ
12. Π((k - 1 - i)^(d (i + 1)) | i < k - 1) = u ∈ ℤ
13. m : ℕ
14. (d 0) = m ∈ ℕ
15. X[bag-rep(N;x)] = u ∈ ℤ
16. ∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[x:Atom].
      (f*g)[bag-rep(m + N;x)] = (* f[bag-rep(m;x)] g[bag-rep((m + N) - m;x)]) ∈ |r| 
      supposing ∀i:ℕ(m + N) + 1. ((¬(i = m ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
⊢ (* (((k)*atom(x)+atom(y)))^(m)[bag-rep(m;x)] X[bag-rep((m + N) - m;x)]) = (k^m * u) ∈ ℤ

---

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.  u  :  \mBbbZ{}
12.  \mPi{}((k  -  1  -  i)\^{}(d  (i  +  1))  |  i  <  k  -  1)  =  u
13.  m  :  \mBbbN{}
14.  (d  0)  =  m
15.  X[bag-rep(N;x)]  =  u
\mvdash{}  ((((k)*atom(x)+atom(y)))\^{}(m)*X)[bag-rep(m  +  N;x)]  =  (k\^{}m  *  u)


By

---

Latex:
TACTIC:((InstLemma  `fps-mul-coeff-bag-rep-simple`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}m  +  N\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  RWO  "-1"  0
                THEN  Auto)

---

Home Index