---

Step * 2 1 1 1 1 1 of Lemma mul-polynom-int-val


1. n : {1...}
2. u : ℤ
3. v : ℤ List
4. ∀[p,q:polyform(n - 1)].  (mul-polynom(n - 1;p;q)@v = (p@v * q@v) ∈ ℤ)
5. ||[u / v]|| = n ∈ ℤ
6. ||v|| = (n - 1) ∈ ℤ
7. q : polyform(n - 1) List
8. ¬(n = 0 ∈ ℤ)
9. r : polyform(n)
⊢ r@[u / v] = (([]@[u / v] * q@[u / v]) + (r@[u / v] * 1)) ∈ ℤ
BY
{ (RWO  "poly_int_val_nil_cons polyconst-val" 0 THEN Try (Complete (Auto))) }

1
1. n : {1...}
2. u : ℤ
3. v : ℤ List
4. ∀[p,q:polyform(n - 1)].  (mul-polynom(n - 1;p;q)@v = (p@v * q@v) ∈ ℤ)
5. ||[u / v]|| = n ∈ ℤ
6. ||v|| = (n - 1) ∈ ℤ
7. q : polyform(n - 1) List
8. ¬(n = 0 ∈ ℤ)
9. r : polyform(n)
⊢ r@[u / v] = ((0 * q@[u / v]) + (r@[u / v] * 1)) ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  \mforall{}[p,q:polyform(n  -  1)].    (mul-polynom(n  -  1;p;q)@v  =  (p@v  *  q@v))
5.  ||[u  /  v]||  =  n
6.  ||v||  =  (n  -  1)
7.  q  :  polyform(n  -  1)  List
8.  \mneg{}(n  =  0)
9.  r  :  polyform(n)
\mvdash{}  r@[u  /  v]  =  (([]@[u  /  v]  *  q@[u  /  v])  +  (r@[u  /  v]  *  1))


By

---

Latex:
(RWO    "poly\_int\_val\_nil\_cons  polyconst-val"  0  THEN  Try  (Complete  (Auto)))

---

Home Index