Nuprl Definition : rotate-ring
rotate-ring(T;L1;L2) ==
(||L1|| = ||L2||)
(
n:
||L1||. 
i:||L1||. if i + n <z ||L1|| then L2[i] = L1[i + n] else L2[i] = L1[i - ||L1|| - n] fi )
Definitions occuring in Statement :
select: l[i],
length: ||as||,
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
int_seg: {i..j
},
all: x:A. B[x],
exists: x:A. B[x],
and: P Q,
subtract: n - m,
add: n + m,
natural_number: $n,
int: 
,
equal: s = t
FDL editor aliases :
rotate-ring
rotate-ring(T;L1;L2) ==
(||L1|| = ||L2||)
\mwedge{} (\mexists{}n:\mBbbN{}||L1||
\mforall{}i:\mBbbN{}||L1||. if i + n <z ||L1|| then L2[i] = L1[i + n] else L2[i] = L1[i - ||L1|| - n] fi )
Date html generated:
2012_02_20-PM-05_54_01
Last ObjectModification:
2012_02_02-PM-02_29_03
Home
Index