---

Step * 1 2 of Lemma fps-Pascal-iff


1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. fps-Pascal(r;x;y;f)
⇐⇒ (f*(1-(<{x}>+<{y}>))) = ((((1-<{y}>)*f(x:=0))+((1-<{x}>)*f(y:=0)))-f(x:=0)(y:=0)) ∈ PowerSeries(r)
⊢ fps-Pascal(r;x;y;f) ⇐⇒ f = (((((1-<{y}>)*f(x:=0))+((1-<{x}>)*f(y:=0)))-f(x:=0)(y:=0))*Δ(x,y)) ∈ PowerSeries(r)
BY
{ ((MoveToConcl (-1) THEN (GenConclAtAddr [1;2;3] THENA Auto))
   THEN (D 0 THENA Auto)
   THEN (RWO  "-1" 0 THENA Auto)
   THEN All Thin) }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. v : PowerSeries(r)
⊢ (f*(1-(<{x}>+<{y}>))) = v ∈ PowerSeries(r) ⇐⇒ f = (v*Δ(x,y)) ∈ PowerSeries(r)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  f  :  PowerSeries(r)
5.  \mneg{}(x  =  y)
6.  fps-Pascal(r;x;y;f)
\mLeftarrow{}{}\mRightarrow{}  (f*(1-(<\{x\}>+<\{y\}>)))  =  ((((1-<\{y\}>)*f(x:=0))+((1-<\{x\}>)*f(y:=0)))-f(x:=0)(y:=0))
\mvdash{}  fps-Pascal(r;x;y;f)  \mLeftarrow{}{}\mRightarrow{}  f  =  (((((1-<\{y\}>)*f(x:=0))+((1-<\{x\}>)*f(y:=0)))-f(x:=0)(y:=0))*\mDelta{}(x,y))


By

---

Latex:
((MoveToConcl  (-1)  THEN  (GenConclAtAddr  [1;2;3]  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  All  Thin)

---

Home Index