Signature symbols in this unit

Symbol	Specification	Kind	Type
. + .	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-basic	p	nat × nat
. > .	nat	p	nat × nat
. ^*	rtc-ref	f	(ref × ref → bool) → ref × ref → bool
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
Boolvar	rtc-ref	v	bool,flexible
Pref	rtc-ref	v	ref × ref → bool
boolvar	rtc-ref	v	bool
boolvar0	rtc-ref	v	bool
boolvar1	rtc-ref	v	bool
m	nat-basic	v	nat
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
null	ref	c	ref
r	ref	v	ref
r0	ref	v	ref
r1	ref	v	ref
ref	ref	s
rtc	rtc-ref	f	nat × (ref × ref → bool) → ref × ref → bool