### Nuprl Lemma : cycle-as-flips

`∀n:ℕ. ∀L:ℕn List.  ∃flips:(ℕn × ℕn) List. (cycle(L) = compose-flips(flips) ∈ (ℕn ⟶ ℕn)) supposing no_repeats(ℕn;L)`

Proof

Definitions occuring in Statement :  compose-flips: `compose-flips(flips)` cycle: `cycle(L)` no_repeats: `no_repeats(T;l)` list: `T List` int_seg: `{i..j-}` nat: `ℕ` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` prop: `ℙ` so_apply: `x[s]` implies: `P `` Q` exists: `∃x:A. B[x]` cycle: `cycle(L)` ifthenelse: `if b then t else f fi ` null: `null(as)` nil: `[]` it: `⋅` btrue: `tt` compose-flips: `compose-flips(flips)` reduce: `reduce(f;k;as)` list_ind: list_ind map: `map(f;as)` or: `P ∨ Q` cons: `[a / b]` top: `Top` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` bfalse: `ff` let: let bool: `𝔹` unit: `Unit` uiff: `uiff(P;Q)` and: `P ∧ Q` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` le: `A ≤ B` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction int_seg_wf isect_wf no_repeats_wf exists_wf list_wf equal_wf cycle_wf compose-flips_wf no_repeats_witness nil_wf cons_wf nat_wf equal-wf-base-T list-cases product_subtype_list null_cons_lemma reduce_hd_cons_lemma list_ind_cons_lemma null_nil_lemma list_ind_nil_lemma map_nil_lemma reduce_nil_lemma eqtt_to_assert assert_of_eq_int int_seg_properties nat_properties decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma decidable__lt intformless_wf int_formula_prop_less_lemma lelt_wf eqff_to_assert bool_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int cycle-flip-lemma length_of_cons_lemma non_neg_length length_wf itermAdd_wf int_term_value_add_lemma reduce_tl_cons_lemma no_repeats_cons map_cons_lemma reduce_cons_lemma squash_wf true_wf compose_wf flip_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination natural_numberEquality setElimination rename because_Cache hypothesis sqequalRule lambdaEquality hypothesisEquality productEquality functionEquality dependent_functionElimination independent_functionElimination isect_memberFormation dependent_pairFormation functionExtensionality baseClosed unionElimination promote_hyp hypothesis_subsumption productElimination isect_memberEquality voidElimination voidEquality equalityElimination independent_isectElimination int_eqEquality intEquality independent_pairFormation computeAll dependent_set_memberEquality equalitySymmetry equalityTransitivity instantiate addEquality independent_pairEquality applyEquality imageElimination universeEquality cumulativity imageMemberEquality

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}L:\mBbbN{}n  List.
\mexists{}flips:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.  (cycle(L)  =  compose-flips(flips))  supposing  no\_repeats(\mBbbN{}n;L)

Date html generated: 2017_04_17-AM-08_20_33
Last ObjectModification: 2017_02_27-PM-04_43_22

Theory : list_1

Home Index