Nuprl Lemma : mul-mono-poly_wf1
∀[m:iMonomial()]. ∀[p:iMonomial() List]. (mul-mono-poly(m;p) ∈ iMonomial() List)
Proof
Definitions occuring in Statement :
mul-mono-poly: mul-mono-poly(m;p),
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,
mul-mono-poly: mul-mono-poly(m;p),
so_lambda: so_lambda(x,y,z.t[x; y; z]),
has-value: (a)↓,
uimplies: b supposing a,
so_apply: x[s1;s2;s3]
Lemmas referenced :
list_ind_wf,
iMonomial_wf,
list_wf,
nil_wf,
value-type-has-value,
iMonomial-value-type,
mul-monomials_wf,
list-value-type,
cons_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
because_Cache,
lambdaEquality,
callbyvalueReduce,
independent_isectElimination,
hypothesisEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality
Latex:
\mforall{}[m:iMonomial()]. \mforall{}[p:iMonomial() List]. (mul-mono-poly(m;p) \mmember{} iMonomial() List)
Date html generated:
2016_05_14-AM-07_03_08
Last ObjectModification:
2015_12_26-PM-01_11_17
Theory : omega
Home
Index