---

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


1. n : ℕ
2. u : ℤ
3. v : ℤ List
4. ||[u / v]|| = n ∈ ℤ
5. q : polyform(n - 1) List
6. ¬(n = 0 ∈ ℤ)
7. ||v|| = (n - 1) ∈ ℤ
8. ∀[p,q:polyform(n - 1)].  (v@mul-polynom(n - 1;p;q) = (v@p * v@q) ∈ ℤ)
9. r : polyform(n)
⊢ [u / v]@r = ((0 * [u / v]@q) + ([u / v]@r * 1)) ∈ ℤ
BY
{ ((InstLemma `poly-int-val_wf` [⌜n⌝;⌜[u / v]⌝;⌜q⌝]⋅ THEN Auto) THEN RecUnfold `polyform` 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `poly-int-val\_wf`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}[u  /  v]\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  RecUnfold  `polyform`  0  THEN  Auto)

---

Home Index