### Nuprl Lemma : pcs-mon-vars_wf

`∀[X:polynomial-constraints()]. (pcs-mon-vars(X) ∈ ℤ List List)`

Proof

Definitions occuring in Statement :  pcs-mon-vars: `pcs-mon-vars(X)` polynomial-constraints: `polynomial-constraints()` list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` pcs-mon-vars: `pcs-mon-vars(X)` polynomial-constraints: `polynomial-constraints()` subtype_rel: `A ⊆r B` uimplies: `b supposing a` iPolynomial: `iPolynomial()` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` sq_stable: `SqStable(P)` implies: `P `` Q` lelt: `i ≤ j < k` and: `P ∧ Q` squash: `↓T` guard: `{T}` all: `∀x:A. B[x]` so_apply: `x[s]` iMonomial: `iMonomial()` prop: `ℙ` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  polynomial-constraints_wf polynomial-mon-vars_wf nil_wf cons_wf subtype_rel_self sorted_wf int_nzero_wf subtype_rel_product le_weakening2 less_than_transitivity2 sq_stable__le select_wf imonomial-less_wf length_wf int_seg_wf all_wf iMonomial_wf subtype_rel_set iPolynomial_wf subtype_rel_list top_wf list_wf list_accum_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination productEquality hypothesis intEquality because_Cache hypothesisEquality applyEquality independent_isectElimination lambdaEquality natural_numberEquality setElimination rename independent_functionElimination imageMemberEquality baseClosed imageElimination dependent_functionElimination setEquality isect_memberEquality voidElimination voidEquality lambdaFormation axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[X:polynomial-constraints()].  (pcs-mon-vars(X)  \mmember{}  \mBbbZ{}  List  List)

Date html generated: 2016_05_14-AM-07_10_11
Last ObjectModification: 2016_01_14-PM-08_41_01

Theory : omega

Home Index