Nuprl Definition : sorted-by
sorted-by(R;L) == ∀i:ℕ||L||. ∀j:ℕi. (R L[j] L[i])
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
apply: f a,
natural_number: $n
Definitions occuring in definition :
length: ||as||,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
apply: f a,
select: L[n]
FDL editor aliases :
sorted-by
Latex:
sorted-by(R;L) == \mforall{}i:\mBbbN{}||L||. \mforall{}j:\mBbbN{}i. (R L[j] L[i])
Date html generated:
2016_05_14-PM-01_46_34
Last ObjectModification:
2015_09_22-PM-05_54_47
Theory : list_1
Home
Index