Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	Array('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
. +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
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
⊥	elem	c	Elem
Array	array	s
Elem	elem	s
Nat	nat-basic	s
Tid	tid	s
Tid	hashset-preds	v	Tid,flexible
allslotsfull	hashset-preds	p	Array(Elem) × Nat × Nat × Elem × Bool
ar	hashset-preds	v	Array(Elem)
b	hashset-preds	v	Bool
between	hashset-preds	p	Nat × Nat × Nat × Bool
done	hashset-preds	v	Bool
dummytid	tid	c	Tid
e	hashset-preds	v	Elem
get_hash	hashset-preds	f	Elem × Nat → Nat
htok	hashset-preds	p	Array(Elem)
m	hashset-preds	v	Nat
mkar	hashset-preds	f	Nat × Elem → Array(Elem)
mkarray	array	f	Nat → Array('a)
mkarray	array	f	Nat × 'a → Array('a)
n	hashset-preds	v	Nat
rely	hashset-preds	p	Array(Elem) × Array(Elem)
sz	hashset-preds	v	Nat
tid	hashset-preds	v	Tid