### Nuprl Lemma : member-pcs-mon-vars

`∀X:polynomial-constraints(). ∀vs:ℤ List.`
`  ((vs ∈ pcs-mon-vars(X))`
`  `⇐⇒` (vs = [] ∈ (ℤ List))`
`      ∨ (∃p∈fst(X). (∃m∈p. vs = (snd(m)) ∈ (ℤ List)))`
`      ∨ (∃p∈snd(X). (∃m∈p. vs = (snd(m)) ∈ (ℤ List))))`

Proof

Definitions occuring in Statement :  pcs-mon-vars: `pcs-mon-vars(X)` polynomial-constraints: `polynomial-constraints()` l_exists: `(∃x∈L. P[x])` l_member: `(x ∈ l)` nil: `[]` list: `T List` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` polynomial-constraints: `polynomial-constraints()` pcs-mon-vars: `pcs-mon-vars(X)` pi1: `fst(t)` pi2: `snd(t)` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` iPolynomial: `iPolynomial()` int_seg: `{i..j-}` sq_stable: `SqStable(P)` implies: `P `` Q` lelt: `i ≤ j < k` and: `P ∧ Q` squash: `↓T` guard: `{T}` so_apply: `x[s]` iMonomial: `iMonomial()` prop: `ℙ` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` or: `P ∨ Q` rev_implies: `P `` Q` false: `False`
Lemmas referenced :  list_wf polynomial-constraints_wf list_induction iPolynomial_wf all_wf iff_wf l_member_wf list_accum_wf top_wf subtype_rel_list subtype_rel_set iMonomial_wf int_seg_wf length_wf imonomial-less_wf select_wf sq_stable__le less_than_transitivity2 le_weakening2 subtype_rel_product int_nzero_wf sorted_wf subtype_rel_self polynomial-mon-vars_wf or_wf l_exists_wf equal-wf-base-T list_subtype_base int_subtype_base list_accum_nil_lemma list_accum_cons_lemma false_wf l_exists_nil l_exists_wf_nil member-polynomial-mon-vars l_exists_cons cons_wf equal-wf-base nil_wf member_singleton
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin sqequalRule cut introduction extract_by_obid isectElimination intEquality hypothesis lambdaEquality because_Cache hypothesisEquality productEquality applyEquality independent_isectElimination natural_numberEquality setElimination rename independent_functionElimination imageMemberEquality baseClosed imageElimination dependent_functionElimination setEquality isect_memberEquality voidElimination voidEquality independent_pairFormation inlFormation unionElimination addLevel allFunctionality impliesFunctionality orFunctionality inrFormation equalityTransitivity equalitySymmetry

Latex:
\mforall{}X:polynomial-constraints().  \mforall{}vs:\mBbbZ{}  List.
((vs  \mmember{}  pcs-mon-vars(X))
\mLeftarrow{}{}\mRightarrow{}  (vs  =  [])  \mvee{}  (\mexists{}p\mmember{}fst(X).  (\mexists{}m\mmember{}p.  vs  =  (snd(m))))  \mvee{}  (\mexists{}p\mmember{}snd(X).  (\mexists{}m\mmember{}p.  vs  =  (snd(m)))))

Date html generated: 2017_04_14-AM-09_03_31
Last ObjectModification: 2017_02_27-PM-03_44_58

Theory : omega

Home Index