Definition: polyform
polyform(n)==r if (n =z 0) then ℤ else polyform(n - 1) List fi
Lemma: polyform_wf
∀[n:ℕ]. (polyform(n) ∈ Type)
Lemma: valueall-type-polyform
∀[n:ℕ]. valueall-type(polyform(n))
Lemma: polyform-value-type
∀[n:ℕ]. value-type(polyform(n))
Definition: poly-zero
poly-zero(n;p) == if (n =z 0) then (p =z 0) else null(p) fi
Lemma: poly-zero_wf
∀[n:ℕ]. ∀[p:polyform(n)]. (poly-zero(n;p) ∈ 𝔹)
Definition: polyform-lead-nonzero
polyform-lead-nonzero(n;p) == 0 < n ⇒ 0 < ||p|| ⇒ (¬↑poly-zero(n - 1;hd(p)))
Lemma: polyform-lead-nonzero_wf
∀[n:ℕ]. ∀[p:polyform(n)]. (polyform-lead-nonzero(n;p) ∈ ℙ)
Lemma: sq_stable__polyform-lead-nonzero
∀n:ℕ. ∀p:polyform(n). SqStable(polyform-lead-nonzero(n;p))
Definition: polynom
polynom(n)==r if (n =z 0) then ℤ else {p:polynom(n - 1) List| polyform-lead-nonzero(n;p)} fi
Lemma: polynom_wf
∀[n:ℕ]. (polynom(n) ∈ Type)
Lemma: polynom_subtype_polyform
∀[n:ℕ]. (polynom(n) ⊆r polyform(n))
Lemma: valueall-type-polynom
∀[n:ℕ]. valueall-type(polynom(n))
Lemma: value-type-polynom
∀[n:ℕ]. value-type(polynom(n))
Lemma: polynom-subtype-list
∀[n:ℕ+]. (polynom(n) ⊆r (polynom(n - 1) List))
Definition: poly-int-val
l@p==r if null(l) then p else let a,as = l in Σ(as@p[i] * a^(||p|| - 1 - i) | i < ||p||) fi
Lemma: poly-int-val_wf
∀[n:ℕ]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p:polyform(n)]. (l@p ∈ ℤ)
Lemma: poly_int_val_cons
∀p,l,a:Top. ([a / l]@p ~ Σ(l@p[i] * a^(||p|| - 1 - i) | i < ||p||))
Lemma: poly_int_val_cons_cons
∀n:ℕ. ∀p:polyform(n) List. ∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . ∀a:ℤ. ∀u:polyform(n).
([a / l]@[u / p] = ((l@u * a^||p||) + [a / l]@p) ∈ ℤ)
Lemma: poly_int_val_cons_cons-sq
∀n:ℕ. ∀p:polyform(n) List. ∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . ∀a:ℤ. ∀u:polyform(n).
([a / l]@[u / p] ~ (l@u * a^||p||) + [a / l]@p)
Lemma: poly_int_val_nil_cons
∀l,a:Top. ([a / l]@[] ~ 0)
Definition: rm-zeros
rm-zeros(n;p) == rec-case(p) of [] => [] | a::as => r.if poly-zero(n;a) then r else [a / as] fi
Lemma: rm-zeros_wf
∀[n:ℕ+]. ∀[p:polynom(n - 1) List]. (rm-zeros(n - 1;p) ∈ polynom(n))
Definition: add-polyn
add-polyn(n;p;q)
==r if (n =z 0)
then p + q
else if p = Ax then q
otherwise if q = Ax then p otherwise eval rp = rev(p) in
eval rq = rev(q) in
eval cs = list_accum2(sofar,a,b.eval c = add-polyn(n - 1;a;b) in
[c / sofar];sofar,a.[a / sofar];sofar,b.[b\000C / sofar];[];rp;rq) in
rm-zeros(n - 1;cs)
fi
Definition: add-polynom
add-polynom(n;rmz;p;q)
==r if (n =z 0)
then p + q
else let pp ⟵ p
in let qq ⟵ q
in if null(pp) then qq
if null(qq) then pp
else eval m = ||pp|| in
eval k = ||qq|| in
if (m) < (k)
then let b,bs = qq
in let cs ⟵ add-polynom(n;ff;pp;bs)
in [b / cs]
else if (k) < (m)
then let a,as = pp
in let cs ⟵ add-polynom(n;ff;as;qq)
in [a / cs]
else let a,as = p
in let b,bs = q
in let c ⟵ add-polynom(n - 1;tt;a;b)
in let cs ⟵ add-polynom(n;ff;as;bs)
in if rmz then rm-zeros(n - 1;[c / cs]) else [c / cs] fi
fi
fi
Lemma: add-polynom_wf1
∀[n:ℕ]. ∀[p,q:polyform(n)]. ∀[rmz:𝔹]. (add-polynom(n;rmz;p;q) ∈ polyform(n))
Lemma: add-polynom_wf
∀[n:ℕ]. ∀[p,q:polynom(n)]. (add-polynom(n;tt;p;q) ∈ polynom(n))
Lemma: add-polynom-length
∀[n:ℕ]. ∀[p,q:polyform(n) List]. (||add-polynom(n + 1;ff;p;q)|| = imax(||p||;||q||) ∈ ℤ)
Lemma: add-polynom-int-val
∀[n:ℕ]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p,q:polyform(n)]. ∀[rmz:𝔹]. (l@add-polynom(n;rmz;p;q) = (l@p + l@q) ∈ ℤ)
Lemma: add-polynom-int-val-sq
∀[n:ℕ]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p,q:polyform(n)]. ∀[rmz:𝔹]. (l@add-polynom(n;rmz;p;q) ~ l@p + l@q)
Lemma: poly-zero-implies
∀n:ℕ. ∀p:polyform(n). ((↑poly-zero(n;p)) ⇒ (∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . (l@p = 0 ∈ ℤ)))
Lemma: poly-int-val_wf2
∀[n:ℕ]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p:polynom(n)]. (l@p ∈ ℤ)
Lemma: poly-zero-false
∀n:ℕ. ∀p:polynom(n). (¬↑poly-zero(n;p) ⇐⇒ ∃l:{l:ℤ List| ||l|| = n ∈ ℤ} . (¬(l@p = 0 ∈ ℤ)))
Lemma: assert-poly-zero
∀n:ℕ. ∀p:polynom(n). (↑poly-zero(n;p) ⇐⇒ ∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . (l@p = 0 ∈ ℤ))
Definition: polyconst
polyconst(n;k)==r if n=0 then k else if k=0 then [] else eval m = n - 1 in eval c = polyconst(m;k) in [c]
Lemma: polyconst_wf
∀[n:ℕ]. ∀[k:ℤ]. (polyconst(n;k) ∈ polyform(n))
Lemma: polyconst-val
∀[n:ℕ]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[k:ℤ]. (l@polyconst(n;k) ~ k)
Lemma: polyconst_wf2
∀[n:ℕ]. ∀[k:ℤ]. (polyconst(n;k) ∈ polynom(n))
Definition: minus-polynom
minus-polynom(n;p)==r if n=0 then -p else map-rev(λq.minus-polynom(n - 1;q);p)
Lemma: minus-polynom_wf
∀[n:ℕ]. ∀[p:polyform(n)]. (minus-polynom(n;p) ∈ polyform(n))
Lemma: length-minus-polynom
∀[n:ℕ+]. ∀[p:polyform(n)]. (||minus-polynom(n;p)|| = ||p|| ∈ ℤ)
Lemma: minus-polynom-val
∀[n:ℕ]. ∀[p:polyform(n)]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. (l@minus-polynom(n;p) = (-l@p) ∈ ℤ)
Lemma: minus-polynom_wf2
∀[n:ℕ]. ∀[p:polynom(n)]. (minus-polynom(n;p) ∈ polynom(n))
Definition: mult-polynom
mult-polynom(n;p;q)
==r eval pp = p in
eval qq = q in
if poly-zero(n;pp) then pp
if poly-zero(n;qq) then qq
else eval zero = polyconst(n;0) in
if n=0
then pp * qq
else eval m = n - 1 in
cbv_list_accum(z,a.eval zero' = polyconst(m;0) in
eval z' = if null(z) then [] else eager-append(z;[zero']) fi in
eval aq = if poly-zero(m;a) then [] else map-rev(λx.mult-polynom(m;a;x);qq) fi in
add-polyn(n;z';aq);zero;pp)
fi
Definition: mul-polynom
mul-polynom(n;p;q)
==r eval pp = p in
eval qq = q in
if poly-zero(n;pp) then pp
if poly-zero(n;qq) then qq
else eval zero = polyconst(n;0) in
if n=0
then pp * qq
else eval m = n - 1 in
eager-accum(z,a.add-polynom(n;tt;if null(z) then [] else z @ [polyconst(m;0)] fi ;if poly-zero(m;a)
then []
else map(λx.mul-polynom(m;a;x);qq)
fi );zero;pp)
fi
Lemma: mul-polynom_wf
∀[n:ℕ]. ∀[p,q:polyform(n)]. (mul-polynom(n;p;q) ∈ polyform(n))
Lemma: mul-polynom-int-val
∀[n:ℕ]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. ∀[p,q:polyform(n)]. (l@mul-polynom(n;p;q) = (l@p * l@q) ∈ ℤ)
Lemma: nonzero-mul-polynom
∀[n:ℕ]. ∀[p,q:polynom(n)].
(poly-zero(n;mul-polynom(n;p;q)) = ff) supposing (poly-zero(n;q) = ff and poly-zero(n;p) = ff)
Lemma: mul-polynom_wf2
∀[n:ℕ]. ∀[p,q:polynom(n)]. (mul-polynom(n;p;q) ∈ polynom(n))
Lemma: polynom-equal-iff
∀[n:ℕ]. ∀[p,q:polynom(n)]. uiff(p = q ∈ polynom(n);∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . (l@p = l@q ∈ ℤ))
Lemma: polynom-is-comm-ring
∀[n:ℕ]
((∀[p,q,r:polynom(n)].
(add-polynom(n;tt;p;add-polynom(n;tt;q;r)) = add-polynom(n;tt;add-polynom(n;tt;p;q);r) ∈ polynom(n)))
∧ (∀[p:polynom(n)]. (add-polynom(n;tt;p;polyconst(n;0)) = p ∈ polynom(n)))
∧ (∀[p,q:polynom(n)]. (add-polynom(n;tt;p;q) = add-polynom(n;tt;q;p) ∈ polynom(n)))
∧ (∀[p:polynom(n)]. (add-polynom(n;tt;p;minus-polynom(n;p)) = polyconst(n;0) ∈ polynom(n)))
∧ (∀[p,q,r:polynom(n)]. (mul-polynom(n;p;mul-polynom(n;q;r)) = mul-polynom(n;mul-polynom(n;p;q);r) ∈ polynom(n)))
∧ (∀[p:polynom(n)]. (mul-polynom(n;p;polyconst(n;1)) = p ∈ polynom(n)))
∧ (∀[p,q:polynom(n)]. (mul-polynom(n;p;q) = mul-polynom(n;q;p) ∈ polynom(n)))
∧ (∀[p,q,r:polynom(n)].
(mul-polynom(n;p;add-polynom(n;tt;q;r)) = add-polynom(n;tt;mul-polynom(n;p;q);mul-polynom(n;p;r)) ∈ polynom(n))))
Definition: compose-polynom
compose-polynom(n;p;q) ==
if (n =z 0)
then q
else accumulate (with value z and list item a):
if poly-zero(n - 1;a) then mul-polynom(n;z;p) else add-polynom(n;tt;mul-polynom(n;z;p);[a]) fi
over list:
q
with starting value:
polyconst(n;0))
fi
Lemma: compose-polynom_wf
∀[n:ℕ]. ∀[p,q:polynom(n)]. (compose-polynom(n;p;q) ∈ polynom(n))
Definition: polyvar
polyvar(n;v)
==r if (v) < (0)
then []
else eval m = n - 1 in
if (m) < (v)
then []
else if v=0
then eval one = polyconst(m;1) in
eval zero = polyconst(m;0) in
[one; zero]
else eval v' = v - 1 in
eval a = polyvar(m;v') in
[a]
Lemma: polyvar_wf
∀[n:ℕ]. ∀[v:ℤ]. polyvar(n;v) ∈ polyform(n) supposing 0 < n
Lemma: polyvar_wf2
∀[n:ℕ]. ∀[v:ℤ]. polyvar(n;v) ∈ polynom(n) supposing 0 < n
Lemma: polyvar-val
∀[n:ℕ+]. ∀[v:ℤ]. ∀[l:{l:ℤ List| ||l|| = n ∈ ℤ} ]. (l@polyvar(n;v) = if 0 ≤z v ∧b v <z n then l[v] else 0 fi ∈ ℤ)
Home
Index