---

Step * of Lemma fps-elim-x-atom

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x,y:X].
  (atom(y)(x:=0) = if eq x y then 0 else atom(y) fi  ∈ PowerSeries(X;r))
BY
{ (Auto
   THEN (BLemma `fps-ext` THEN Try (QuickAuto))
   THEN Auto
   THEN RepUR ``fps-elim-x fps-elim fps-atom fps-single fps-coeff fps-zero`` 0
   THEN Repeat (AutoSplit)) }

1
1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. x : X
5. y : X
6. ¬(x = y ∈ X)
7. b : bag(X)
8. x ↓∈ b
9. b = {y} ∈ bag(X)
⊢ 0 = 1 ∈ |r|

2
1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. x : X
5. y : X
6. b : bag(X)
7. ¬x ↓∈ b
8. b = {y} ∈ bag(X)
9. x = y ∈ X
⊢ 1 = 0 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x,y:X].
    (atom(y)(x:=0)  =  if  eq  x  y  then  0  else  atom(y)  fi  )


By

---

Latex:
(Auto
  THEN  (BLemma  `fps-ext`  THEN  Try  (QuickAuto))
  THEN  Auto
  THEN  RepUR  ``fps-elim-x  fps-elim  fps-atom  fps-single  fps-coeff  fps-zero``  0
  THEN  Repeat  (AutoSplit))

---

Home Index