---

Step * of Lemma poly_int_val_cons_cons

∀n:ℕ. ∀p:polyform(n) List. ∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . ∀a:ℤ. ∀u:polyform(n).
  ([u / p]@[a / l] = ((u@l * a^||p||) + p@[a / l]) ∈ ℤ)
BY
{ (((UnivCD THENA Auto) THEN (RWO "poly_int_val_cons" 0 THENA Auto))
   THEN (RW  (AddrC [2] (LemmaC  `sum_split_first`)) 0 THENA Auto)
   THEN Reduce 0
   THEN RepeatFor 3 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}p:polyform(n)  List.  \mforall{}l:\{l:\mBbbZ{}  List|  ||l||  =  n\}  .  \mforall{}a:\mBbbZ{}.  \mforall{}u:polyform(n).
    ([u  /  p]@[a  /  l]  =  ((u@l  *  a\^{}||p||)  +  p@[a  /  l]))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  (RWO  "poly\_int\_val\_cons"  0  THENA  Auto))
  THEN  (RW    (AddrC  [2]  (LemmaC    `sum\_split\_first`))  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index