Nuprl Definition : orbit
orbit(T;f;L) ==
0 < ||L|| ∧ no_repeats(T;L) ∧ (∀i:ℕ||L||. ((f L[i]) = if (i =z ||L|| - 1) then L[0] else L[i + 1] fi ∈ T))
Definitions occuring in Statement :
no_repeats: no_repeats(T;l),
select: L[n],
length: ||as||,
int_seg: {i..j-},
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
less_than: a < b,
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
subtract: n - m,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
less_than: a < b,
and: P ∧ Q,
no_repeats: no_repeats(T;l),
all: ∀x:A. B[x],
int_seg: {i..j-},
equal: s = t ∈ T,
apply: f a,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
subtract: n - m,
length: ||as||,
select: L[n],
add: n + m,
natural_number: $n
FDL editor aliases :
orbit
Latex:
orbit(T;f;L) ==
0 < ||L||
\mwedge{} no\_repeats(T;L)
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((f L[i]) = if (i =\msubz{} ||L|| - 1) then L[0] else L[i + 1] fi ))
Date html generated:
2016_05_14-PM-02_22_43
Last ObjectModification:
2015_09_22-PM-05_55_53
Theory : list_1
Home
Index