[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
# .	queue	f	queue → nat
. % .	nat-div	f	nat × nat → nat
. % .	int-div	f	int × int → int
. '	queue	f	elem → queue
. * .	nat-mult	f	nat × nat → nat
. * .	int-mult	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	queue	f	elem × queue → queue
. + .	queue	f	queue × queue → queue
. + .	queue	f	elem × elem → queue
. ++ .	queue	f	queue × elem → queue
. +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 .	queue	f	queue × nat → queue
. -1l .	queue	f	queue × elem → queue
. -l .	queue	f	queue × elem → queue
. .butlast	queue	f	queue → queue
. .data	ring-buffer	f	ring_buffer → array
. .data:= .	ring-buffer	f	ring_buffer × array → ring_buffer
. .first	ring-buffer	f	ring_buffer → int
. .first:= .	ring-buffer	f	ring_buffer × int → ring_buffer
. .last	queue	f	queue → elem
. .len	ring-buffer	f	ring_buffer → int
. .len:= .	ring-buffer	f	ring_buffer × int → ring_buffer
. .size	ring-buffer	f	ring_buffer → int
. .size:= .	ring-buffer	f	ring_buffer × int → ring_buffer
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. < .	queue	p	queue × queue
. > .	int-abs	p	int × int
. > .	nat	p	nat × nat
. [ . ]	queue	f	queue × nat → elem
. [ . ]	queue	f	queue × nat × elem → queue
. [ . ]	array	f	array × nat × elem → array
. [ . ]	array	f	array × nat → elem
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ∈ .	queue	p	elem × queue
. ⊑ .	queue	p	queue × queue
. ⊒ .	queue	p	queue × queue
[]	queue	c	queue
~ .	int-abs	f	int → int
a	elem	v	elem
a0	queue-impl	v	elem
abs	int-abs	f	int → int
abs	refinement	p	ring_buffer × queue
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
array	array	s
assert#	queue-impl	pr	bool :
b	elem	v	elem
buf	ring-buffer	v	ring_buffer
butlastn	queue	f	nat × queue → queue
bv	queue-impl	v	bool
c	elem	v	elem
clear#	queue-impl	pr	: ring_buffer
create#	queue-impl	pr	int : ring_buffer
disj	queue	p	queue × queue
dups	queue	p	queue
elem	elem	s
fillfirst	queue	f	nat × elem × queue → queue
firstn	queue	f	nat × queue → queue
frome	queue	f	queue × elem → queue
get#	queue-impl	pr	int × array : elem
head	queue	f	queue → elem
head#	queue-impl	pr	ring_buffer : elem
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
i1	ring-buffer	v	int
i2	ring-buffer	v	int
i3	ring-buffer	v	int
i4	ring-buffer	v	int
int	int-basic1	s
inv	ring-buffer-inv	p	ring_buffer
j	int-basic1	v	int
j0	int-basic1	v	int
lastn	queue	f	nat × queue → queue
m	nat-basic2	v	nat
mk	ring-buffer	f	array × int × int × int → ring_buffer
mkarray	array	f	nat → array
mklist	queue	f	elem × nat → queue
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
pop	queue	f	queue → queue
pop#	queue-impl	pr	: ring_buffer × elem
pos	array	f	array × elem → nat
pos	queue	f	elem × queue → nat
push	queue	f	queue × elem → queue
push#	queue-impl	pr	elem : ring_buffer
put#	queue-impl	pr	int × elem : array
queue	queue	s
restn	queue	f	nat × queue → queue
rev	queue	f	queue → queue
ring_buffer	ring-buffer	s
rmdup	queue	f	queue → queue
sublist	queue	f	nat × nat × queue → queue
test#	queue-impl	pr	elem × elem × elem :
tolist	refinement	f	ring_buffer × nat → queue
x	queue	v	queue
x0	queue	v	queue
x1	queue	v	queue
x2	queue	v	queue
y	queue	v	queue
y0	queue	v	queue
y1	queue	v	queue
y2	queue	v	queue
z	queue	v	queue
z0	queue	v	queue
z1	queue	v	queue
z2	queue	v	queue