[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
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. * .	rational	f	rationals × rationals → rationals
. * .	nat-mult	f	nat × nat → nat
. * .	int-mult	f	int × int → int
. + .	int-basic2	f	int × int → int
. + .	rational	f	rationals × rationals → rationals
. + .	nat-basic2	f	nat × nat → nat
. +1	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. - .	rational	f	rationals × rationals → rationals
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. .denom	rational	f	rationals → int
. .num	rational	f	rationals → int
. / .	int-div	f	int × int → int
. / .	rational	f	rationals × rationals → rationals
. / .	nat-div	f	nat × nat → nat
. < .	rational	p	rationals × rationals
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. > .	rational	p	rationals × rationals
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. ^ .	int-pot	f	int × int → int
. ^2	int-square	f	int → int
. \| .	int-gcd	p	int × int
. ≤ .	rational	p	rationals × rationals
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	rational	p	rationals × rationals
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
~ .	int-abs	f	int → int
~ .	rational	f	rationals → rationals
0r	rational	c	rationals
1r	rational	c	rationals
abs	int-abs	f	int → int
abs	rational	f	rationals → rationals
even	int-min	p	int
gcd	int-gcd	f	int × int → int
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
int	int-basic1	s
isSquare	int-square	p	int
j	int-basic1	v	int
j0	int-basic1	v	int
m	nat-basic1	v	nat
max	int-min	f	int × int → int
max_prime_divisor	int-gcd	f	int → int
min	int-min	f	int × int → int
n	nat-basic1	v	nat
n→i	intnat	f	nat → int
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
odd	int-min	p	int
prime	int-gcd	p	int
rational	rational	f	int × int → rationals
rationals	rational	s
ri	rational	v	rationals
ri0	rational	v	rationals
ri1	rational	v	rationals
rj	rational	v	rationals
rj0	rational	v	rationals
rj1	rational	v	rationals
sgn	int-min	f	int → int
sqrt	int-square	f	int → int