[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
# .	queue	f	queue → nat
. '	queue	f	elem → queue
. + .	nat-basic2	f	nat × nat → nat
. + .	queue	f	elem × elem → queue
. + .	queue	f	elem × queue → queue
. + .	queue	f	queue × queue → queue
. ++ .	queue	f	queue × elem → queue
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	queue	f	queue × nat → queue
. -1l .	queue	f	queue × elem → queue
. -l .	queue	f	queue × elem → queue
. .butlast	queue	f	queue → queue
. .last	queue	f	queue → elem
. < .	queue	p	queue × queue
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	queue	f	queue × nat → elem
. [ . ]	queue	f	queue × nat × elem → queue
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ∈ .	queue	p	elem × queue
. ⊑ .	queue	p	queue × queue
. ⊒ .	queue	p	queue × queue
[]	queue	c	queue
a	elem	v	elem
a0	list-data	v	elem
b	elem	v	elem
butlastn	queue	f	nat × queue → queue
c	elem	v	elem
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
head	queue	f	queue → elem
lastn	queue	f	nat × queue → queue
m	nat-basic2	v	nat
mklist	queue	f	elem × nat → queue
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pop	queue	f	queue → queue
pos	queue	f	elem × queue → nat
push	queue	f	queue × elem → queue
queue	queue	s
restn	queue	f	nat × queue → queue
rev	queue	f	queue → queue
rmdup	queue	f	queue → queue
sublist	queue	f	nat × nat × queue → 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