---

Step * 1 4 of Lemma KozenSilva-lemma


1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
10. fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
11. ∀f,g:PowerSeries(r).
      ([([(f+g)]_n(y:=1)*Δ(x,y))]_m = ([([f]_n(y:=1)*Δ(x,y))]_m+[([g]_n(y:=1)*Δ(x,y))]_m) ∈ PowerSeries(r))
12. f : PowerSeries(r)
13. g : PowerSeries(r)
⊢ ([(f+g)]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
= (([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))+([g]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
∈ PowerSeries(r)
BY
{ xxx((RWW "fps-compose-add fps-add-slice" 0 THENM FpsNorm 0) THEN Auto')xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  h  :  PowerSeries(r)
5.  n  :  \mBbbN{}
6.  m  :  \mBbbN{}
7.  n  \mleq{}  m
8.  \mneg{}(x  =  y)
9.  fps-ucont(Atom;AtomDeq;r;f.[([f]\_n(y:=1)*\mDelta{}(x,y))]\_m)
10.  fps-ucont(Atom;AtomDeq;r;f.([f]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n)))
11.  \mforall{}f,g:PowerSeries(r).
            ([([(f+g)]\_n(y:=1)*\mDelta{}(x,y))]\_m  =  ([([f]\_n(y:=1)*\mDelta{}(x,y))]\_m+[([g]\_n(y:=1)*\mDelta{}(x,y))]\_m))
12.  f  :  PowerSeries(r)
13.  g  :  PowerSeries(r)
\mvdash{}  ([(f+g)]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n))
=  (([f]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n))
      +([g]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n)))


By

---

Latex:
xxx((RWW  "fps-compose-add  fps-add-slice"  0  THENM  FpsNorm  0)  THEN  Auto')xxx

---

Home Index