---

Step * 2 1 2 1 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. k ∈ ℕ
9. k ≠ 0
10. 0 < k
11. [Moessner-aux(r;x;y;h;d;k - 1)]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
12. Σ(d i | i < k) ∈ ℕ
13. Σ(d i | i < k + 1) ∈ ℕ
14. [([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)
                                                                      +atom(y)))^(d (i + 1)))]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
⊢ [([([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k 
- 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))]_Σ(d i | i < k)(y:=1)*Δ(x,y))]_Σ(d i | i < k + 1)
= ([h]_d 0(y:=((k ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
BY
{ TACTIC:((Assert Σ(d i | i < k) ≤ Σ(d i | i < k + 1) BY
                 (RW (AddrC [2] (LemmaC `sum_split1`)) 0 THEN Auto'))
          THEN (RWW "KozenSilva-lemma -2 fps-compose-mul fps-mul-assoc" 0⋅
                THEN Try (Complete ((GenConclTerm ⌜upto(k)⌝⋅ THEN Auto')))
                THEN Try (Complete ((GenConclTerm ⌜upto(k - 1)⌝⋅ THEN Auto'))))⋅
          ) }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. h : PowerSeries(r)
6. d : ℕ ⟶ ℕ
7. k : ℤ
8. k ∈ ℕ
9. k ≠ 0
10. 0 < k
11. [Moessner-aux(r;x;y;h;d;k - 1)]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
12. Σ(d i | i < k) ∈ ℕ
13. Σ(d i | i < k + 1) ∈ ℕ
14. [([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)
                                                                      +atom(y)))^(d (i + 1)))]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
15. Σ(d i | i < k) ≤ Σ(d i | i < k + 1)
⊢ ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))(y:=(atom(x)+atom(y)))*(Π(i∈upto(k 
- 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(Σ(d i | i < k + 1) 
- Σ(d i | i < k))))
= ([h]_d 0(y:=((k ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 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.  k  \mmember{}  \mBbbN{}
9.  k  \mneq{}  0
10.  0  <  k
11.  [Moessner-aux(r;x;y;h;d;k  -  1)]\_\mSigma{}(d  i  |  i  <  k)
=  ([h]\_d  0(y:=(((k  -  1)  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k 
    -  1)).((((k  -  1  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  (i  +  1)))
12.  \mSigma{}(d  i  |  i  <  k)  \mmember{}  \mBbbN{}
13.  \mSigma{}(d  i  |  i  <  k  +  1)  \mmember{}  \mBbbN{}
14.  [([h]\_d  0(y:=(((k  -  1)  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k 
-  1)).((((k  -  1  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  (i  +  1)))]\_\mSigma{}(d  i  |  i  <  k)
=  ([h]\_d  0(y:=(((k  -  1)  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k 
    -  1)).((((k  -  1  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  (i  +  1)))
\mvdash{}  [([([h]\_d  0(y:=(((k  -  1)  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k 
-  1)).((((k  -  1  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  (i  +  1)))]\_\mSigma{}(d  i  |  i  <  k)(y:=1)*\mDelta{}(x,y))]\_\mSigma{}(d 
                                                                                                                                                                                      i  |  i  <  k
+  1)
=  ([h]\_d  0(y:=((k  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k)).((((k  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d 
                                                                                                                                                                                      (i  +  1)))


By

---

Latex:
TACTIC:((Assert  \mSigma{}(d  i  |  i  <  k)  \mleq{}  \mSigma{}(d  i  |  i  <  k  +  1)  BY
                              (RW  (AddrC  [2]  (LemmaC  `sum\_split1`))  0  THEN  Auto'))
                THEN  (RWW  "KozenSilva-lemma  -2  fps-compose-mul  fps-mul-assoc"  0\mcdot{}
                            THEN  Try  (Complete  ((GenConclTerm  \mkleeneopen{}upto(k)\mkleeneclose{}\mcdot{}  THEN  Auto')))
                            THEN  Try  (Complete  ((GenConclTerm  \mkleeneopen{}upto(k  -  1)\mkleeneclose{}\mcdot{}  THEN  Auto'))))\mcdot{}
                )

---

Home Index