---

Step * 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@mul-polynom(n;p;q) = (l@p * l@q) ∈ ℤ
BY
{ (RecUnfold `mul-polynom` 0
   THEN RepeatFor 4 ((CallByValueReduce 0 THENA Auto))
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (((Subst' l@p = 0 ∈ ℤ 0 THENA (BLemma `poly-zero-implies`  THEN Complete (Auto)))
              THEN InstLemma `poly-int-val_wf` [⌜n⌝;⌜l⌝;⌜q⌝]⋅
              THEN Auto))
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (((Subst' l@q = 0 ∈ ℤ 0 THENA (BLemma `poly-zero-implies`  THEN Complete (Auto)))
              THEN InstLemma `poly-int-val_wf` [⌜n⌝;⌜l⌝;⌜p⌝]⋅
              THEN Auto))
   THEN RepeatFor 2 (Thin (-1))) }

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 : 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)
∈ ℤ

---

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@mul-polynom(n;p;q)  =  (l@p  *  l@q)


By

---

Latex:
(RecUnfold  `mul-polynom`  0
  THEN  RepeatFor  4  ((CallByValueReduce  0  THENA  Auto))
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (((Subst'  l@p  =  0  0  THENA  (BLemma  `poly-zero-implies`    THEN  Complete  (Auto)))
                        THEN  InstLemma  `poly-int-val\_wf`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
                        THEN  Auto))
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (((Subst'  l@q  =  0  0  THENA  (BLemma  `poly-zero-implies`    THEN  Complete  (Auto)))
                        THEN  InstLemma  `poly-int-val\_wf`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
                        THEN  Auto))
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index