---

Step * 2 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. 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])
∈ ℤ
BY
{ (Assert ⌜∀r:polyform(n)
             (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 );r;p)@[u / v]
             = ((p@[u / v] * q@[u / v]) + (r@[u / v] * u^||p||))
             ∈ ℤ)⌝⋅
THENM ((Assert p@[u / v] ∈ ℤ BY
              ((Assert p ∈ polyform(n) BY (RecUnfold `polyform` 0 THEN Auto)) THEN Auto))
       THEN (Assert q@[u / v] ∈ ℤ BY
                   ((Assert q ∈ polyform(n) BY (RecUnfold `polyform` 0 THEN Auto)) THEN Auto))
       THEN (RWO "-3" 0 THENA Auto)
       THEN RWO "polyconst-val" 0
       THEN Auto)
) }

1
.....assertion..... 
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 ∈ ℤ)
⊢ ∀r:polyform(n)
    (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 );r;p)@[u / v]
    = ((p@[u / v] * q@[u / v]) + (r@[u / v] * u^||p||))
    ∈ ℤ)

---

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.  p  :  polyform(n  -  1)  List
8.  q  :  polyform(n  -  1)  List
9.  \mneg{}(n  =  0)
\mvdash{}  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(\mlambda{}x.mul-polynom(n  -  1;a;x);q)  fi  );polyconst(n;0);p)@[u  / 
                                                                                                                                                                                                v]
=  (p@[u  /  v]  *  q@[u  /  v])


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}r:polyform(n)
                      (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(\mlambda{}x.mul-polynom(n  -  1;a;x);q)  fi  );r;p)@[u  /  v]
                      =  ((p@[u  /  v]  *  q@[u  /  v])  +  (r@[u  /  v]  *  u\^{}||p||)))\mkleeneclose{}\mcdot{}
THENM  ((Assert  p@[u  /  v]  \mmember{}  \mBbbZ{}  BY
                            ((Assert  p  \mmember{}  polyform(n)  BY  (RecUnfold  `polyform`  0  THEN  Auto))  THEN  Auto))
              THEN  (Assert  q@[u  /  v]  \mmember{}  \mBbbZ{}  BY
                                      ((Assert  q  \mmember{}  polyform(n)  BY  (RecUnfold  `polyform`  0  THEN  Auto))  THEN  Auto))
              THEN  (RWO  "-3"  0  THENA  Auto)
              THEN  RWO  "polyconst-val"  0
              THEN  Auto)
)

---

Home Index