---

Step * 1 1 2 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 - 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)
∈ ℤ
BY
{ ((D 2 With ⌜n - 1⌝  THENA Auto)
   THEN DVar `l'
   THEN (DVar `l'
         THENL [(Assert ⌜False⌝⋅ THEN Auto THEN Reduce 2⋅ THEN Auto)
               ; ((Assert ||v|| = (n - 1) ∈ ℤ BY (All Reduce THEN Auto)) THEN (D -2 With ⌜v⌝  THENA Auto))]
   )) }

1
1. n : ℕ
2. u : ℤ
3. v : ℤ List
4. ||[u / v]|| = n ∈ ℤ
5. p : polyform(n - 1) List
6. q : polyform(n - 1) List
7. ¬(n = 0 ∈ ℤ)
8. ||v|| = (n - 1) ∈ ℤ
9. ∀[p,q:polyform(n - 1)].  (v@mul-polynom(n - 1;p;q) = (v@p * v@q) ∈ ℤ)
⊢ [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 );polyconst(n;0);p)
= ([u / v]@p * [u / v]@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  -  1)  List
5.  q  :  polyform(n  -  1)  List
6.  \mneg{}(n  =  0)
\mvdash{}  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(\mlambda{}x.mul-polynom(n  -  1;a;x);q)  fi  );polyconst(n;0);p)
=  (l@p  *  l@q)


By

---

Latex:
((D  2  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
  THEN  DVar  `l'
  THEN  (DVar  `l'
              THENL  [(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Reduce  2\mcdot{}  THEN  Auto)
                          ;  ((Assert  ||v||  =  (n  -  1)  BY
                                              (All  Reduce  THEN  Auto))
                                THEN  (D  -2  With  \mkleeneopen{}v\mkleeneclose{}    THENA  Auto)
                                )]
  ))

---

Home Index