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

`∀X:polynomial-constraints(). no_repeats(ℤ List;pcs-mon-vars(X))`

Proof

Definitions occuring in Statement :  pcs-mon-vars: `pcs-mon-vars(X)` polynomial-constraints: `polynomial-constraints()` no_repeats: `no_repeats(T;l)` list: `T List` all: `∀x:A. B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` polynomial-constraints: `polynomial-constraints()` pcs-mon-vars: `pcs-mon-vars(X)` member: `t ∈ T` uall: `∀[x:A]. B[x]` 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}` so_apply: `x[s]` iMonomial: `iMonomial()` prop: `ℙ` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  no_repeats-polynomial-mon-vars list_accum_cons_lemma list_accum_nil_lemma no_repeats_wf list_induction polynomial-constraints_wf no_repeats_singleton 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 lambdaFormation sqequalHypSubstitution productElimination thin sqequalRule cut hypothesis dependent_functionElimination hypothesisEquality lemma_by_obid isectElimination productEquality intEquality because_Cache applyEquality independent_isectElimination lambdaEquality natural_numberEquality setElimination rename independent_functionElimination introduction imageMemberEquality baseClosed imageElimination setEquality isect_memberEquality voidElimination voidEquality functionEquality

Latex:
\mforall{}X:polynomial-constraints().  no\_repeats(\mBbbZ{}  List;pcs-mon-vars(X))

Date html generated: 2016_05_14-AM-07_10_23
Last ObjectModification: 2016_01_14-PM-08_40_57

Theory : omega

Home Index