---

Step * 2 of Lemma fps-pascal-elim


1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. ¬(1 = 0 ∈ |r|)
6. ¬(1(x:=0) = 0 ∈ PowerSeries(r))
⊢ ((1-(atom(x)+atom(y)))[{}] * 1) = 1 ∈ |r|
BY
{ xxx(FpsCompute 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  \mneg{}(x  =  y)
5.  \mneg{}(1  =  0)
6.  \mneg{}(1(x:=0)  =  0)
\mvdash{}  ((1-(atom(x)+atom(y)))[\{\}]  *  1)  =  1


By

---

Latex:
xxx(FpsCompute  0  THEN  Auto)xxx

---

Home Index