### Nuprl Lemma : cycle-injection

`∀[n:ℕ]. ∀[L:ℕn 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: `T List` inject: `Inj(A;B;f)` int_seg: `{i..j-}` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` natural_number: `\$n`
Definitions unfolded in proof :  or: `P ∨ Q` decidable: `Dec(P)` nat: `ℕ` prop: `ℙ` implies: `P `` Q` all: `∀x:A. B[x]` inject: `Inj(A;B;f)` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` cand: `A 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: `P `` Q` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` iff: `P `⇐⇒` Q` squash: `↓T` top: `Top` not: `¬A` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` subtype_rel: `A ⊆r B` ge: `i ≥ j ` 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