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: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: 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 <j subtract: m ifthenelse: if then else 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:  Q iff: ⇐⇒ Q int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than: a < b squash: T subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] rotate-by: rotate-by(n;i) rotate: rot(n) compose: g decidable: Dec(P) less_than': less_than'(a;b) nat_plus: + true: True int_nzero: -o nequal: a ≠ b ∈  remainder: 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