[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
# .	assoclista	f	assoclist → nat
. '	assoclista	f	pair → assoclist
. + .	nat-basic2	f	nat × nat → nat
. + .	assoclista	f	pair × pair → assoclist
. + .	assoclista	f	pair × assoclist → assoclist
. + .	assoclista	f	assoclist × pair → assoclist
. + .	assoclista	f	assoclist × assoclist → assoclist
. ++ .	assoclista	f	assoclist × pair → assoclist
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	assoclista	f	assoclist × nat → assoclist
. -1l .	assoclista	f	assoclist × pair → assoclist
. -l .	assoclista	f	assoclist × pair → assoclist
. .1	pair	f	pair → elem
. .2	pair	f	pair → data
. .butlast	assoclista	f	assoclist → assoclist
. .first	assoclista	f	assoclist → pair
. .last	assoclista	f	assoclist → pair
. .rest	assoclista	f	assoclist → assoclist
. < .	assoclista	p	assoclist × assoclist
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	assoclista	f	assoclist × nat → pair
. [ . ]	assoclist	f	assoclist × elem × data → assoclist
. [ . ]	assoclista	f	assoclist × nat × pair → assoclist
. [ . ]	assoclist	f	assoclist × data → elem
. [ . ]	assoclist	f	assoclist × elem → data
. × .	pair	f	elem × data → pair
. ∈ .	assoclist	p	elem × assoclist
. ∈ .	assoclista	p	pair × assoclist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	assoclista	p	assoclist × assoclist
. ⊒ .	assoclista	p	assoclist × assoclist
[]	assoclista	c	assoclist
a	elem	v	elem
a0	pair	v	elem
assoclist	assoclista	s
ax	assoclista	v	assoclist
ax0	assoclista	v	assoclist
ax1	assoclista	v	assoclist
ax2	assoclista	v	assoclist
ay	assoclista	v	assoclist
ay0	assoclista	v	assoclist
ay1	assoclista	v	assoclist
ay2	assoclista	v	assoclist
az	assoclista	v	assoclist
az0	assoclista	v	assoclist
az1	assoclista	v	assoclist
az2	assoclista	v	assoclist
b	elem	v	elem
butlastn	assoclista	f	nat × assoclist → assoclist
c	elem	v	elem
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
disj	assoclista	p	assoclist × assoclist
dups	assoclista	p	assoclist
elem	elem	s
fillfirst	assoclista	f	nat × pair × assoclist → assoclist
firstn	assoclista	f	nat × assoclist → assoclist
frome	assoclista	f	assoclist × pair → assoclist
lastn	assoclista	f	nat × assoclist → assoclist
m	nat-basic1	v	nat
mklist	assoclista	f	pair × nat → assoclist
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
p	pair	v	pair
p0	pair	v	pair
p1	pair	v	pair
p2	pair	v	pair
pair	pair	s
pos	assoclista	f	pair × assoclist → nat
restn	assoclista	f	nat × assoclist → assoclist
rev	assoclista	f	assoclist → assoclist
rmdup	assoclista	f	assoclist → assoclist
sublist	assoclista	f	nat × nat × assoclist → assoclist
unique_al	assoclist	p	assoclist