Nuprl Lemma : no_repeats-polynomial-mon-vars
∀p:iMonomial() List. ∀L:ℤ List List. (no_repeats(ℤ List;L) ⇒ no_repeats(ℤ List;polynomial-mon-vars(L;p)))
Proof
Definitions occuring in Statement :
polynomial-mon-vars: polynomial-mon-vars(init;p),
iMonomial: iMonomial(),
no_repeats: no_repeats(T;l),
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
int: ℤ
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],
implies: P ⇒ Q,
prop: ℙ,
so_lambda: λ2x y.t[x; y],
iMonomial: iMonomial(),
so_apply: x[s1;s2],
so_apply: x[s],
top: Top,
and: P ∧ Q,
uimplies: b supposing a
Lemmas referenced :
list_induction,
iMonomial_wf,
all_wf,
list_wf,
no_repeats_wf,
list_accum_wf,
insert_wf,
list-deq_wf,
int-deq_wf,
list_accum_nil_lemma,
list_accum_cons_lemma,
insert_property
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
thin,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesis,
lambdaEquality,
intEquality,
functionEquality,
hypothesisEquality,
spreadEquality,
setElimination,
rename,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
because_Cache,
productElimination,
independent_isectElimination
Latex:
\mforall{}p:iMonomial() List. \mforall{}L:\mBbbZ{} List List.
(no\_repeats(\mBbbZ{} List;L) {}\mRightarrow{} no\_repeats(\mBbbZ{} List;polynomial-mon-vars(L;p)))
Date html generated:
2016_05_14-AM-07_10_05
Last ObjectModification:
2015_12_26-PM-01_07_16
Theory : omega
Home
Index