Nuprl 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))))
Proof
Definitions occuring in Statement :
mul-polynom: mul-polynom(n;p;q),
minus-polynom: minus-polynom(n;p),
polyconst: polyconst(n;k),
add-polynom: add-polynom(n;rmz;p;q),
polynom: polynom(n),
nat: ℕ,
btrue: tt,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
top: Top,
not: ¬A,
false: False,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
or: P ∨ Q,
decidable: Dec(P),
ge: i ≥ j ,
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
guard: {T},
true: True,
squash: ↓T,
so_apply: x[s],
nat: ℕ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
prop: ℙ,
all: ∀x:A. B[x],
uimplies: b supposing a,
uiff: uiff(P;Q),
cand: A c∧ B,
and: P ∧ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
minus-polynom-val,
add_functionality_wrt_eq,
true_wf,
squash_wf,
mul-polynom_wf,
add-inverse,
minus-polynom_wf,
add-polynom_wf1,
int_term_value_mul_lemma,
itermMultiply_wf,
mul-polynom-int-val,
mul-polynom_wf2,
minus-polynom_wf2,
int_formula_prop_wf,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_term_value_add_lemma,
int_formula_prop_eq_lemma,
int_formula_prop_not_lemma,
itermConstant_wf,
itermVar_wf,
itermAdd_wf,
intformeq_wf,
intformnot_wf,
satisfiable-full-omega-tt,
le_wf,
decidable__equal_int,
nat_properties,
polyconst-val,
iff_weakening_equal,
poly-int-val_wf2,
btrue_wf,
polynom_subtype_polyform,
add-polynom-int-val,
equal_wf,
polyconst_wf,
equal-wf-base-T,
list_wf,
set_wf,
add-polynom_wf,
polynom-equal-iff
Rules used in proof :
universeEquality,
multiplyEquality,
minusEquality,
addEquality,
independent_pairEquality,
computeAll,
voidEquality,
voidElimination,
int_eqEquality,
dependent_pairFormation,
unionElimination,
dependent_functionElimination,
independent_functionElimination,
imageMemberEquality,
equalitySymmetry,
equalityTransitivity,
dependent_set_memberEquality,
imageElimination,
natural_numberEquality,
independent_pairFormation,
axiomEquality,
isect_memberEquality,
rename,
setElimination,
because_Cache,
applyEquality,
baseClosed,
closedConclusion,
baseApply,
lambdaEquality,
sqequalRule,
intEquality,
lambdaFormation,
independent_isectElimination,
productElimination,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[n:\mBbbN{}]
((\mforall{}[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)))
\mwedge{} (\mforall{}[p:polynom(n)]. (add-polynom(n;tt;p;polyconst(n;0)) = p))
\mwedge{} (\mforall{}[p,q:polynom(n)]. (add-polynom(n;tt;p;q) = add-polynom(n;tt;q;p)))
\mwedge{} (\mforall{}[p:polynom(n)]. (add-polynom(n;tt;p;minus-polynom(n;p)) = polyconst(n;0)))
\mwedge{} (\mforall{}[p,q,r:polynom(n)].
(mul-polynom(n;p;mul-polynom(n;q;r)) = mul-polynom(n;mul-polynom(n;p;q);r)))
\mwedge{} (\mforall{}[p:polynom(n)]. (mul-polynom(n;p;polyconst(n;1)) = p))
\mwedge{} (\mforall{}[p,q:polynom(n)]. (mul-polynom(n;p;q) = mul-polynom(n;q;p)))
\mwedge{} (\mforall{}[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)))))
Date html generated:
2017_04_20-AM-07_16_52
Last ObjectModification:
2017_04_19-PM-01_59_37
Theory : list_1
Home
Index