---

Step * 1 of Lemma KozenSilva-theorem


1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. h : PowerSeries(r)
6. d : ℕ ⟶ ℕ
7. k : ℤ
8. 0 = 0 ∈ ℤ
⊢ [h]_Σ(d i | i < 1)
= ([h]_d 0(y:=((0 ⋅r 1)*atom(x)+atom(y)))*Π(i∈[]).((((0 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
BY
{ TACTIC:((RWO "sum-unroll" 0 THENA Auto)
          THEN Reduce 0
          THEN RepUR ``fps-product bag-product bag-summation bag-accum`` 0
          THEN Subst' 0 ⋅r 1 ~ 0 0) }

1
.....equality..... 
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. h : PowerSeries(r)
6. d : ℕ ⟶ ℕ
7. k : ℤ
8. 0 = 0 ∈ ℤ
⊢ 0 ⋅r 1 ~ 0

2
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. h : PowerSeries(r)
6. d : ℕ ⟶ ℕ
7. k : ℤ
8. 0 = 0 ∈ ℤ
⊢ [h]_0 + (d 0) = ([h]_d 0(y:=((0)*atom(x)+atom(y)))*1) ∈ PowerSeries(r)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  \mneg{}(x  =  y)
5.  h  :  PowerSeries(r)
6.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
7.  k  :  \mBbbZ{}
8.  0  =  0
\mvdash{}  [h]\_\mSigma{}(d  i  |  i  <  1)
=  ([h]\_d  0(y:=((0  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}[]).((((0  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  (i  +  1)))


By

---

Latex:
TACTIC:((RWO  "sum-unroll"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  RepUR  ``fps-product  bag-product  bag-summation  bag-accum``  0
                THEN  Subst'  0  \mcdot{}r  1  \msim{}  0  0)

---

Home Index