Nuprl Lemma : add_ipoly_wf
∀[p,q:iPolynomial()]. (add_ipoly(p;q) ∈ iPolynomial())
Proof
Definitions occuring in Statement :
add_ipoly: add_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 :
add_ipoly-sq,
add-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()]. (add\_ipoly(p;q) \mmember{} iPolynomial())
Date html generated:
2017_09_29-PM-05_53_08
Last ObjectModification:
2017_05_04-PM-03_23_28
Theory : omega
Home
Index