### 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: c∧ B upto: upto(n) nat: uimplies: supposing a subtype_rel: A ⊆B int_seg: {i..j-} implies:  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