[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	pair × assoclist → assoclist
. + .	assoclist	f	assoclist × assoclist → assoclist
. + .	assoclist	f	assoclist × pair → 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 λ x. x ≠ []
. .head	assoclist	pf	assoclist → pair with λ x. x ≠ []
. .last	assoclist	pf	assoclist → pair with λ x. x ≠ []
. .tail	assoclist	pf	assoclist → assoclist with λ x. x ≠ []
. < .	nat-basic	p	nat × nat
. < .	assoclist	p	assoclist × assoclist
. > .	nat	p	nat × nat
. [ . ]	assoclist	f	assoclist × elem × data → assoclist
. [ . ]	assoclist	pf	assoclist × nat → pair with λ x, n. n < # x
. [ . ]	assoclist	pf	assoclist × nat × pair → assoclist with λ x, n, a. n < # x
. [ . ]	assoclist	pf	assoclist × elem → data with λ ax, a. a ∈ ax
. [ . ]	assoclist	pf	assoclist × data → elem with λ ax, d. ∃ a. a × d ∈ ax
. × .	pair	f	elem × data → pair
. ∈ .	assoclist	p	pair × assoclist
. ∈ .	assoclist	p	elem × assoclist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	assoclist	p	assoclist × assoclist
. ⊒ .	assoclist	p	assoclist × assoclist
[]	assoclist	c	assoclist
a	assoclist	v	elem
assoclist	assoclist	s
ax	assoclist	v	assoclist
ay	assoclist	v	assoclist
az	assoclist	v	assoclist
b	assoclist	v	elem
butlastn	assoclist	pf	nat × assoclist → assoclist with λ n, x. n ≤ # x
d	assoclist	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, x. n ≤ # x
frome	assoclist	f	assoclist × pair → assoclist
lastn	assoclist	pf	nat × assoclist → assoclist with λ n, x. n ≤ # x
mklist	assoclist	f	pair × nat → assoclist
nat	nat-basic	s
pair	pair	s
pos	assoclist	f	pair × assoclist → nat
restn	assoclist	pf	nat × assoclist → assoclist with λ n, x. n ≤ # x
rev	assoclist	f	assoclist → assoclist
rmdup	assoclist	f	assoclist → assoclist
sublist	assoclist	pf	nat × nat × assoclist → assoclist with λ n, m, x. n + m ≤ # x
unique_al	assoclist	p	assoclist