Nuprl Lemma : member-polynomial-mon-vars
∀p:iMonomial() List. ∀L:ℤ List List. ∀vs:ℤ List.
((vs ∈ polynomial-mon-vars(L;p)) ⇐⇒ (vs ∈ L) ∨ (∃m∈p. vs = (snd(m)) ∈ (ℤ List)))
Proof
Definitions occuring in Statement :
polynomial-mon-vars: polynomial-mon-vars(init;p),
iMonomial: iMonomial(),
l_exists: (∃x∈L. P[x]),
l_member: (x ∈ l),
list: T List,
pi2: snd(t),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
polynomial-mon-vars: polynomial-mon-vars(init;p),
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_lambda: λ2x y.t[x; y],
iMonomial: iMonomial(),
so_apply: x[s1;s2],
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
pi2: snd(t),
so_apply: x[s],
implies: P ⇒ Q,
top: Top,
iff: P ⇐⇒ Q,
and: P ∧ Q,
or: P ∨ Q,
rev_implies: P ⇐ Q,
false: False,
guard: {T}
Lemmas referenced :
list_induction,
iMonomial_wf,
all_wf,
list_wf,
iff_wf,
l_member_wf,
list_accum_wf,
insert_wf,
list-deq_wf,
int-deq_wf,
or_wf,
l_exists_wf,
equal-wf-base-T,
list_subtype_base,
int_subtype_base,
list_accum_nil_lemma,
false_wf,
l_exists_nil,
l_exists_wf_nil,
list_accum_cons_lemma,
l_exists_cons,
cons_wf,
member-insert,
equal_wf,
equal-wf-base,
set_subtype_base,
sorted_wf,
subtype_rel_self
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
thin,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesis,
lambdaEquality,
intEquality,
because_Cache,
hypothesisEquality,
productElimination,
setElimination,
rename,
applyEquality,
independent_isectElimination,
setEquality,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
independent_pairFormation,
inlFormation,
unionElimination,
addLevel,
allFunctionality,
impliesFunctionality,
orFunctionality,
spreadEquality,
levelHypothesis,
promote_hyp,
inrFormation
Latex:
\mforall{}p:iMonomial() List. \mforall{}L:\mBbbZ{} List List. \mforall{}vs:\mBbbZ{} List.
((vs \mmember{} polynomial-mon-vars(L;p)) \mLeftarrow{}{}\mRightarrow{} (vs \mmember{} L) \mvee{} (\mexists{}m\mmember{}p. vs = (snd(m))))
Date html generated:
2016_05_14-AM-07_10_02
Last ObjectModification:
2015_12_26-PM-01_07_30
Theory : omega
Home
Index