### Nuprl Lemma : orbit-cover

`∀[T:Type]`
`  ((∀x,y:T.  Dec(x = y ∈ T))`
`  `` finite-type(T)`
`  `` (∀f:T ⟶ T`
`        ∃orbits:T List List`
`         ((∀orbit∈orbits.0 < ||orbit||`
`                 ∧ no_repeats(T;orbit)`
`                 ∧ (∀i:ℕ||orbit||. (orbit[i] = (f^i orbit[0]) ∈ T))`
`                 ∧ (∀b:T. ((b ∈ orbit) `⇐⇒` ∃n:ℕ. (b = (f^n orbit[0]) ∈ T))))`
`         ∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))`
`         ∧ (∀o1∈orbits.(∀o2∈orbits.(o1[0] ∈ o2) `` o1 ⊆ o2)))))`

Proof

Definitions occuring in Statement :  finite-type: `finite-type(T)` l_contains: `A ⊆ B` l_exists: `(∃x∈L. P[x])` l_all: `(∀x∈L.P[x])` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` select: `L[n]` length: `||as||` list: `T List` fun_exp: `f^n` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` exists: `∃x:A. B[x]` finite-type: `finite-type(T)` prop: `ℙ` and: `P ∧ Q` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` less_than: `a < b` squash: `↓T` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` pi1: `fst(t)` nat: `ℕ` cand: `A c∧ B` so_lambda: `λ2x.t[x]` ge: `i ≥ j ` so_apply: `x[s]` compose: `f o g` cons: `[a / b]` uiff: `uiff(P;Q)` subtract: `n - m` true: `True` surject: `Surj(A;B;f)` l_all: `(∀x∈L.P[x])` l_contains: `A ⊆ B` l_member: `(x ∈ l)`
Lemmas referenced :  orbit-exists finite-type_wf decidable_wf equal_wf no_repeats_wf int_seg_wf length_wf select_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_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_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma fun_exp_wf int_seg_subtype_nat l_member_wf nat_wf map_wf list_wf compose_wf upto_wf l_all_wf less_than_wf all_wf nat_properties istype-false iff_wf exists_wf l_exists_wf l_all_iff member_map le_wf fun_exp0_lemma list-cases length_of_nil_lemma nil_member product_subtype_list length_of_cons_lemma length_wf_nat not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel l_exists_iff squash_wf true_wf subtype_rel_self iff_weakening_equal member_upto2 itermAdd_wf int_term_value_add_lemma fun_exp_add_sq l_contains_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis dependent_functionElimination promote_hyp productElimination Error :functionIsType,  Error :universeIsType,  Error :inhabitedIsType,  sqequalRule universeEquality applyEquality functionExtensionality Error :productIsType,  natural_numberEquality Error :equalityIsType1,  cumulativity because_Cache setElimination rename independent_isectElimination unionElimination approximateComputation Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation imageElimination equalityTransitivity equalitySymmetry productEquality Error :setIsType,  hyp_replacement applyLambdaEquality Error :dependent_set_memberEquality_alt,  hypothesis_subsumption addEquality minusEquality imageMemberEquality baseClosed instantiate functionEquality

Latex:
\mforall{}[T:Type]
((\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  finite-type(T)
{}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T
\mexists{}orbits:T  List  List
((\mforall{}orbit\mmember{}orbits.0  <  ||orbit||
\mwedge{}  no\_repeats(T;orbit)
\mwedge{}  (\mforall{}i:\mBbbN{}||orbit||.  (orbit[i]  =  (f\^{}i  orbit[0])))
\mwedge{}  (\mforall{}b:T.  ((b  \mmember{}  orbit)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (b  =  (f\^{}n  orbit[0])))))
\mwedge{}  (\mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit)))
\mwedge{}  (\mforall{}o1\mmember{}orbits.(\mforall{}o2\mmember{}orbits.(o1[0]  \mmember{}  o2)  {}\mRightarrow{}  o1  \msubseteq{}  o2)))))

Date html generated: 2019_06_20-PM-01_39_03
Last ObjectModification: 2018_10_04-PM-02_56_28

Theory : list_1

Home Index