---

Step * 1 7 1 1 1 2 1 1 1 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,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))
13. ∀c:|r|. ∀f:PowerSeries(r).  ([([(c)*f]_n(y:=1)*Δ(x,y))]_m = (c)*[([f]_n(y:=1)*Δ(x,y))]_m ∈ PowerSeries(r))
14. ∀c:|r|. ∀f:PowerSeries(r).
      (([(c)*f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
      = (c)*([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
      ∈ PowerSeries(r))
15. b : bag(Atom)
16. #(b) = n ∈ ℤ
17. IsMonoid(PowerSeries(r);λk,y. (k+y);0)
18. Comm(PowerSeries(r);λk,y. (k+y))
19. fps-summation(r;[k∈upto(m + 1)|(k =z #((b|¬y)))];k.([<(b|¬y)>]_k*[Δ(x,y)]_m - k))
= (<b>(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
∈ PowerSeries(r)
20. ∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(ℤ)]. ∀[p:ℤ ⟶ 𝔹]. ∀[f:ℤ ⟶ R].
      Σ(x∈[x∈b|p[x]]). f[x] = Σ(x∈b). if p[x] then f[x] else zero fi  ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
21. k : ℤ
22. k ↓∈ upto(m + 1)
⊢ ([<(b|¬y)>]_k*[Δ(x,y)]_m - k) = if (k =z #((b|¬y))) then ([<(b|¬y)>]_k*[Δ(x,y)]_m - k) else 0 fi  ∈ PowerSeries(r)
BY
{ xxx((RWO "fps-single-slice" 0 THEN Auto) THEN AutoSplit)xxx }

1
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,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))
13. ∀c:|r|. ∀f:PowerSeries(r).  ([([(c)*f]_n(y:=1)*Δ(x,y))]_m = (c)*[([f]_n(y:=1)*Δ(x,y))]_m ∈ PowerSeries(r))
14. ∀c:|r|. ∀f:PowerSeries(r).
      (([(c)*f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
      = (c)*([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
      ∈ PowerSeries(r))
15. b : bag(Atom)
16. #(b) = n ∈ ℤ
17. IsMonoid(PowerSeries(r);λk,y. (k+y);0)
18. Comm(PowerSeries(r);λk,y. (k+y))
19. fps-summation(r;[k∈upto(m + 1)|(k =z #((b|¬y)))];k.([<(b|¬y)>]_k*[Δ(x,y)]_m - k))
= (<b>(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
∈ PowerSeries(r)
20. ∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(ℤ)]. ∀[p:ℤ ⟶ 𝔹]. ∀[f:ℤ ⟶ R].
      Σ(x∈[x∈b|p[x]]). f[x] = Σ(x∈b). if p[x] then f[x] else zero fi  ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
21. k : ℤ
22. #((b|¬y)) ≠ k
23. k ↓∈ upto(m + 1)
⊢ (0*[Δ(x,y)]_m - k) = if (k =z #((b|¬y))) then (0*[Δ(x,y)]_m - k) else 0 fi  ∈ PowerSeries(r)

---

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.  \mforall{}f,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))))
13.  \mforall{}c:|r|.  \mforall{}f:PowerSeries(r).    ([([(c)*f]\_n(y:=1)*\mDelta{}(x,y))]\_m  =  (c)*[([f]\_n(y:=1)*\mDelta{}(x,y))]\_m)
14.  \mforall{}c:|r|.  \mforall{}f:PowerSeries(r).
            (([(c)*f]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n))
            =  (c)*([f]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n)))
15.  b  :  bag(Atom)
16.  \#(b)  =  n
17.  IsMonoid(PowerSeries(r);\mlambda{}k,y.  (k+y);0)
18.  Comm(PowerSeries(r);\mlambda{}k,y.  (k+y))
19.  fps-summation(r;[k\mmember{}upto(m  +  1)|(k  =\msubz{}  \#((b|\mneg{}y)))];k.([<(b|\mneg{}y)>]\_k*[\mDelta{}(x,y)]\_m  -  k))
=  (<b>(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n))
20.  \mforall{}[R:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(\mBbbZ{})].  \mforall{}[p:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  R].
            \mSigma{}(x\mmember{}[x\mmember{}b|p[x]]).  f[x]  =  \mSigma{}(x\mmember{}b).  if  p[x]  then  f[x]  else  zero  fi   
            supposing  IsMonoid(R;add;zero)  \mwedge{}  Comm(R;add)
21.  k  :  \mBbbZ{}
22.  k  \mdownarrow{}\mmember{}  upto(m  +  1)
\mvdash{}  ([<(b|\mneg{}y)>]\_k*[\mDelta{}(x,y)]\_m  -  k)  =  if  (k  =\msubz{}  \#((b|\mneg{}y)))  then  ([<(b|\mneg{}y)>]\_k*[\mDelta{}(x,y)]\_m  -  k)  else  0  fi 


By

---

Latex:
xxx((RWO  "fps-single-slice"  0  THEN  Auto)  THEN  AutoSplit)xxx

---

Home Index