---

Step * 2 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) ∈ ℤ
⊢ ∀[p,q:polyform(n - 1) List].  (mul-polynom(n;p;q)@[u / v] = (p@[u / v] * q@[u / v]) ∈ ℤ)
BY
{ (Auto THEN RecUnfold `mul-polynom` 0 THEN (Decide ⌜n = 0 ∈ ℤ⌝⋅ THENA Auto) THEN Reduce 0 THEN 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. p : polyform(n - 1) List
8. q : polyform(n - 1) List
9. ¬(n = 0 ∈ ℤ)
⊢ eager-accum(z,a.add-polynom(n;tt;if null(z) then [] else z @ [polyconst(n - 1;0)] fi ;if poly-zero(n - 1;a)
then []
else map(λx.mul-polynom(n - 1;a;x);q)
fi );polyconst(n;0);p)@[u / v]
= (p@[u / v] * q@[u / v])
∈ ℤ

---

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)
\mvdash{}  \mforall{}[p,q:polyform(n  -  1)  List].    (mul-polynom(n;p;q)@[u  /  v]  =  (p@[u  /  v]  *  q@[u  /  v]))


By

---

Latex:
(Auto  THEN  RecUnfold  `mul-polynom`  0  THEN  (Decide  \mkleeneopen{}n  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index