### Nuprl Lemma : orbit-decomp

`∀[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||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ T))`
`                 ∧ (∀x∈orbit.∀n:ℕ. (f^n x ∈ orbit)))`
`         ∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))`
`         ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))) `
`        supposing Inj(T;T;f)))`

Proof

Definitions occuring in Statement :  finite-type: `finite-type(T)` pairwise: `(∀x,y∈L.  P[x; y])` l_disjoint: `l_disjoint(T;l1;l2)` 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` inject: `Inj(A;B;f)` int_seg: `{i..j-}` nat: `ℕ` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` less_than: `a < b` decidable: `Dec(P)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` 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]` uimplies: `b supposing a` member: `t ∈ T` inject: `Inj(A;B;f)` exists: `∃x:A. B[x]` and: `P ∧ Q` so_lambda: `λ2x.t[x]` prop: `ℙ` int_seg: `{i..j-}` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` 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)` so_apply: `x[s]` l_disjoint: `l_disjoint(T;l1;l2)` pairwise: `(∀x,y∈L.  P[x; y])` ge: `i ≥ j ` nat: `ℕ` true: `True` subtract: `n - m` uiff: `uiff(P;Q)` cons: `[a / b]` compose: `f o g` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` assert: `↑b` l_all: `(∀x∈L.P[x])` sq_type: `SQType(T)` cand: `A c∧ B` l_member: `(x ∈ l)` no_repeats: `no_repeats(T;l)` last: `last(L)` nequal: `a ≠ b ∈ T ` bnot: `¬bb` listp: `A List+` rev_uimplies: `rev_uimplies(P;Q)` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` l_contains: `A ⊆ B` l_exists: `(∃x∈L. P[x])`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction sqequalRule sqequalHypSubstitution Error :lambdaEquality_alt,  dependent_functionElimination thin hypothesisEquality axiomEquality hypothesis Error :functionIsTypeImplies,  Error :inhabitedIsType,  rename extract_by_obid isectElimination independent_functionElimination productElimination Error :universeIsType,  setElimination productEquality closedConclusion natural_numberEquality because_Cache independent_isectElimination unionElimination approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation imageElimination applyEquality Error :setIsType,  functionEquality Error :functionIsType,  instantiate universeEquality Error :inrFormation_alt,  Error :unionIsType,  Error :inlFormation_alt,  Error :productIsType,  Error :dependent_set_memberEquality_alt,  cumulativity intWeakElimination functionExtensionality minusEquality addEquality hypothesis_subsumption promote_hyp Error :equalityIsType1,  equalitySymmetry equalityTransitivity Error :equalityIsType4,  intEquality baseClosed baseApply equalityElimination imageMemberEquality hyp_replacement applyLambdaEquality Error :equalityIstype,  sqequalBase

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||
((f  orbit[i])  =  if  (i  =\msubz{}  ||orbit||  -  1)  then  orbit[0]  else  orbit[i  +  1]  fi  ))
\mwedge{}  (\mforall{}x\mmember{}orbit.\mforall{}n:\mBbbN{}.  (f\^{}n  x  \mmember{}  orbit)))
\mwedge{}  (\mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit)))
\mwedge{}  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2)))
supposing  Inj(T;T;f)))

Date html generated: 2019_06_20-PM-01_39_37
Last ObjectModification: 2018_11_22-PM-10_09_09

Theory : list_1

Home Index