### 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