Nuprl Lemma : count-cyclic-map

n:ℕ+cyclic-map(ℕn) ~ ℕ(n 1)!


Proof




Definitions occuring in Statement :  cyclic-map: cyclic-map(T) fact: (n)! equipollent: B int_seg: {i..j-} nat_plus: + all: x:A. B[x] subtract: m natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] nat_plus: + nat: decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop: subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  nat_plus_wf cyclic-map_wf int_seg_wf fact_wf subtract_wf nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf combination_wf injection_wf equipollent_same equipollent_functionality_wrt_equipollent equipollent_transitivity equipollent_inversion cyclic-map-equipollent injections-combinations equipollent-factorial equipollent_weakening_ext-eq ext-eq_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt universeIsType cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality dependent_set_memberEquality_alt because_Cache dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation applyEquality productElimination

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  cyclic-map(\mBbbN{}n)  \msim{}  \mBbbN{}(n  -  1)!



Date html generated: 2019_10_15-AM-11_22_24
Last ObjectModification: 2018_10_09-PM-00_15_12

Theory : general


Home Index