Nuprl Lemma : rotate-by-rotate-by

[n,i,j:ℕ]. ∀[x:ℕn].  ((rotate-by(n;i) (rotate-by(n;j) x)) (rotate-by(n;i j) x) ∈ ℤ)


Proof




Definitions occuring in Statement :  rotate-by: rotate-by(n;i) int_seg: {i..j-} nat: uall: [x:A]. B[x] apply: a add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: guard: {T} int_seg: {i..j-} ge: i ≥  lelt: i ≤ j < k and: P ∧ Q all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top prop: true: True squash: T subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q fun_exp: f^n primrec: primrec(n;b;c) compose: g
Lemmas referenced :  int_seg_wf nat_wf int_seg_properties nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf le_wf equal_wf fun_exp_wf fun_exp_add rotate_wf iff_weakening_equal compose_wf squash_wf true_wf iterate-rotate-rotate-by
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality sqequalRule isect_memberEquality axiomEquality because_Cache intEquality dependent_set_memberEquality addEquality productElimination dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality voidElimination voidEquality independent_pairFormation computeAll applyEquality imageElimination imageMemberEquality baseClosed equalityTransitivity equalitySymmetry independent_functionElimination universeEquality

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



Date html generated: 2018_05_21-PM-08_18_47
Last ObjectModification: 2017_07_26-PM-05_52_16

Theory : general


Home Index