---

Step * 1 6 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|
15. 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)
BY
{ xxx(InstLemma `fps-scalar-mul-property` [⌜Atom⌝;⌜AtomDeq⌝;⌜r⌝]⋅
      THEN Auto
      THEN InstHyp [⌜c⌝] (-1)⋅
      THEN Auto
      THEN (UnfoldTopAb (-1) THEN Reduce (-1))
      THEN xxx(RWO "-1.1" 0 THEN Auto THEN Auto' THEN EqCD THEN Auto')xxx)⋅xxx }

1
.....subterm..... T:t
3:n
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|
15. f : PowerSeries(r)
16. IsAction(|r|;*;1;PowerSeries(r);λc,f. (c)*f)
17. IsBilinear(|r|;PowerSeries(r);PowerSeries(r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f)
18. ∀c:|r|. Dist1op2opLR(PowerSeries(r);λf.(c)*f;λf,g. (f*g))
19. ∀[u,v:PowerSeries(r)].  (((c)*(u*v) = ((c)*u*v) ∈ PowerSeries(r)) ∧ ((c)*(u*v) = (u*(c)*v) ∈ PowerSeries(r)))
⊢ [(c)*f]_n(y:=(atom(x)+atom(y))) = (c)*[f]_n(y:=(atom(x)+atom(y))) ∈ 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.  c  :  |r|
15.  f  :  PowerSeries(r)
\mvdash{}  ([(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))


By

---

Latex:
xxx(InstLemma  `fps-scalar-mul-property`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  InstHyp  [\mkleeneopen{}c\mkleeneclose{}]  (-1)\mcdot{}
        THEN  Auto
        THEN  (UnfoldTopAb  (-1)  THEN  Reduce  (-1))
        THEN  xxx(RWO  "-1.1"  0  THEN  Auto  THEN  Auto'  THEN  EqCD  THEN  Auto')xxx)\mcdot{}xxx

---

Home Index