Step * 2 2 2 2 1 2 of Lemma KozenSilva-corollary2


1. Atom
2. Atom
3. ¬(x y ∈ Atom)
4. : ℤ
5. 0 < k
6. : ℕ ⟶ ℕ
7. PowerSeries(ℤ-rng)
8. Π(i∈upto(k 1)).(((k i)*atom(x)+atom(y)))^(d (i 1)) X ∈ PowerSeries(ℤ-rng)
9. : ℕ
10. Σ(d (i 1) i < 1) N ∈ ℕ
11. : ℤ
12. Π((k i)^(d (i 1)) i < 1) u ∈ ℤ
13. : ℕ
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) ∈ ℤ
BY
TACTIC:(RepUR ``rng_times int_ring`` THEN EqCD THEN Auto) }

1
.....subterm..... T:t
1:n
1. Atom
2. Atom
3. ¬(x y ∈ Atom)
4. : ℤ
5. 0 < k
6. : ℕ ⟶ ℕ
7. PowerSeries(ℤ-rng)
8. Π(i∈upto(k 1)).(((k i)*atom(x)+atom(y)))^(d (i 1)) X ∈ PowerSeries(ℤ-rng)
9. : ℕ
10. Σ(d (i 1) i < 1) N ∈ ℕ
11. : ℤ
12. Π((k i)^(d (i 1)) i < 1) u ∈ ℤ
13. : ℕ
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)] k^m ∈ ℤ


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
16.  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(r)].  \mforall{}[x:Atom].
            (f*g)[bag-rep(m  +  N;x)]  =  (*  f[bag-rep(m;x)]  g[bag-rep((m  +  N)  -  m;x)]) 
            supposing  \mforall{}i:\mBbbN{}(m  +  N)  +  1.  ((\mneg{}(i  =  m))  {}\mRightarrow{}  (f[bag-rep(i;x)]  =  0))
\mvdash{}  (*  (((k)*atom(x)+atom(y)))\^{}(m)[bag-rep(m;x)]  X[bag-rep((m  +  N)  -  m;x)])  =  (k\^{}m  *  u)


By


Latex:
TACTIC:(RepUR  ``rng\_times  int\_ring``  0  THEN  EqCD  THEN  Auto)




Home Index