---

Step * 2 1 1 1 1 2 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. u1 : polyform(n - 1)
10. v1 : polyform(n - 1) List
11. ∀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;v1)@[u / v]
      = ((v1@[u / v] * q@[u / v]) + (r@[u / v] * u^||v1||))
      ∈ ℤ)
12. r : polyform(n)
⊢ let y' ⟵ 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 )
  in 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 );y';v1)@[u / v]
= (([u1 / v1]@[u / v] * q@[u / v]) + (r@[u / v] * u^||v1|| + 1))
∈ ℤ
BY
{ ((Assert 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) BY
          (RecUnfold `polyform` (-1)
           THEN (SplitOnHypITE -1  THENA Auto)
           THEN Try (Trivial)
           THEN MemCD
           THEN Try ((RecUnfold `polyform` 0 THEN SplitOnConclITE))
           THEN Auto))
   THEN (CallByValueReduce 0 THENA 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. u1 : polyform(n - 1)
10. v1 : polyform(n - 1) List
11. ∀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;v1)@[u / v]
      = ((v1@[u / v] * q@[u / v]) + (r@[u / v] * 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)
⊢ 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 / v] * u^||v1|| + 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.  u1  :  polyform(n  -  1)
10.  v1  :  polyform(n  -  1)  List
11.  \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;v1)@[u  /  v]
            =  ((v1@[u  /  v]  *  q@[u  /  v])  +  (r@[u  /  v]  *  u\^{}||v1||)))
12.  r  :  polyform(n)
\mvdash{}  let  y'  \mleftarrow{}{}  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  )
    in  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  );y';v1)@[u  /  v]
=  (([u1  /  v1]@[u  /  v]  *  q@[u  /  v])  +  (r@[u  /  v]  *  u\^{}||v1||  +  1))


By

---

Latex:
((Assert  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)  BY
                (RecUnfold  `polyform`  (-1)
                  THEN  (SplitOnHypITE  -1    THENA  Auto)
                  THEN  Try  (Trivial)
                  THEN  MemCD
                  THEN  Try  ((RecUnfold  `polyform`  0  THEN  SplitOnConclITE))
                  THEN  Auto))
  THEN  (CallByValueReduce  0  THENA  Auto)
  )

---

Home Index