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

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
%	nat-div	function, nat × nat → nat
*	nat-mult	function, nat × nat → nat
+	nat-basic2	function, nat × nat → nat
+1	nat-basic1	function, nat → nat
-	nat	function, nat × nat → nat
-1	nat-basic1	function, nat → nat
/	nat-div	function, nat × nat → nat
<	nat-basic1	predicate, nat × nat
>	nat	predicate, nat × nat
Boolvar	instance	variable, bool,flexible
Done	implementation	variable, bool,flexible
G	instance	variable, nat × nat × nat × nat → bool
G	RG2-Theory	variable, state × state → bool
G1	instance	variable, nat × nat × nat × nat → bool
G1	RG2-Theory	variable, state × state → bool
G2	instance	variable, nat × nat × nat × nat → bool
G2	RG2-Theory	variable, state × state → bool
GCD	implementation	procedure, : nat, nat
GCD_loop	implementation	procedure, : nat, nat
Init	instance	variable, nat × nat → bool
Init	RG2-Theory	variable, state → bool
Inv	instance	variable, nat × nat → bool
Inv	RG2-Theory	variable, state → bool
M	implementation	variable, nat,flexible
N	implementation	variable, nat,flexible
N	RG2-Theory	variable, nat,flexible
Post	instance	variable, nat × nat → bool
Post	RG2-Theory	variable, state → bool
Post1	instance	variable, nat × nat → bool
Post1	RG2-Theory	variable, state → bool
Post2	instance	variable, nat × nat → bool
Post2	RG2-Theory	variable, state → bool
Pre	instance	variable, nat × nat → bool
Pre	RG2-Theory	variable, state → bool
Pre1	instance	variable, nat × nat → bool
Pre1	RG2-Theory	variable, state → bool
Pre2	instance	variable, nat × nat → bool
Pre2	RG2-Theory	variable, state → bool
R	instance	variable, nat × nat × nat × nat → bool
R	RG2-Theory	variable, state × state → bool
R1	instance	variable, nat × nat × nat × nat → bool
R1	RG2-Theory	variable, state × state → bool
R2	instance	variable, nat × nat × nat × nat → bool
R2	RG2-Theory	variable, state × state → bool
RG-restr	instance	predicate, 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
RG-restr	RG2-Theory	predicate, state → bool × state → bool × state × state → bool × state × state → bool × state → bool × state → bool × state × state → bool × state × state → bool × state → bool × state → bool
S	state	variable, state,flexible
X	implementation	variable, nat,flexible
Y	implementation	variable, nat,flexible
boolvar	instance	variable, bool
boolvar0	instance	variable, bool
boolvar1	instance	variable, bool
bv	RG2-Theory	variable, bool
dist	nat-prime	function, nat × nat → nat
gcd	nat-prime	function, nat × nat → nat
inv	verification	predicate, nat × nat × nat × nat
m	nat-basic1	variable, nat
m'	verification	variable, nat
m0	instance	variable, nat
m1	instance	variable, nat
m2	instance	variable, nat
n	nat-basic1	variable, nat
n'	verification	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
n2	instance	variable, nat
nat	nat-basic1	sort,
prime	nat-prime	predicate, nat
rely	verification	predicate, nat × nat × nat × nat
s	state	variable, state
s0	state	variable, state
s1	state	variable, state
s2	state	variable, state
state	state	sort,
\|	nat-prime	predicate, nat × nat
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat