Nuprl Lemma : mul_ipoly_wf
∀[p,q:iPolynomial()]. (mul_ipoly(p;q) ∈ iPolynomial())
Proof
Definitions occuring in Statement :
mul_ipoly: mul_ipoly(p;q),
iPolynomial: iPolynomial(),
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
iPolynomial: iPolynomial()
Lemmas referenced :
mul_poly-sq,
mul-ipoly_wf,
iPolynomial_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setElimination,
rename,
hypothesisEquality,
hypothesis
Latex:
\mforall{}[p,q:iPolynomial()]. (mul\_ipoly(p;q) \mmember{} iPolynomial())
Date html generated:
2017_09_29-PM-05_53_50
Last ObjectModification:
2017_05_04-PM-03_45_33
Theory : omega
Home
Index