Nuprl Lemma : add-ipoly-prepend_wf
∀[p,q,l:iMonomial() List]. (add-ipoly-prepend(p;q;l) ∈ iMonomial() List)
Proof
Definitions occuring in Statement :
add-ipoly-prepend: add-ipoly-prepend(p;q;l),
iMonomial: iMonomial(),
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas referenced :
add-poly-prepend-sq,
rev-append_wf,
iMonomial_wf,
add-ipoly_wf1,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[p,q,l:iMonomial() List]. (add-ipoly-prepend(p;q;l) \mmember{} iMonomial() List)
Date html generated:
2017_09_29-PM-05_53_03
Last ObjectModification:
2017_05_04-PM-03_19_35
Theory : omega
Home
Index