---

Step * 1 1 2 1 1 2 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. u1 : polyform(n - 1)
10. v1 : polyform(n - 1) List
11. ∀r:polyform(n)
      ([u / v]@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;v1)
      = (([u / v]@v1 * [u / v]@q) + ([u / v]@r * u^||v1||))
      ∈ ℤ)
12. r : polyform(n)
13. add-polynom(n;tt;if null(r) then [] else r @ [polyconst(n - 1;0)] fi ;if poly-zero(n - 1;u1)
    then []
    else map(λx.mul-polynom(n - 1;u1;x);q)
    fi ) ∈ polyform(n)
⊢ [u / v]@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 );add-polynom(n;tt;if null(r) then [] else r @ [polyconst(n - 1;0)] fi ;if poly-zero(n - 1;u1)
then []
else map(λx.mul-polynom(n - 1;u1;x);q)
fi );v1)
= (([u / v]@[u1 / v1] * [u / v]@q) + ([u / v]@r * u^(||v1|| + 1)))
∈ ℤ
BY
{ (((Assert [u1 / v1] ∈ polyform(n) BY
           (RecUnfold `polyform` 0 THEN Auto))
    THEN (Assert v1 ∈ polyform(n) BY
                (RecUnfold `polyform` 0 THEN Auto))
    )
   THEN (Assert q ∈ polyform(n) BY
               (RecUnfold `polyform` 0 THEN Auto))
   THEN (RWO "-6" 0 THENA Auto)) }

1
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. u1 : polyform(n - 1)
10. v1 : polyform(n - 1) List
11. ∀r:polyform(n)
      ([u / v]@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;v1)
      = (([u / v]@v1 * [u / v]@q) + ([u / v]@r * u^||v1||))
      ∈ ℤ)
12. r : polyform(n)
13. add-polynom(n;tt;if null(r) then [] else r @ [polyconst(n - 1;0)] fi ;if poly-zero(n - 1;u1)
    then []
    else map(λx.mul-polynom(n - 1;u1;x);q)
    fi ) ∈ polyform(n)
14. [u1 / v1] ∈ polyform(n)
15. v1 ∈ polyform(n)
16. q ∈ polyform(n)
⊢ (([u / v]@v1 * [u / v]@q)
+ ([u / v]@add-polynom(n;tt;if null(r) then [] else r @ [polyconst(n - 1;0)] fi ;if poly-zero(n - 1;u1)
  then []
  else map(λx.mul-polynom(n - 1;u1;x);q)
  fi )
  * u^||v1||))
= (([u / v]@[u1 / v1] * [u / v]@q) + ([u / v]@r * u^(||v1|| + 1)))
∈ ℤ

---

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.  u1  :  polyform(n  -  1)
10.  v1  :  polyform(n  -  1)  List
11.  \mforall{}r:polyform(n)
            ([u  /  v]@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;v1)
            =  (([u  /  v]@v1  *  [u  /  v]@q)  +  ([u  /  v]@r  *  u\^{}||v1||)))
12.  r  :  polyform(n)
13.  add-polynom(n;tt;if  null(r)  then  []  else  r  @  [polyconst(n  -  1;0)]  fi  ;if  poly-zero(n  -  1;u1)
        then  []
        else  map(\mlambda{}x.mul-polynom(n  -  1;u1;x);q)
        fi  )  \mmember{}  polyform(n)
\mvdash{}  [u  /  v]@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  );add-polynom(n;tt;if  null(r)  then  []  else  r  @  [polyconst(n  -  1;0)]  fi  ;if  poly-zero(n  -  1;u1)
then  []
else  map(\mlambda{}x.mul-polynom(n  -  1;u1;x);q)
fi  );v1)
=  (([u  /  v]@[u1  /  v1]  *  [u  /  v]@q)  +  ([u  /  v]@r  *  u\^{}(||v1||  +  1)))


By

---

Latex:
(((Assert  [u1  /  v1]  \mmember{}  polyform(n)  BY
                  (RecUnfold  `polyform`  0  THEN  Auto))
    THEN  (Assert  v1  \mmember{}  polyform(n)  BY
                            (RecUnfold  `polyform`  0  THEN  Auto))
    )
  THEN  (Assert  q  \mmember{}  polyform(n)  BY
                          (RecUnfold  `polyform`  0  THEN  Auto))
  THEN  (RWO  "-6"  0  THENA  Auto))

---

Home Index