Nuprl Lemma : mul-mono-poly-equiv
∀[m:iMonomial()]. ∀[p:iMonomial() List].
ipolynomial-term(mul-mono-poly(m;p)) ≡ imonomial-term(m) (*) ipolynomial-term(p)
Proof
Definitions occuring in Statement :
mul-mono-poly: mul-mono-poly(m;p),
ipolynomial-term: ipolynomial-term(p),
imonomial-term: imonomial-term(m),
iMonomial: iMonomial(),
equiv_int_terms: t1 ≡ t2,
itermMultiply: left (*) right,
list: T List,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
iMonomial: iMonomial(),
int_nzero: ℤ-o,
so_apply: x[s],
implies: P ⇒ Q,
mul-mono-poly: mul-mono-poly(m;p),
all: ∀x:A. B[x],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3],
uimplies: b supposing a,
prop: ℙ,
callbyvalueall: callbyvalueall,
has-value: (a)↓,
has-valueall: has-valueall(a),
equiv_int_terms: t1 ≡ t2,
ipolynomial-term: ipolynomial-term(p),
ifthenelse: if b then t else f fi ,
btrue: tt,
int_term_value: int_term_value(f;t),
itermConstant: "const",
int_term_ind: int_term_ind,
itermMultiply: left (*) right,
subtype_rel: A ⊆r B,
uiff: uiff(P;Q),
and: P ∧ Q,
rev_uimplies: rev_uimplies(P;Q),
itermAdd: left (+) right
Lemmas referenced :
list_induction,
iMonomial_wf,
equiv_int_terms_wf,
ipolynomial-term_wf,
mul-mono-poly_wf1,
itermMultiply_wf,
imonomial-term_wf,
list_wf,
list_ind_nil_lemma,
list_ind_cons_lemma,
valueall-type-has-valueall,
product-valueall-type,
int_nzero_wf,
sorted_wf,
subtype_rel_self,
set-valueall-type,
nequal_wf,
int-valueall-type,
list-valueall-type,
mul-monomials_wf,
evalall-reduce,
null_nil_lemma,
mul-commutes,
int_term_value_wf,
subtype_rel_product,
zero-mul,
cons_wf,
itermAdd_wf,
equiv_int_terms_functionality,
equiv_int_terms_transitivity,
ipolynomial-term-cons,
itermAdd_functionality,
mul-monomials-equiv,
itermMultiply_functionality,
equiv_int_terms_weakening,
int_term_wf,
equal_wf,
mul-distributes
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
thin,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesis,
sqequalRule,
lambdaEquality,
hypothesisEquality,
productElimination,
independent_pairEquality,
setElimination,
rename,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
lambdaFormation,
independent_isectElimination,
setEquality,
intEquality,
because_Cache,
natural_numberEquality,
callbyvalueReduce,
equalityTransitivity,
equalitySymmetry,
axiomEquality,
functionEquality,
applyEquality,
addEquality,
multiplyEquality
Latex:
\mforall{}[m:iMonomial()]. \mforall{}[p:iMonomial() List].
ipolynomial-term(mul-mono-poly(m;p)) \mequiv{} imonomial-term(m) (*) ipolynomial-term(p)
Date html generated:
2017_09_29-PM-05_53_33
Last ObjectModification:
2017_07_26-PM-01_42_49
Theory : omega
Home
Index