Signature symbols in this unit

Symbol	Specification	Kind	Type
#	rawcontext	f	rawctxt → nat
#	term	f	term → nat
. + .	nat-basic2	f	nat × nat → nat
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. .1	term	f	term → term
. .2	term	f	term → term
. .t	rawcontext	f	rawctxt → term
. < .	nat-basic1	p	nat × nat
. => .	reduce	p	term × term
. =>* .	reduce	p	term × term
. =>top .	reduce	p	term × term
. > .	nat	p	nat × nat
. [ . ]	subst	f	rawctxt × term → term
. ^ .	reduce	f	(term × term → bool) × nat → term × term → bool
. _ .	term	f	term × term → term
. _ .	rawcontext	f	rawctxt × term → rawctxt
. _ .	rawcontext	f	term × rawctxt → rawctxt
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
.c	rawcontext	f	rawctxt → rawctxt
ap	term	p	term
C	rawcontext	v	rawctxt
C0	rawcontext	v	rawctxt
Ca	rawcontext	p	rawctxt
Cf	rawcontext	p	rawctxt
context	context	p	rawctxt
irred	reduce	p	term
K	term	c	term
m	nat-basic2	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
O	rawcontext	c	rawctxt
R	reduce	v	term × term → bool
rawctxt	rawcontext	s
S	term	c	term
t	term	v	term
t'	reduce	v	term
t0	term	v	term
t1	term	v	term
t2	term	v	term
term	term	s
v	reduce	v	term
v1	reduce	v	term
v2	reduce	v	term
v3	reduce	v	term
value	value	p	term