[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	array → nat
# .	suffix-array-base	f	suffixarray → nat
# .	bag-union	f	bag → nat
. + .	nat-basic2	f	nat × nat → nat
. + .	suffix-array-base	f	suffixarray × suffixarray → suffixarray
. ++ .	suffix-array-base	f	bag × nat → bag
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	suffix-array-base	f	bag × nat → bag
. -1	nat-basic1	f	nat → nat
. .elems	suffix-array-base	f	suffixarray → bag
. < .	suffix	p	array × array
. < .	oelem	p	elem × elem
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	suffix-array-base	f	suffixarray × nat → nat
. [ . ]	array	f	array × nat × elem → array
. [ . ]	suffix-array-base	f	suffixarray × nat × nat → suffixarray
. [ . ]	array	f	array × nat → elem
. \ .	bag-union	f	bag × bag → bag
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ∈ .	array-copy	p	elem × array
. ∈ .	suffix-array-base	p	nat × bag
. ∈ .	suffix-array-base	p	nat × suffixarray
. ∪ .	bag-union	f	bag × bag → bag
. ⊆ .	bag-union	p	bag × bag
. elems .	suffix-array-base	f	suffixarray × nat → bag
{ . }	suffix-array-base	f	nat → bag
⊑	suffix-array-base	v	nat × nat → bool
∅	bag-basic	c	bag
a	elem	v	elem
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
array	array	s
b	elem	v	elem
bag	bag-basic	s
bag	bag-basic	v	bag
bag< .	suffix-array	f	nat → bag
bag0	bag-basic	v	bag
bag1	bag-basic	v	bag
bag2	bag-basic	v	bag
Boolvar	gearray	v	bool,flexible
boolvar	gearray	v	bool
boolvar0	gearray	v	bool
boolvar1	gearray	v	bool
c	elem	v	elem
cmp	array-copy	p	array × elem × nat × nat
cmp	suffix-array-base	p	suffixarray × nat × suffixarray × nat × nat
cmp	array-copy	p	array × nat × array × nat × nat
cmp	suffix-array-base	p	suffixarray × nat × nat × nat
copy	suffix-array-base	f	suffixarray × nat × suffixarray × nat × nat → suffixarray
copy	array-copy	f	array × nat × array × nat × nat → array
count	suffix-array-base	f	nat × bag → nat
elem	elem	s
empty	suffix-array-base	c	nat
fill	suffix-array-base	f	suffixarray × nat × nat × nat → suffixarray
fill	suffix-array-base	f	suffixarray × nat → suffixarray
fill	array-copy	f	array × elem × nat × nat → array
fill	array-copy	f	array × elem → array
id○	array-copy	p	array × array × nat
id○	suffix-array-base	p	suffixarray × suffixarray × nat
idrange	suffix-array-base	p	suffixarray × nat × nat
idrange	array-copy	p	array × nat × nat
inv-inner	suffix-array-base	p	suffixarray × suffixarray × nat × nat × (nat × nat → bool)
inv-outer	suffix-array-base	p	suffixarray × suffixarray × nat × (nat × nat → bool)
k	suffix-array-base	v	nat
k0	suffix-array-base	v	nat
k1	suffix-array-base	v	nat
m	nat-basic2	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkarray	array	f	nat → array
mkemparray	suffix-array-base	f	nat → suffixarray
mksuffixarray	suffix-array-base	f	nat → suffixarray
mkzarray	suffix-array-base	f	nat → suffixarray
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pos	suffix-array-base	f	suffixarray × nat → nat
pos	array-copy	f	array × elem → nat
R	suffix-array-base	v	nat × nat → bool
range=	suffix-array-base	p	suffixarray × nat × suffixarray × nat × nat
reflexive	suffix-array-base	p	(nat × nat → bool)
resize	suffix-array-base	f	suffixarray × nat → suffixarray
sar	suffix-array-base	v	suffixarray
sar0	suffix-array-base	v	suffixarray
sar1	suffix-array-base	v	suffixarray
sar2	suffix-array-base	v	suffixarray
sort#	suffix-array-base	pr	nat × nat → bool : suffixarray
sorted	suffix-array-base	p	suffixarray × nat × nat × (nat × nat → bool)
sorted	suffix-array-base	p	suffixarray × (nat × nat → bool)
splice	suffix-array-base	f	suffixarray × nat × suffixarray × nat × nat → suffixarray
subarray	suffix-array-base	f	suffixarray × nat × nat → suffixarray
subarray	array-copy	f	array × nat × nat → array
suffix	suffix	f	array × nat → array
suffixarray	suffix-array-base	s
total	suffix-array-base	p	(nat × nat → bool)
transitive	suffix-array-base	p	(nat × nat → bool)
valid	suffix-array	p	suffixarray × array
zero	suffix-array-base	c	nat