---

Step * 1 of Lemma fps-Pascal-iff


1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
⊢ 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
{ Assert ⌜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)⌝⋅ }

1
.....assertion..... 
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
⊢ 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)

2
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)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  f  :  PowerSeries(r)
5.  \mneg{}(x  =  y)
\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:
Assert  \mkleeneopen{}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))\mkleeneclose{}\mcdot{}

---

Home Index