Nuprl Lemma : cycle-injection

[n:ℕ]. ∀[L:ℕList].  Inj(ℕn;ℕn;cycle(L)) supposing no_repeats(ℕn;L)


Proof




Definitions occuring in Statement :  cycle: cycle(L) no_repeats: no_repeats(T;l) list: List inject: Inj(A;B;f) int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  or: P ∨ Q decidable: Dec(P) nat: prop: implies:  Q all: x:A. B[x] inject: Inj(A;B;f) uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] cand: c∧ B exists: x:A. B[x] l_member: (x ∈ l) guard: {T} sq_type: SQType(T) so_apply: x[s] so_lambda: λ2x.t[x] int_seg: {i..j-} bfalse: ff rev_implies:  Q btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) iff: ⇐⇒ Q squash: T top: Top not: ¬A false: False satisfiable_int_formula: satisfiable_int_formula(fmla) subtype_rel: A ⊆B ge: i ≥  true: True le: A ≤ B and: P ∧ Q lelt: i ≤ j < k less_than: a < b less_than': less_than'(a;b) no_repeats: no_repeats(T;l)
Lemmas referenced :  decidable__equal_int_seg decidable__l_member nat_wf list_wf no_repeats_wf cycle_wf int_seg_wf equal_wf int_subtype_base lelt_wf set_subtype_base subtype_base_sq assert_of_bnot iff_weakening_uiff iff_transitivity eqff_to_assert assert_of_eq_int eqtt_to_assert bool_subtype_base bool_wf bool_cases iff_weakening_equal apply-cycle-member true_wf squash_wf not_wf bnot_wf assert_wf int_formula_prop_wf int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermVar_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt select_wf nat_properties int_seg_properties subtract_wf eq_int_wf length_wf equal-wf-base-T int_term_value_subtract_lemma itermSubtract_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma itermAdd_wf itermConstant_wf intformle_wf intformand_wf decidable__le le_wf false_wf decidable__equal_int less_than_wf cycle-closed istype-int full-omega-unsat istype-void istype-universe apply-cycle-non-member subtype_rel_self istype-le istype-less_than l_member_wf
Rules used in proof :  unionElimination independent_functionElimination equalitySymmetry equalityTransitivity isect_memberEquality axiomEquality dependent_functionElimination lambdaEquality sqequalRule hypothesisEquality applyEquality because_Cache rename setElimination natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid hypothesis lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productElimination intEquality independent_isectElimination cumulativity instantiate impliesFunctionality baseClosed imageMemberEquality universeEquality imageElimination computeAll voidEquality voidElimination int_eqEquality dependent_pairFormation applyLambdaEquality independent_pairFormation dependent_set_memberEquality levelHypothesis equalityUniverse addEquality productEquality Error :lambdaEquality_alt,  approximateComputation Error :dependent_pairFormation_alt,  Error :isect_memberEquality_alt,  Error :universeIsType,  Error :dependent_set_memberEquality_alt,  Error :inhabitedIsType,  Error :productIsType,  Error :lambdaFormation_alt,  hyp_replacement Error :equalityIstype

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:\mBbbN{}n  List].    Inj(\mBbbN{}n;\mBbbN{}n;cycle(L))  supposing  no\_repeats(\mBbbN{}n;L)



Date html generated: 2019_06_20-PM-01_40_24
Last ObjectModification: 2019_01_13-PM-02_03_53

Theory : list_1


Home Index