[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
. % .	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
. / .	nat-div	f	nat × nat → nat
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. \| .	nat-prime	p	nat × nat
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
Boolvar	instance	v	bool,flexible
Done	implementation	v	bool,flexible
G	instance	v	nat × nat × nat × nat → bool
G1	instance	v	nat × nat × nat × nat → bool
G2	instance	v	nat × nat × nat × nat → bool
GCD	implementation	pr	: nat, nat
GCD_loop	implementation	pr	: nat, nat
Init	instance	v	nat × nat → bool
Inv	instance	v	nat × nat → bool
M	implementation	v	nat,flexible
N	RG2-Theory	v	nat,flexible
Post	instance	v	nat × nat → bool
Post1	instance	v	nat × nat → bool
Post2	instance	v	nat × nat → bool
Pre	instance	v	nat × nat → bool
Pre1	instance	v	nat × nat → bool
Pre2	instance	v	nat × nat → bool
R	instance	v	nat × nat × nat × nat → bool
R1	instance	v	nat × nat × nat × nat → bool
R2	instance	v	nat × nat × nat × nat → bool
RG-restr	instance	p	(nat × nat → bool) × (nat × nat → bool) × (nat × nat × nat × nat → bool) × (nat × nat × nat × nat → bool) × (nat × nat → bool) × (nat × nat → bool) × (nat × nat × nat × nat → bool) × (nat × nat × nat × nat → bool) × (nat × nat → bool) × (nat × nat → bool)
X	implementation	v	nat,flexible
Y	implementation	v	nat,flexible
boolvar	instance	v	bool
boolvar0	instance	v	bool
boolvar1	instance	v	bool
bv	RG2-Theory	v	bool
dist	nat-prime	f	nat × nat → nat
gcd	nat-prime	f	nat × nat → nat
inv	verification	p	nat × nat × nat × nat
m	nat-basic1	v	nat
m'	verification	v	nat
m0	instance	v	nat
m1	instance	v	nat
m2	instance	v	nat
n	nat-basic1	v	nat
n'	verification	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
n2	instance	v	nat
nat	nat-basic1	s
prime	nat-prime	p	nat
rely	verification	p	nat × nat × nat × nat