---

Step * of Lemma fps-deriv-single

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[b:bag(X)]. ∀[x:X].
  (d<b>/dx = (int-to-ring(r;(#x in b)))*<bag-drop(eq;b;x)> ∈ PowerSeries(X;r))
BY
{ (Auto
   THEN BLemma `fps-ext`
   THEN Auto
   THEN RepUR ``fps-scalar-mul fps-deriv fps-coeff fps-single`` 0
   THEN Auto
   THEN (InstLemma `bag-drop-property` [⌜X⌝;⌜eq⌝;⌜x⌝;⌜b⌝]⋅ THENA Auto)
   THEN AutoSplit) }

1
1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. b : bag(X)
5. x : X
6. b1 : bag(X)
7. (b = ({x} + bag-drop(eq;b;x)) ∈ bag(X)) ∨ ((¬x ↓∈ b) ∧ (b = bag-drop(eq;b;x) ∈ bag(X)))
8. x.b1 = b ∈ bag(X)
⊢ (int-to-ring(r;(#x in b1) + 1) * 1)
= (int-to-ring(r;(#x in b)) * if bag-eq(eq;b1;bag-drop(eq;b;x)) then 1 else 0 fi )
∈ |r|

2
1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. b : bag(X)
5. x : X
6. b1 : bag(X)
7. ¬(x.b1 = b ∈ bag(X))
8. (b = ({x} + bag-drop(eq;b;x)) ∈ bag(X)) ∨ ((¬x ↓∈ b) ∧ (b = bag-drop(eq;b;x) ∈ bag(X)))
⊢ (int-to-ring(r;(#x in b1) + 1) * 0)
= (int-to-ring(r;(#x in b)) * if bag-eq(eq;b1;bag-drop(eq;b;x)) then 1 else 0 fi )
∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[b:bag(X)].  \mforall{}[x:X].
    (d<b>/dx  =  (int-to-ring(r;(\#x  in  b)))*<bag-drop(eq;b;x)>)


By

---

Latex:
(Auto
  THEN  BLemma  `fps-ext`
  THEN  Auto
  THEN  RepUR  ``fps-scalar-mul  fps-deriv  fps-coeff  fps-single``  0
  THEN  Auto
  THEN  (InstLemma  `bag-drop-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  AutoSplit)

---

Home Index