Step
*
1
7
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)
⊢ [([<b>]_n(y:=1)*Δ(x,y))]_m = ([<b>]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)
BY
{ xxx((RWO "fps-set-to-one-single 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 ∈ ℤ
⊢ [(<(b|¬y)>*Δ(x,y))]_m = (<b>(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)
2
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
⊢ [(0*Δ(x,y))]_m = (0(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ 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)
\mvdash{} [([<b>]\_n(y:=1)*\mDelta{}(x,y))]\_m = ([<b>]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m - n))
By
Latex:
xxx((RWO "fps-set-to-one-single fps-single-slice" 0 THEN Auto') THEN AutoSplit)xxx
Home
Index