---

Step * 1 1 2 1 2 2 1 1 of Lemma fps-Pascal-iff


1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. b : bag(Atom)
7. ((f (({x} + {y}) + b)) +r ((-r (f ({x} + b))) +r (-r (f ({y} + b))))) = 0 ∈ |r|
⊢ (f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|
BY
{ (CRngAdd ⌜(f ({x} + b)) +r (f ({y} + b))⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  f  :  PowerSeries(r)
5.  \mneg{}(x  =  y)
6.  b  :  bag(Atom)
7.  ((f  ((\{x\}  +  \{y\})  +  b))  +r  ((-r  (f  (\{x\}  +  b)))  +r  (-r  (f  (\{y\}  +  b)))))  =  0
\mvdash{}  (f  ((\{x\}  +  \{y\})  +  b))  =  ((f  (\{x\}  +  b))  +r  (f  (\{y\}  +  b)))


By

---

Latex:
(CRngAdd  \mkleeneopen{}(f  (\{x\}  +  b))  +r  (f  (\{y\}  +  b))\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index