[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
# .	bitlista	f	bitlist → nat
# .	bytelist	f	bytelist → nat
#oc	bytelist	f	byte × bytelist → nat
#oc	bitlista	f	bool × bitlist → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	bytelist	f	byte → bytelist
. '	bitlista	f	bool → bitlist
. * .	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
. + .	bitlista	f	bool × bitlist → bitlist
. + .	bytelist	f	bytelist × byte → bytelist
. + .	bitlista	f	bitlist × bitlist → bitlist
. + .	bytelist	f	bytelist × bytelist → bytelist
. + .	bitlista	f	bitlist × bool → bitlist
. + .	bytelist	f	byte × bytelist → bytelist
. + .	bitlista	f	bool × bool → bitlist
. ++ .	bytelist	f	bytelist × byte → bytelist
. ++ .	bitlista	f	bitlist × bool → bitlist
. +1	int-basic1	f	int → int
. +1	bitopsaux	f	bitlist → bitlist
. +1	nat-basic1	f	nat → nat
. - .	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 .	bitlista	f	bitlist × bool → bitlist
. -1l .	bitlista	f	bitlist × nat → bitlist
. -l .	bitlista	f	bitlist × bool → bitlist
. -l .	bytelist	f	bytelist × byte → bytelist
. .butlast	bitlista	f	bitlist → bitlist
. .butlast	bytelist	f	bytelist → bytelist
. .first	bitlista	p	bitlist
. .first	bytelist	f	bytelist → byte
. .last	bitlista	p	bitlist
. .last	bytelist	f	bytelist → byte
. .rest	bitlista	f	bitlist → bitlist
. .rest	bytelist	f	bytelist → bytelist
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	bytelist	p	bytelist × bytelist
. < .	bitlista	p	bitlist × bitlist
. < .	nat-basic1	p	nat × nat
. < .	int-basic1	p	int × int
. << .	intops	f	int × int → int
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. >> .	intops	f	int × int → int
. [ . ]	bitlista	p	bitlist × nat
. [ . ]	bitlista	f	bitlist × nat × bool → bitlist
. [ . ]	bytelist	f	bytelist × nat → byte
. [ . ]	bytelist	f	bytelist × nat × byte → bytelist
. \ .	bytelist	f	bytelist × bytelist → bytelist
. \ .	bitlista	f	bitlist × bitlist → bitlist
. ^ .	int-pot	f	int × int → int
. ^2	int-square	f	int → int
. ∈ .	bytelist	p	byte × bytelist
. ∈ .	bitlista	p	bool × bitlist
. ∈bint	byte	p	int
. ∈byte	byte	p	int
. ∈long	byte	p	int
. ∈short	byte	p	int
. ∪ .	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
. ⊆ .	bitlista	p	bitlist × bitlist
. ⊆m .	bytelist	p	bytelist × bytelist
. ⊆m .	bitlista	p	bitlist × bitlist
. ⊑ .	bitlista	p	bitlist × bitlist
. ⊑ .	bytelist	p	bytelist × bytelist
. ⊒ .	bytelist	p	bytelist × bytelist
. ⊒ .	bitlista	p	bitlist × bitlist
. 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
[]	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
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	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
bytelist	bytelist	s
bytes	bytelist	v	bytelist
bytes0	bytelist	v	bytelist
bytes1	bytelist	v	bytelist
bytes10	bytelist	v	bytelist
bytes2	bytelist	v	bytelist
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
disj	bytelist	p	bytelist × bytelist
disj	bitlista	p	bitlist × bitlist
dups	bytelist	p	bytelist
dups	bitlista	p	bitlist
even	int-min	p	int
fillfirst	bitlista	f	nat × bool × bitlist → bitlist
fillfirst	bytelist	f	nat × byte × bytelist → bytelist
fillsgn	bitopsaux	f	nat × bitlist → bitlist
filter	bytelist	f	bytelist × bytelist → bytelist
filter	bitlista	f	bitlist × bitlist → bitlist
firstn	bitlista	f	nat × bitlist → bitlist
firstn	bytelist	f	nat × bytelist → bytelist
fix	bitopsaux	f	nat × bitlist → bitlist
frome	bytelist	f	bytelist × byte → bytelist
frome	bitlista	f	bitlist × bool → bitlist
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
i2b	byte	f	int → byte
i2bi	byte	f	int → bint
i2l	byte	f	int → long
i2s	byte	f	int → short
int	int-basic1	s
int2bits	int2bits	f	int → bitlist
isSquare	int-square	p	int
j	int-basic1	v	int
j0	int-basic1	v	int
l2i	byte	f	long → int
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
min	int-min	f	int × int → int
mklist	bytelist	f	byte × nat → bytelist
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
perm	bytelist	p	bytelist × bytelist
perm	bitlista	p	bitlist × bitlist
pos	bitlista	f	bool × bitlist → nat
pos	bytelist	f	byte × bytelist → nat
restn	bytelist	f	nat × bytelist → bytelist
restn	bitlista	f	nat × bitlist → bitlist
rev	bitlista	f	bitlist → bitlist
rev	bytelist	f	bytelist → bytelist
rmdup	bitlista	f	bitlist → bitlist
rmdup	bytelist	f	bytelist → bytelist
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
sqrt	int-square	f	int → int
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