[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
#	term	f	term → nat
#	termfuns	f	term_or_none → nat
#	rawcontext	f	rawctxt → nat
. % .	nat-div	f	nat × nat → nat
. * .	nat-mult	f	nat × nat → 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
. .t	term_or_none	f	term_or_none → term
. / .	nat-div	f	nat × nat → nat
. < .	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
even	nat-even	p	nat
hasS	termfuns	p	term
hasS	termfuns	p	term_or_none
I	OUTREDUCE	c	term
irred	reduce	p	term
K	term	c	term
ks	termfuns	f	nat → term
m	nat-basic2	v	nat
max	nat-even	f	nat × nat → nat
min	nat-even	f	nat × nat → nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
none	term_or_none	c	term_or_none
O	rawcontext	c	rawctxt
odd	nat-even	p	nat
R	reduce	v	term × term → bool
rawctxt	rawcontext	s
RED	OUTREDUCE	pr	term : term
RED1	OUTREDUCE	pr	term : term_or_none
S	term	c	term
SII	OUTREDUCE	c	term
some	term_or_none	f	term → term_or_none
t	term	v	term
t'	reduce	v	term
t0	term	v	term
t1	term	v	term
t2	term	v	term
term	term	s
term_or_none	term_or_none	s
tn	term_or_none	v	term_or_none
TOPRED	OUTREDUCE	pr	term : term_or_none
v	reduce	v	term
v1	reduce	v	term
v2	reduce	v	term
v3	reduce	v	term
value	value	p	term