---

Step * 1 1 of Lemma fps-Pascal-iff

.....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)
BY
{ TACTIC:((FpsNorm 0 THENA Auto)
          THEN (RWO "fps-mul-single-general" 0 THENA Auto)⋅
          THEN (RWO "fps-mul-comm" 0
                THENA (Try (QuickAuto)
                       THEN Try (Fold `member` 0)
                       THEN RepUR ``power-series fps-neg fps-add fps-coeff`` 0
                       THEN Auto)
                )
          THEN (RWO "fps-mul-single-general" 0
                THENA (Try (QuickAuto)
                       THEN Try (Fold `member` 0)
                       THEN RepUR ``power-series fps-neg fps-add fps-coeff`` 0
                       THEN Auto)
                )
          THEN RepUR ``fps-Pascal fps-elim-x fps-elim fps-add fps-coeff fps-neg fps-sub`` 0
          THEN RepUR ``power-series`` 0
          THEN Auto
          THEN Try ((Unfold `power-series` 0 THEN Auto))) }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. ∀b:bag(Atom). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
⊢ (λb.(+r (-r case bag-diff(AtomDeq;b;{x}) of inl(d) => f d | inr(z) => 0) 
       (+r (-r case bag-diff(AtomDeq;b;{y}) of inl(d) => f d | inr(z) => 0) (f b))))
= (λb.(+r (-r if bag-deq-member(AtomDeq;y;b) then 0 if bag-deq-member(AtomDeq;x;b) then 0 else f b fi ) 
       ...))
∈ (bag(Atom) ⟶ |r|)

2
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. (λb.(+r (-r case bag-diff(AtomDeq;b;{x}) of inl(d) => f d | inr(z) => 0) 
        (+r (-r case bag-diff(AtomDeq;b;{y}) of inl(d) => f d | inr(z) => 0) (f b))))
= (λb.(+r (-r if bag-deq-member(AtomDeq;y;b) then 0 if bag-deq-member(AtomDeq;x;b) then 0 else f b fi ) 
       ...))
∈ (bag(Atom) ⟶ |r|)
7. b : bag(Atom)
⊢ (f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|

---

Latex:

---

Latex:
.....assertion..... 
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-(<\{x\}>+<\{y\}>)))  =  ((((1-<\{y\}>)*f(x:=0))+((1-<\{x\}>)*f(y:=0)))-f(x:=0)(y:=0))


By

---

Latex:
TACTIC:((FpsNorm  0  THENA  Auto)
                THEN  (RWO  "fps-mul-single-general"  0  THENA  Auto)\mcdot{}
                THEN  (RWO  "fps-mul-comm"  0
                            THENA  (Try  (QuickAuto)
                                          THEN  Try  (Fold  `member`  0)
                                          THEN  RepUR  ``power-series  fps-neg  fps-add  fps-coeff``  0
                                          THEN  Auto)
                            )
                THEN  (RWO  "fps-mul-single-general"  0
                            THENA  (Try  (QuickAuto)
                                          THEN  Try  (Fold  `member`  0)
                                          THEN  RepUR  ``power-series  fps-neg  fps-add  fps-coeff``  0
                                          THEN  Auto)
                            )
                THEN  RepUR  ``fps-Pascal  fps-elim-x  fps-elim  fps-add  fps-coeff  fps-neg  fps-sub``  0
                THEN  RepUR  ``power-series``  0
                THEN  Auto
                THEN  Try  ((Unfold  `power-series`  0  THEN  Auto)))

---

Home Index