[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
# .	intlista	f	intlist → nat
# .	bytelist	f	bytelist → nat
# .	string-less	f	string → nat
# .	bitlista	f	bitlist → nat
#oc	bytelist	f	byte × bytelist → nat
#oc	bitlista	f	bool × bitlist → nat
#oc	intlista	f	int × intlist → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	bytelist	f	byte → bytelist
. '	bitlista	f	bool → bitlist
. '	intlista	f	int → intlist
. '	string-append	f	char → string
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. + .	bytelist	f	byte × byte → bytelist
. + .	intlista	f	int × intlist → intlist
. + .	bytelist	f	bytelist × byte → bytelist
. + .	intlista	f	intlist × intlist → intlist
. + .	bytelist	f	bytelist × bytelist → bytelist
. + .	intlista	f	intlist × int → intlist
. + .	bytelist	f	byte × bytelist → bytelist
. + .	string-data	f	char × string → string
. + .	bitlista	f	bool × bool → bitlist
. + .	string-append	f	string × string → string
. + .	bitlista	f	bitlist × bool → bitlist
. + .	bitlista	f	bool × bitlist → bitlist
. + .	bitlista	f	bitlist × bitlist → bitlist
. ++ .	bytelist	f	bytelist × byte → bytelist
. ++ .	intlista	f	intlist × int → intlist
. ++ .	bitlista	f	bitlist × bool → bitlist
. +1	int-basic1	f	int → int
. +1	bitopsaux	f	bitlist → bitlist
. +1	nat-basic1	f	nat → nat
. +l .	intlista	f	int × int → intlist
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. -1l .	bytelist	f	bytelist × nat → bytelist
. -1l .	bytelist	f	bytelist × byte → bytelist
. -1l .	intlista	f	intlist × int → intlist
. -1l .	bitlista	f	bitlist × nat → bitlist
. -1l .	intlista	f	intlist × nat → intlist
. -1l .	bitlista	f	bitlist × bool → bitlist
. -l .	intlista	f	intlist × int → intlist
. -l .	bytelist	f	bytelist × byte → bytelist
. -l .	bitlista	f	bitlist × bool → bitlist
. .butlast	intlista	f	intlist → intlist
. .butlast	bytelist	f	bytelist → bytelist
. .butlast	bitlista	f	bitlist → bitlist
. .char1	string-data	f	string → char
. .first	bitlista	p	bitlist
. .first	intlista	f	intlist → int
. .first	bytelist	f	bytelist → byte
. .last	bitlista	p	bitlist
. .last	bytelist	f	bytelist → byte
. .last	intlista	f	intlist → int
. .rest	intlista	f	intlist → intlist
. .rest	bytelist	f	bytelist → bytelist
. .rest	bitlista	f	bitlist → bitlist
. .rstring	string-data	f	string → string
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	bytelist	p	bytelist × bytelist
. < .	bitlista	p	bitlist × bitlist
. < .	string-less	p	char × char
. < .	int-basic1	p	int × int
. < .	string-less	p	string × string
. < .	nat-basic1	p	nat × nat
. < .	intlista	p	intlist × intlist
. << .	intops	f	int × int → int
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. >> .	intops	f	int × int → int
. [ . ]	intlista	f	intlist × nat → int
. [ . ]	bitlista	p	bitlist × nat
. [ . ]	intlista	f	intlist × nat × int → intlist
. [ . ]	bitlista	f	bitlist × nat × bool → bitlist
. [ . ]	bytelist	f	bytelist × nat × byte → bytelist
. [ . ]	bytelist	f	bytelist × nat → byte
. \ .	bytelist	f	bytelist × bytelist → bytelist
. \ .	intlista	f	intlist × intlist → intlist
. \ .	bitlista	f	bitlist × bitlist → bitlist
. ^ .	int-pot	f	int × int → int
. ^2	int-square	f	int → int
. ∈ .	bytelist	p	byte × bytelist
. ∈ .	intlista	p	int × intlist
. ∈ .	bitlista	p	bool × bitlist
. ∈bint	byte	p	int
. ∈byte	byte	p	int
. ∈long	byte	p	int
. ∈short	byte	p	int
. ∪ .	intlista	f	intlist × intlist → intlist
. ∪ .	bitlista	f	bitlist × bitlist → bitlist
. ∪ .	bytelist	f	bytelist × bytelist → bytelist
. ≤ .	nat	p	nat × nat
. ≤ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ⊆ .	bytelist	p	bytelist × bytelist
. ⊆ .	intlista	p	intlist × intlist
. ⊆ .	bitlista	p	bitlist × bitlist
. ⊆m .	bytelist	p	bytelist × bytelist
. ⊆m .	bitlista	p	bitlist × bitlist
. ⊆m .	intlista	p	intlist × intlist
. ⊑ .	intlista	p	intlist × intlist
. ⊑ .	bytelist	p	bytelist × bytelist
. ⊑ .	bitlista	p	bitlist × bitlist
. ⊒ .	bytelist	p	bytelist × bytelist
. ⊒ .	bitlista	p	bitlist × bitlist
. ⊒ .	intlista	p	intlist × intlist
. i<< .	intops	f	int × int → int
. i>> .	intops	f	int × int → int
. i>>> .	intops	f	int × int → int
. l<< .	intops	f	int × int → int
. l>> .	intops	f	int × int → int
. l>>> .	intops	f	int × int → int
>>>	intops	f	nat × int × int → int
[]	intlista	c	intlist
[]	bitlista	c	bitlist
[]	bytelist	c	bytelist
~ .	int-abs	f	int → int
0b	byte	c	byte
0bi	byte	c	bint
0l	byte	c	long
0s	byte	c	short
abs	int-abs	f	int → int
b2bi	byte	f	byte → bint
b2i	byte	f	byte → int
b2s	byte	f	byte → short
band	intops	f	int × int → int
bcompl	intops	f	int → int
bi	byte	v	bint
bi2b	byte	f	bint → byte
bi2i	byte	f	bint → int
bi2s	byte	f	bint → short
bint	byte	s
bitlist	bitlista	s
bits	bitlista	v	bitlist
bits0	bitlista	v	bitlist
bits1	bitlista	v	bitlist
bits10	bitlista	v	bitlist
bits2	bitlista	v	bitlist
bits2bytes	bytes	f	bitlist → bytelist
bits2int	int2bits	f	bitlist → int
bits2uint	int2bits	f	bitlist → int
bits3	bitlista	v	bitlist
bits4	bitlista	v	bitlist
bits5	bitlista	v	bitlist
bits6	bitlista	v	bitlist
bits7	bitlista	v	bitlist
bits8	bitlista	v	bitlist
bits9	bitlista	v	bitlist
bitsand	intops	f	bitlist × bitlist → bitlist
bitsinvert	bitopsaux	f	bitlist → bitlist
bitsor	intops	f	bitlist × bitlist → bitlist
bitsxor	intops	f	bitlist × bitlist → bitlist
bj	byte	v	bint
bool	bool	s
boolvar	bool	v	bool
boolvar0	bool	v	bool
boolvar1	bitlista	v	bool
boolvar2	bitlista	v	bool
bor	intops	f	int × int → int
butlastn	intlista	f	nat × intlist → intlist
butlastn	bitlista	f	nat × bitlist → bitlist
butlastn	bytelist	f	nat × bytelist → bytelist
bxor	intops	f	int × int → int
by	byte	v	byte
by0	bytelist	v	byte
by1	bytelist	v	byte
by2	bytelist	v	byte
byi	byte	v	byte
byj	byte	v	byte
byte	byte	s
byte2bits	bytes	f	byte → bitlist
bytelist	bytelist	s
bytes	bytelist	v	bytelist
bytes0	bytelist	v	bytelist
bytes1	bytelist	v	bytelist
bytes10	bytelist	v	bytelist
bytes2	bytelist	v	bytelist
bytes2bits	bytes	f	bytelist → bitlist
bytes2int	bytes	f	bytelist → int
bytes3	bytelist	v	bytelist
bytes4	bytelist	v	bytelist
bytes5	bytelist	v	bytelist
bytes6	bytelist	v	bytelist
bytes7	bytelist	v	bytelist
bytes8	bytelist	v	bytelist
bytes9	bytelist	v	bytelist
cast	intops	f	int × int → int
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
char3	string-less	v	char
disj	bytelist	p	bytelist × bytelist
disj	intlista	p	intlist × intlist
disj	bitlista	p	bitlist × bitlist
dups	bytelist	p	bytelist
dups	intlista	p	intlist
dups	bitlista	p	bitlist
even	int-min	p	int
fillfirst	intlista	f	nat × int × intlist → intlist
fillfirst	bitlista	f	nat × bool × bitlist → bitlist
fillfirst	bytelist	f	nat × byte × bytelist → bytelist
fillsgn	bytes	f	nat × bytelist → bytelist
fillsgn	bitopsaux	f	nat × bitlist → bitlist
filter	intlista	f	intlist × intlist → intlist
filter	bytelist	f	bytelist × bytelist → bytelist
filter	bitlista	f	bitlist × bitlist → bitlist
firstn	intlista	f	nat × intlist → intlist
firstn	bitlista	f	nat × bitlist → bitlist
firstn	bytelist	f	nat × bytelist → bytelist
fix	bytes	f	nat × bytelist → bytelist
fix	bitopsaux	f	nat × bitlist → bitlist
frome	intlista	f	intlist × int → intlist
frome	bitlista	f	bitlist × bool → bitlist
frome	bytelist	f	bytelist × byte → bytelist
hex	hexstring	f	string → int
hexbyte	hexstring	f	string → byte
hexchar	hexstring	f	char → int
hexint	hexstring	f	intlist → int
hexstring	hexstring	f	string → intlist
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
i1	intlista	v	int
i2	intlista	v	int
i2b	byte	f	int → byte
i2bi	byte	f	int → bint
i2l	byte	f	int → long
i2s	byte	f	int → short
ins≤	intlista	f	int × intlist → intlist
int	int-basic1	s
int2bits	int2bits	f	int → bitlist
int2bytes	bytes	f	int → bytelist
intlist	intlista	s
ints	intlista	v	intlist
ints0	intlista	v	intlist
ints1	intlista	v	intlist
ints10	intlista	v	intlist
ints2	intlista	v	intlist
ints3	intlista	v	intlist
ints4	intlista	v	intlist
ints5	intlista	v	intlist
ints6	intlista	v	intlist
ints7	intlista	v	intlist
ints8	intlista	v	intlist
ints9	intlista	v	intlist
isSquare	int-square	p	int
j	int-basic1	v	int
j0	int-basic1	v	int
l2i	byte	f	long → int
lastn	intlista	f	nat × intlist → intlist
lastn	bitlista	f	nat × bitlist → bitlist
lastn	bytelist	f	nat × bytelist → bytelist
lo	byte	v	long
loi	byte	v	long
loj	byte	v	long
long	byte	s
m	nat-basic1	v	nat
max	int-min	f	int × int → int
merge	intlista	f	intlist × intlist → intlist
min	int-min	f	int × int → int
mklist	bytelist	f	byte × nat → bytelist
mklist	intlista	f	int × nat → intlist
mklist	bitlista	f	bool × nat → bitlist
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
odd	int-min	p	int
ordered<	intlista	p	intlist
ordered≤	intlista	p	intlist
perm	bytelist	p	bytelist × bytelist
perm	bitlista	p	bitlist × bitlist
perm	intlista	p	intlist × intlist
pos	intlista	f	int × intlist → nat
pos	string-less	f	char × string → nat
pos	bytelist	f	byte × bytelist → nat
pos	bitlista	f	bool × bitlist → nat
restn	bytelist	f	nat × bytelist → bytelist
restn	intlista	f	nat × intlist → intlist
restn	bitlista	f	nat × bitlist → bitlist
rev	intlista	f	intlist → intlist
rev	bytelist	f	bytelist → bytelist
rev	bitlista	f	bitlist → bitlist
rmdup	intlista	f	intlist → intlist
rmdup	bytelist	f	bytelist → bytelist
rmdup	bitlista	f	bitlist → bitlist
s2b	byte	f	short → byte
s2bi	byte	f	short → bint
s2i	byte	f	short → int
sgn	int-min	f	int → int
sgn	bitopsaux	f	bitlist → bitlist
sho	byte	v	short
shoi	byte	v	short
shoj	byte	v	short
short	byte	s
shortOverflow	byte	p	int
sort	intlista	f	intlist → intlist
sortedchars	string-less	c	string
sqrt	int-square	f	int → int
str	string-data	v	string
str0	string-data	v	string
str1	string-data	v	string
str2	string-data	v	string
str3	string-data	v	string
string	string-data	s
stringvar	string-append	v	string
stringvar0	string-append	v	string
sublist	intlista	f	nat × nat × intlist → intlist
sublist	bytelist	f	nat × nat × bytelist → bytelist
sublist	bitlista	f	nat × nat × bitlist → bitlist
ub2i	byte	f	byte → int
uint2bits	int2bits	f	int → bitlist
us2i	byte	f	short → int