---

Step * of Lemma fps-pascal-elim

∀[r:CRng]. ∀[x,y:Atom].  Δ(x,y)(x:=0) = (1÷(1-atom(y))) ∈ PowerSeries(r) supposing (¬(x = y ∈ Atom)) ∧ (¬(1 = 0 ∈ |r|))
BY
{ (Auto
   THEN (RepUR ``fps-pascal fps-elim-x`` 0 THEN Try (Fold `fps-atom` 0))
   THEN RWO "fps-elim-div" 0
   THEN Auto
   THEN All (Fold `fps-elim-x`)
   THEN RWW "fps-elim-x-one fps-elim-x-add fps-elim-x-sub fps-elim-x-atom" 0
   THEN Auto
   THEN Try ((RepeatFor 2 (AutoSplit) THEN FpsNorm 0 THEN Auto))) }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. ¬(1 = 0 ∈ |r|)
⊢ ¬(1 = 0 ∈ PowerSeries(r))

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

3
1. r : CRng
2. x : Atom
3. y : Atom
4. x ≠ y ∈ Atom 
5. ¬(x = y ∈ Atom)
6. ¬(1 = 0 ∈ |r|)
7. ↑(AtomDeq x x)
⊢ (1÷(-(atom(y))+(1-0))) = (1÷(-(atom(y))+1)) ∈ PowerSeries(r)

4
1. r : CRng
2. x : Atom
3. ¬↑(AtomDeq x x)
4. y : Atom
5. x ≠ y ∈ Atom 
6. ¬(x = y ∈ Atom)
7. ¬(1 = 0 ∈ |r|)
⊢ (1÷(-(atom(x))+(-(atom(y))+1))) = (1÷(-(atom(y))+1)) ∈ PowerSeries(r)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].    \mDelta{}(x,y)(x:=0)  =  (1\mdiv{}(1-atom(y)))  supposing  (\mneg{}(x  =  y))  \mwedge{}  (\mneg{}(1  =  0))


By

---

Latex:
(Auto
  THEN  (RepUR  ``fps-pascal  fps-elim-x``  0  THEN  Try  (Fold  `fps-atom`  0))
  THEN  RWO  "fps-elim-div"  0
  THEN  Auto
  THEN  All  (Fold  `fps-elim-x`)
  THEN  RWW  "fps-elim-x-one  fps-elim-x-add  fps-elim-x-sub  fps-elim-x-atom"  0
  THEN  Auto
  THEN  Try  ((RepeatFor  2  (AutoSplit)  THEN  FpsNorm  0  THEN  Auto)))

---

Home Index