---

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


1. n : ℕ
2. ∀n:ℕn. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p,q:polyform(n)].  (l@mul-polynom(n;p;q) = (l@p * l@q) ∈ ℤ)
3. l : {l:ℤ List| ||l|| = n ∈ ℤ} 
4. p : polyform(n)
5. q : polyform(n)
⊢ l@if n=0
    then p * q
    else 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)
= (l@p * l@q)
∈ ℤ
BY
{ ((RecUnfold `polyform` (-2) THEN RecUnfold `polyform` (-1))
   THEN RepeatFor 2 ((SplitOnHypITE -2  THENA Auto))
   THEN Try (Trivial)
   THEN Thin (-1)
   THEN Reduce 0) }

1
1. n : ℕ
2. ∀n:ℕn. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p,q:polyform(n)].  (l@mul-polynom(n;p;q) = (l@p * l@q) ∈ ℤ)
3. l : {l:ℤ List| ||l|| = n ∈ ℤ} 
4. p : ℤ
5. q : ℤ
6. n = 0 ∈ ℤ
⊢ l@p * q = (l@p * l@q) ∈ ℤ

2
1. n : ℕ
2. ∀n:ℕn. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p,q:polyform(n)].  (l@mul-polynom(n;p;q) = (l@p * l@q) ∈ ℤ)
3. l : {l:ℤ List| ||l|| = n ∈ ℤ} 
4. p : polyform(n - 1) List
5. q : polyform(n - 1) List
6. ¬(n = 0 ∈ ℤ)
⊢ l@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)
= (l@p * l@q)
∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mforall{}n:\mBbbN{}n.  \mforall{}[l:\{l:\mBbbZ{}  List|  ||l||  =  n\}  ].  \mforall{}[p,q:polyform(n)].    (l@mul-polynom(n;p;q)  =  (l@p  *  l@q))
3.  l  :  \{l:\mBbbZ{}  List|  ||l||  =  n\} 
4.  p  :  polyform(n)
5.  q  :  polyform(n)
\mvdash{}  l@if  n=0
        then  p  *  q
        else  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)
=  (l@p  *  l@q)


By

---

Latex:
((RecUnfold  `polyform`  (-2)  THEN  RecUnfold  `polyform`  (-1))
  THEN  RepeatFor  2  ((SplitOnHypITE  -2    THENA  Auto))
  THEN  Try  (Trivial)
  THEN  Thin  (-1)
  THEN  Reduce  0)

---

Home Index