Nuprl Lemma : eqmod-by-orbits

∀n,k,p:ℕ.
  ((∃T:Type
     ∃f:T ⟶ T
      (T ~ ℕn
      ∧ Inj(T;T;f)
      ∧ {x:T| (f x) = x ∈ T}  ~ ℕk
      ∧ (∀L:T List. (||L|| = 1 ∈ ℤ) ∨ (p | ||L||) supposing orbit(T;f;L))))
  ⇒ (n ≡ k mod p))


Proof



Definitions occuring in Statement :  eqmod: a ≡ b mod m,  divides: b | a,  equipollent: A ~ B,  orbit: orbit(T;f;L),  length: ||as||,  list: T List,  inject: Inj(A;B;f),  int_seg: {i..j-},  nat: ℕ,  uimplies: b supposing a,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  apply: f a,  function: x:A ⟶ B[x],  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  all: ∀x:A. B[x],  implies: P ⇒ Q,  exists: ∃x:A. B[x],  and: P ∧ Q,  member: t ∈ T,  uall: ∀[x:A]. B[x],  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  l_all: (∀x∈L.P[x]),  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  less_than: a < b,  squash: ↓T,  nat: ℕ,  ge: i ≥ j ,  decidable: Dec(P),  or: P ∨ Q,  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  false: False,  prop: ℙ,  subtype_rel: A ⊆r B,  so_lambda: λ2x.t[x],  so_apply: x[s],  l_sum: l_sum(L),  iff: P ⇐⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  ifthenelse: if b then t else f fi ,  bfalse: ff,  rev_implies: P ⇐ Q,  eqmod: a ≡ b mod m,  subtract: n - m,  top: Top,  cand: A c∧ B,  equipollent: A ~ B,  less_than': less_than'(a;b),  compose: f o g,  true: True,  cons: [a / b],  inject: Inj(A;B;f),  surject: Surj(A;B;f),  biject: Bij(A;B;f),  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  no_repeats: no_repeats(T;l),  l_disjoint: l_disjoint(T;l1;l2),  assert: ↑b,  orbit: orbit(T;f;L),  rev_uimplies: rev_uimplies(P;Q),  listp: A List+,  l_member: (x ∈ l)
Lemmas referenced :  count-by-orbits,  subtype_base_sq,  int_subtype_base,  select_wf,  list_wf,  int_seg_properties,  nat_properties,  decidable__le,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformle_wf,  itermConstant_wf,  itermVar_wf,  istype-int,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_var_lemma,  int_formula_prop_wf,  decidable__lt,  length_wf,  intformless_wf,  int_formula_prop_less_lemma,  int_seg_wf,  istype-universe,  equipollent_wf,  inject_wf,  equal_wf,  orbit_wf,  length_wf_nat,  set_subtype_base,  le_wf,  divides_wf,  istype-nat,  list_induction,  l_all_wf,  equal-wf-base,  l_member_wf,  eqmod_wf,  l_sum_wf,  map_wf,  top_wf,  filter_wf5,  subtype_rel_list,  eq_int_wf,  map_nil_lemma,  filter_nil_lemma,  reduce_nil_lemma,  length_of_nil_lemma,  map_cons_lemma,  filter_cons_lemma,  reduce_cons_lemma,  l_all_wf_nil,  istype-void,  eqmod_weakening,  l_all_cons,  cons_wf,  equal-wf-T-base,  bool_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,  length_of_cons_lemma,  add-commutes,  eqmod_refl,  eqmod_functionality_wrt_eqmod,  add_functionality_wrt_eqmod,  minus-zero,  add-zero,  zero-add,  equipollent-nsub,  equipollent_functionality_wrt_equipollent2,  equipollent_inversion,  filter_wf4,  subtype_rel_list_set,  biject_wf,  hd_wf,  intformeq_wf,  int_formula_prop_eq_lemma,  l_all_iff,  orbit-closed,  istype-false,  less_than_wf,  fun_exp1_lemma,  select0,  list-cases,  product_subtype_list,  reduce_hd_cons_lemma,  nil_wf,  non_neg_length,  itermAdd_wf,  int_term_value_add_lemma,  member_singleton,  decidable__equal_int_seg,  no_repeats_filter,  pairwise-implies,  l_disjoint_wf,  int_seg_subtype_nat,  lelt_wf,  squash_wf,  true_wf,  l_disjoint-symmetry,  hd_member,  null_nil_lemma,  null_cons_lemma,  singleton-orbit,  l_exists_iff,  or_wf,  length-one-iff,  nil_member,  not-lt-2,  condition-implies-le,  minus-add,  minus-one-mul,  minus-one-mul-top,  add_functionality_wrt_le,  add-associates,  le-add-cancel,  orbit-transitive,  exists_wf,  nat_wf,  fun_exp_wf,  fun_exp-fixedpoint,  subtype_rel_self,  iff_weakening_equal,  member_filter,  subtype_rel_sets_simple,  listp_properties,  istype-less_than,  istype-le
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  sqequalHypSubstitution,  productElimination,  thin,  cut,  introduction,  extract_by_obid,  dependent_functionElimination,  hypothesisEquality,  isectElimination,  independent_functionElimination,  hypothesis,  independent_isectElimination,  instantiate,  cumulativity,  intEquality,  equalityTransitivity,  equalitySymmetry,  setElimination,  rename,  because_Cache,  imageElimination,  natural_numberEquality,  unionElimination,  approximateComputation,  dependent_pairFormation_alt,  lambdaEquality_alt,  int_eqEquality,  Error :memTop,  sqequalRule,  independent_pairFormation,  universeIsType,  voidElimination,  productIsType,  universeEquality,  functionIsType,  setEquality,  applyEquality,  isectIsType,  unionIsType,  equalityIstype,  baseClosed,  sqequalBase,  inhabitedIsType,  functionEquality,  unionEquality,  setIsType,  equalityElimination,  addEquality,  closedConclusion,  isect_memberEquality_alt,  productEquality,  equalityIsType1,  dependent_set_memberEquality_alt,  functionExtensionality,  promote_hyp,  hypothesis_subsumption,  applyLambdaEquality,  equalityIsType4,  hyp_replacement,  imageMemberEquality,  isect_memberFormation_alt,  axiomEquality,  minusEquality
Latex:
\mforall{}n,k,p:\mBbbN{}.
    ((\mexists{}T:Type
          \mexists{}f:T  {}\mrightarrow{}  T
            (T  \msim{}  \mBbbN{}n
            \mwedge{}  Inj(T;T;f)
            \mwedge{}  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k
            \mwedge{}  (\mforall{}L:T  List.  (||L||  =  1)  \mvee{}  (p  |  ||L||)  supposing  orbit(T;f;L))))
    {}\mRightarrow{}  (n  \mequiv{}  k  mod  p))


Date html generated: 2020_05_19-PM-10_03_29
Last ObjectModification: 2020_01_01-AM-10_06_47

Theory : num_thy_1


Home Index