### Nuprl Lemma : rotate-by-transitive

`∀n,b:ℕ.  (gcd(b;n) = 1 ∈ ℤ supposing 0 < n `⇐⇒` ∀x,y:ℕn.  ∃k:ℕ. ((rotate-by(n;b)^k x) = y ∈ ℤ))`

Proof

Definitions occuring in Statement :  rotate-by: `rotate-by(n;i)` fun_exp: `f^n` gcd: `gcd(a;b)` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` apply: `f a` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat: `ℕ` uimplies: `b supposing a` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` exists: `∃x:A. B[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` squash: `↓T` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` prop: `ℙ` sq_type: `SQType(T)` guard: `{T}` modulus: `a mod n` has-value: `(a)↓` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` less_than': `less_than'(a;b)` true: `True` bfalse: `ff` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` nat_plus: `ℕ+` gt: `i > j` divides: `b | a` rotate-by: `rotate-by(n;i)` remainder: `n rem m` gcd: `gcd(a;b)` eq_int: `(i =z j)` gcd_p: `GCD(a;b;y)` cand: `A c∧ B`
Lemmas referenced :  int_seg_wf istype-less_than istype-int set_subtype_base le_wf int_subtype_base lelt_wf istype-nat int_seg_properties nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformle_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf bezout_ident_n gcd_sat_gcd_p gcd_unique subtype_base_sq assoced_elim decidable__equal_int intformeq_wf itermAdd_wf itermMultiply_wf itermMinus_wf int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_minus_lemma subtract_wf itermSubtract_wf int_term_value_subtract_lemma value-type-has-value int-value-type remainder_wfa nequal_wf lt_int_wf eqtt_to_assert assert_of_lt_int istype-top eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf equal_wf squash_wf true_wf istype-universe rem_base_case int_seg_subtype_nat istype-false subtype_rel_self iff_weakening_equal absval_wf add_functionality_wrt_eq rem_bounds_1 decidable__le istype-le div_rem_sum divide_wfa add-is-int-iff multiply-is-int-iff false_wf pos_mul_arg_bounds modulus-equal modulus-is-rem add_nat_wf multiply_nat_wf nat_wf equal-wf-base iterate-rotate-by rem-one zero-add one_divs_any divides_wf gcd_wf gcd_sat_pred mul-commutes zero-mul divisor_bound gcd-positive
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt independent_pairFormation inhabitedIsType hypothesisEquality universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesis sqequalRule isectIsType equalityIstype baseApply closedConclusion baseClosed applyEquality intEquality lambdaEquality_alt independent_isectElimination sqequalBase equalitySymmetry isect_memberFormation_alt because_Cache functionIsType productIsType productElimination imageElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination addEquality multiplyEquality equalityTransitivity instantiate cumulativity minusEquality applyLambdaEquality hyp_replacement callbyvalueReduce dependent_set_memberEquality_alt equalityElimination lessCases axiomSqEquality isectIsTypeImplies imageMemberEquality promote_hyp universeEquality pointwiseFunctionality productEquality

Latex:
\mforall{}n,b:\mBbbN{}.    (gcd(b;n)  =  1  supposing  0  <  n  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x,y:\mBbbN{}n.    \mexists{}k:\mBbbN{}.  ((rotate-by(n;b)\^{}k  x)  =  y))

Date html generated: 2019_10_15-AM-11_20_13
Last ObjectModification: 2019_06_25-PM-01_30_45

Theory : general

Home Index