### Nuprl Lemma : iterate-rotate-rotate-by

`∀[n,i:ℕ].  (rot(n)^i = rotate-by(n;i) ∈ (ℕn ⟶ ℕn))`

Proof

Definitions occuring in Statement :  rotate-by: `rotate-by(n;i)` rotate: `rot(n)` fun_exp: `f^n` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` prop: `ℙ` fun_exp: `f^n` lt_int: `i <z j` subtract: `n - m` ifthenelse: `if b then t else f fi ` btrue: `tt` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` bfalse: `ff` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` squash: `↓T` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rotate-by: `rotate-by(n;i)` rotate: `rot(n)` compose: `f o g` decidable: `Dec(P)` less_than': `less_than'(a;b)` nat_plus: `ℕ+` true: `True` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` remainder: `n rem m`
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than primrec-unroll rotate-by-zero subtract-1-ge-0 lt_int_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf istype-nat equal-wf-T-base int_seg_wf compose_wf rotate_wf int_subtype_base set_subtype_base le_wf rem_addition subtract_wf int_seg_properties decidable__le intformnot_wf itermAdd_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_add_lemma int_term_value_subtract_lemma istype-le istype-void decidable__lt equal_wf squash_wf true_wf istype-universe rem_bounds_1 decidable__equal_int remainder_wfa nequal_wf eq_int_wf assert_of_eq_int neg_assert_of_eq_int intformeq_wf int_formula_prop_eq_lemma rem-1 add-swap add-commutes rem_add1 remainder_wf iff_weakening_equal ifthenelse_wf add_functionality_wrt_eq rem_rem_to_rem lelt_wf one-rem int_nzero_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation_alt natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination Error :memTop,  sqequalRule independent_pairFormation universeIsType voidElimination axiomEquality functionIsTypeImplies inhabitedIsType equalitySymmetry because_Cache unionElimination equalityElimination equalityTransitivity productElimination equalityIstype promote_hyp instantiate cumulativity isect_memberEquality_alt isectIsTypeImplies hyp_replacement applyLambdaEquality functionEquality imageElimination baseApply closedConclusion baseClosed applyEquality intEquality functionExtensionality_alt dependent_set_memberEquality_alt addEquality universeEquality imageMemberEquality productIsType sqequalBase minusEquality

Latex:
\mforall{}[n,i:\mBbbN{}].    (rot(n)\^{}i  =  rotate-by(n;i))

Date html generated: 2020_05_20-AM-08_15_16
Last ObjectModification: 2019_12_31-PM-08_42_31

Theory : general

Home Index