---

Step * of Lemma KozenSilva-theorem

∀[r:CRng]. ∀[x,y:Atom].
  ∀[h:PowerSeries(r)]. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
    (Moessner(r;x;y;h;d;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)) 
  supposing ¬(x = y ∈ Atom)
BY
{ (Unfold `Moessner` 0 THEN InductionOnNat THEN RecUnfold `Moessner-aux` 0 THEN AutoSplit) }

1
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)

2
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. h : PowerSeries(r)
6. d : ℕ ⟶ ℕ
7. k : ℤ
8. k ≠ 0
9. 0 < k
10. [Moessner-aux(r;x;y;h;d;k - 1)]_Σ(d i | i < (k - 1) + 1)
= ([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)
⊢ [([Moessner-aux(r;x;y;h;d;k - 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)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].
    \mforall{}[h:PowerSeries(r)].  \mforall{}[d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[k:\mBbbN{}].
        (Moessner(r;x;y;h;d;k)
        =  ([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)))) 
    supposing  \mneg{}(x  =  y)


By

---

Latex:
(Unfold  `Moessner`  0  THEN  InductionOnNat  THEN  RecUnfold  `Moessner-aux`  0  THEN  AutoSplit)

---

Home Index