Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	Array('a) → Nat
# .	set-basic	f	Set('a) → Nat
. % .	nat-div	pf	Nat × Nat → Nat with λ n, m. m ≠ 0
. * .	nat-mult	f	Nat × Nat → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. ++ .	set-basic	f	Set('a) × 'a → Set('a)
. +1	nat-basic	f	Nat → Nat
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. / .	nat-div	pf	Nat × Nat → Nat with λ n, m. m ≠ 0
. < .	nat-basic	p	Nat × Nat
. > .	nat	p	Nat × Nat
. [ . := . ]	array	pf	Array('a) × Nat × 'a → Array('a) with λ ar, n, a. n < # ar
. [ . ]	array	pf	Array('a) × Nat → 'a with λ ar, n. n < # ar
. ∈ .	set-basic	p	'a × Set('a)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	set-basic	p	Set('a) × Set('a)
∅	set-basic	c	Set('a)
⊥	elem	c	Elem
Array	array	s
Elem	elem	s
Nat	nat-basic	s
Set	set-basic	s
Tid	tid	s
absset	abs	p	Array(Elem) × Set(Elem)
allslotsfull	hashset-preds	p	Array(Elem) × Nat × Nat × Elem × Bool
ar	abs	v	Array(Elem)
b	abs	v	Bool
between	hashset-preds	p	Nat × Nat × Nat × Bool
dummytid	tid	c	Tid
e	abs	v	Elem
get_hash	hashset-preds	f	Elem × Nat → Nat
htok	hashset-preds	p	Array(Elem)
mkar	hashset-preds	f	Nat × Elem → Array(Elem)
mkarray	array	f	Nat → Array('a)
mkarray	array	f	Nat × 'a → Array('a)
n	abs	v	Nat
rely	hashset-preds	p	Array(Elem) × Array(Elem)
set	abs	v	Set(Elem)