[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
# .	list-data	f	list → nat
#oc	boollist	f	bool × list → nat
. % .	nat-div	f	nat × nat → nat
. % .	int-div	f	int × int → int
. '	boollist	f	bool → list
. * .	nat-mult	f	nat × nat → nat
. * .	int-mult	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	boollist	f	bool × list → list
. + .	list	f	list × list → list
. + .	boollist	f	bool × bool → list
. + .	boollist	f	list × bool → list
. ++ .	boollist	f	list × bool → list
. +1	nat-basic1	f	nat → nat
. +1	int-basic1	f	int → int
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1	int-basic1	f	int → int
. -1l .	list-del	f	list × nat → list
. -1l .	boollist	f	list × bool → list
. -l .	boollist	f	list × bool → list
. .butlast	list-last	f	list → list
. .first	boollist	p	list
. .last	boollist	p	list
. .rest	list-data	f	list → list
. / .	nat-div	f	nat × nat → nat
. / .	int-div	f	int × int → int
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. < .	list-data	p	list × list
. < .	boollist	p	bool × bool
. > .	int-abs	p	int × int
. > .	nat	p	nat × nat
. [ . ]	boolarr	f	array × nat × bool → array
. [ . ]	boollist	f	list × nat × bool → list
. [ . ]	boollist	p	list × nat
. [ . ]	boolarr	p	array × nat
. \ .	list-set	f	list × list → list
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ∈ .	boollist	p	bool × list
. ∪ .	list-set	f	list × list → list
. ⊆ .	list-set	p	list × list
. ⊆m .	list-perm	p	list × list
. ⊑ .	list-last	p	list × list
. ⊒ .	list-last	p	list × list
[]	list-data	c	list
~ .	int-abs	f	int → int
abs	int-abs	f	int → int
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
arr2list	arr2list	f	array × nat → list
array	array	s
bool	boollist	s
butlastn	list-last	f	nat × list → list
bv	boollist	v	bool
bv0	boollist	v	bool
bv1	boollist	v	bool
bv2	boollist	v	bool
disj	list-dup	p	list × list
dups	list-dup	p	list
fillfirst	boollist	f	nat × bool × list → list
filter	list-set	f	list × list → list
firstn	list-del	f	nat × list → list
frome	boollist	f	list × bool → list
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
ins≤	boollist	f	bool × list → list
int	int-basic1	s
isperm	arr2list	p	array × array
issorted	arr2list	p	array
j	int-basic1	v	int
j0	int-basic1	v	int
lastn	list-del	f	nat × list → list
list	list-data	s
m	nat-basic2	v	nat
merge	olist	f	list × list → list
mkarray	array	f	nat → array
mklist	boollist	f	bool × nat → list
n	nat-basic1	v	nat
n→i	intnat	f	nat → int
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
ordered<	olist	p	list
ordered≤	olist	p	list
perm	list-perm	p	list × list
pos	boolarr	f	array × bool → nat
pos	boollist	f	bool × list → nat
restn	list-del	f	nat × list → list
rev	list-last	f	list → list
rmdup	list-dup	f	list → list
sort	olist-sort	f	list → list
sublist	list-del	f	nat × nat × list → list
swap#	2-way-sort	pr	int × int : array
two_way_sort#	2-way-sort	pr	: array
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
x2	list-data	v	list
y	list-data	v	list
y0	list-data	v	list
y1	list-data	v	list
y2	list-data	v	list
z	list-data	v	list
z0	list-data	v	list
z1	list-data	v	list
z2	list-data	v	list