Signature symbols in this unit

Symbol	Specification	Kind	Type
. + .	nat-basic2	f	nat × nat → nat
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. ^*	rtc	f	(elem × elem → bool) → elem × elem → bool
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
Pelem	rtc	v	elem × elem → bool
a	elem	v	elem
b	elem	v	elem
c	elem	v	elem
elem	elem	s
m	nat-basic1	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
rtc	rtc	f	nat × (elem × elem → bool) → elem × elem → bool