---

Step * 1 1 1 of Lemma polynomial-deriv-seq


1. I : Interval
2. n : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. i : ℕn
5. n - i ≠ 0
6. ¬n < i + 1
7. ¬n < i
8. d((Σi≤n - i. poly-nth-deriv(i;a)_i * x^i))/dx = λx.rpoly-deriv(n - i;poly-nth-deriv(i;a);x) on I
9. x : Base
⊢ poly-nth-deriv(i + 1;a) ~ poly-deriv(poly-nth-deriv(i;a))
BY
{ ((Unfold `poly-nth-deriv` 0 THEN (RW (AddrC [1] (LemmaC `primrec-unroll`)) 0  THENA Auto)) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  n  :  \mBbbN{}
3.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
4.  i  :  \mBbbN{}n
5.  n  -  i  \mneq{}  0
6.  \mneg{}n  <  i  +  1
7.  \mneg{}n  <  i
8.  d((\mSigma{}i\mleq{}n  -  i.  poly-nth-deriv(i;a)\_i  *  x\^{}i))/dx  =  \mlambda{}x.rpoly-deriv(n  -  i;poly-nth-deriv(i;a);x)  on  I
9.  x  :  Base
\mvdash{}  poly-nth-deriv(i  +  1;a)  \msim{}  poly-deriv(poly-nth-deriv(i;a))


By

---

Latex:
((Unfold  `poly-nth-deriv`  0  THEN  (RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0    THENA  Auto))
  THEN  AutoSplit
  )

---

Home Index