### Nuprl Lemma : no_repeats_upto

`∀[n:ℕ]. (no_repeats(ℤ;upto(n)) ∧ no_repeats(ℕn;upto(n)))`

Proof

Definitions occuring in Statement :  upto: `upto(n)` no_repeats: `no_repeats(T;l)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` and: `P ∧ Q` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` upto: `upto(n)` nat: `ℕ` uimplies: `b supposing a` subtype_rel: `A ⊆r B` int_seg: `{i..j-}` implies: `P `` Q`
Lemmas referenced :  no_repeats_from-upto no_repeats-subtype int_seg_wf upto_wf no_repeats_witness subtype_rel_list nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality hypothesis independent_pairFormation intEquality independent_isectElimination lambdaEquality because_Cache productElimination independent_pairEquality applyEquality independent_functionElimination

Latex:
\mforall{}[n:\mBbbN{}].  (no\_repeats(\mBbbZ{};upto(n))  \mwedge{}  no\_repeats(\mBbbN{}n;upto(n)))

Date html generated: 2016_05_14-PM-02_05_05
Last ObjectModification: 2015_12_26-PM-05_09_14

Theory : list_1

Home Index