[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
# .	assoclist	f	assoclist → nat
. '	assoclist	f	pair → assoclist
. + .	nat-basic	f	nat × nat → nat
. + .	assoclist	f	assoclist × pair → assoclist
. + .	assoclist	f	pair × assoclist → assoclist
. + .	assoclist	f	assoclist × assoclist → assoclist
. ++ .	assoclist	f	assoclist × pair → assoclist
. +1	nat-basic	f	nat → nat
. +2 .	assoclist	f	pair × pair → assoclist
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	assoclist	f	assoclist × pair → assoclist
. -l .	assoclist	f	assoclist × pair → assoclist
. -p .	assoclist	f	assoclist × nat → assoclist
. .1	pair	f	pair → elem
. .2	pair	f	pair → data
. .butlast	assoclist	pf	assoclist → assoclist with λ ax. ax ≠ []
. .head	assoclist	pf	assoclist → pair with λ ax. ax ≠ []
. .last	assoclist	pf	assoclist → pair with λ ax. ax ≠ []
. .tail	assoclist	pf	assoclist → assoclist with λ ax. ax ≠ []
. < .	nat-basic	p	nat × nat
. < .	assoclist	p	assoclist × assoclist
. > .	nat	p	nat × nat
. [ . ]	assoclist	pf	assoclist × data → elem with λ ax, d. ∃ a. a × d ∈ ax
. [ . ]	assoclist	pf	assoclist × elem → data with λ ax, a. a ∈ ax
. [ . ]	assoclist	pf	assoclist × nat × pair → assoclist with λ ax, n, p. n < # ax
. [ . ]	assoclist	pf	assoclist × nat → pair with λ ax, n. n < # ax
. [ . ]	assoclist	f	assoclist × elem × data → assoclist
. × .	pair	f	elem × data → pair
. ∈ .	assoclist	p	elem × assoclist
. ∈ .	assoclist	p	pair × assoclist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	assoclist	p	assoclist × assoclist
. ⊒ .	assoclist	p	assoclist × assoclist
[]	assoclist	c	assoclist
a	elem	v	elem
a0	pair	v	elem
assoclist	assoclist	s
ax	assoclist	v	assoclist
ax0	assoclist	v	assoclist
ax1	assoclist	v	assoclist
ay	assoclist	v	assoclist
az	assoclist	v	assoclist
b	elem	v	elem
butlastn	assoclist	pf	nat × assoclist → assoclist with λ n, ax. n ≤ # ax
c	elem	v	elem
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
disj	assoclist	p	assoclist × assoclist
dups	assoclist	p	assoclist
elem	elem	s
fillfirst	assoclist	f	nat × pair × assoclist → assoclist
firstn	assoclist	pf	nat × assoclist → assoclist with λ n, ax. n ≤ # ax
frome	assoclist	f	assoclist × pair → assoclist
lastn	assoclist	pf	nat × assoclist → assoclist with λ n, ax. n ≤ # ax
m	nat-basic	v	nat
mklist	assoclist	f	pair × nat → assoclist
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
p	pair	v	pair
p0	pair	v	pair
p1	pair	v	pair
p2	pair	v	pair
pair	pair	s
pos	assoclist	f	pair × assoclist → nat
restn	assoclist	pf	nat × assoclist → assoclist with λ n, ax. n ≤ # ax
rev	assoclist	f	assoclist → assoclist
rmdup	assoclist	f	assoclist → assoclist
sublist	assoclist	pf	nat × nat × assoclist → assoclist with λ n, m, ax. n + m ≤ # ax
unique_al	assoclist	p	assoclist