Signature symbols in this unit

Symbol	Specification	Kind	Type
. % .	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
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
ADR_DUMMY	constants	c	address
BRANCH_SIZE	constants	c	nat
MIN_SIZE	constants	c	nat
address	address	s
adr	address	v	address
adr0	address	v	address
adr1	address	v	address
adr2	address	v	address
adr3	address	v	address
adr4	address	v	address
adr5	address	v	address
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
is-aligned	align	p	nat × nat
m	nat-basic	v	nat
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s