### Nuprl Lemma : flip-conjugate-rotate

`∀[n:ℕ]. ∀[i:ℕn - 1].  ((i, i + 1) = (rot(n)^i o ((0, 1) o rot(n)^n - i)) ∈ (ℕn ⟶ ℕn))`

Proof

Definitions occuring in Statement :  flip: `(i, j)` rotate: `rot(n)` fun_exp: `f^n` compose: `f o g` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` nat: `ℕ` ge: `i ≥ j ` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` subtype_rel: `A ⊆r B` uiff: `uiff(P;Q)` guard: `{T}` subtract: `n - m` compose: `f o g` le: `A ≤ B` less_than': `less_than'(a;b)` sq_type: `SQType(T)` flip: `(i, j)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` assert: `↑b` bnot: `¬bb` nequal: `a ≠ b ∈ T `
Lemmas referenced :  nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf itermSubtract_wf itermConstant_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le istype-less_than add-member-int_seg2 int_seg_wf subtract_wf int_seg_properties decidable__le intformle_wf int_formula_prop_le_lemma iterated-rotate int_seg_subtype_nat istype-false itermAdd_wf int_term_value_add_lemma subtype_base_sq int_subtype_base eq_int_wf equal-wf-base bool_wf set_subtype_base lelt_wf assert_wf bnot_wf not_wf istype-assert uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot equal-wf-T-base lt_int_wf ifthenelse_wf int_formula_prop_eq_lemma intformeq_wf decidable__equal_int equal_wf false_wf less_than_wf assert-bnot bool_subtype_base bool_cases_sqequal assert_of_lt_int le_wf le_int_wf assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int neg_assert_of_eq_int istype-nat add-associates minus-one-mul add-swap add-commutes add-mul-special zero-mul zero-add subtract-add-cancel le_weakening2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalHypSubstitution setElimination thin rename Error :dependent_set_memberEquality_alt,  hypothesisEquality productElimination independent_pairFormation hypothesis extract_by_obid isectElimination dependent_functionElimination unionElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination sqequalRule Error :universeIsType,  Error :productIsType,  because_Cache closedConclusion applyEquality equalityTransitivity equalitySymmetry applyLambdaEquality Error :functionExtensionality_alt,  Error :lambdaFormation_alt,  Error :inhabitedIsType,  axiomEquality Error :isectIsTypeImplies,  instantiate cumulativity intEquality baseApply baseClosed Error :equalityIstype,  sqequalBase Error :functionIsType,  equalityElimination Error :equalityIsType1,  voidEquality isect_memberEquality lambdaEquality dependent_pairFormation lambdaFormation impliesFunctionality functionExtensionality hyp_replacement promote_hyp dependent_set_memberEquality addEquality Error :equalityIsType4,  multiplyEquality minusEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n  -  1].    ((i,  i  +  1)  =  (rot(n)\^{}i  o  ((0,  1)  o  rot(n)\^{}n  -  i)))

Date html generated: 2019_06_20-PM-01_35_56
Last ObjectModification: 2018_11_22-AM-10_00_45

Theory : list_1

Home Index