[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-basic2	f	nat × nat → nat
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
G	RG-I-2-Theory	v	param × state × state → bool
G1	RG-I-2-Theory	v	param × state × state → bool
G2	RG-I-2-Theory	v	param × state × state → bool
I	RG-I-2-Theory	v	param × state → bool
N	RG-I-2-Theory	v	nat,flexible
P	Progress-I-2-Theory	v	param × state → bool
P-restr	Progress-I-2-Theory	p	param × (param × state → bool) × (param × state → bool) × (param × state × state → bool)
Post	RG-I-2-Theory	v	param × state × state → bool
Post1	RG-I-2-Theory	v	param × state × state → bool
Post2	RG-I-2-Theory	v	param × state × state → bool
Pre	RG-I-2-Theory	v	param × state → bool
Pre1	RG-I-2-Theory	v	param × state → bool
Pre2	RG-I-2-Theory	v	param × state → bool
R	RG-I-2-Theory	v	param × state × state → bool
R1	RG-I-2-Theory	v	param × state × state → bool
R2	RG-I-2-Theory	v	param × state × state → bool
RG-restr	RG-I-2-Theory	p	param × (param × state × state → bool) × (param × state × state → bool) × (param × state → bool) × (param × state × state → bool) × (param × state → bool) × (param × state × state → bool) × (param × state × state → bool) × (param × state → bool) × (param × state × state → bool)
S	RG-I-2-Theory	v	state,flexible
bv	RG-I-2-Theory	v	bool
m	nat-basic1	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
not .	Progress-I-2-Theory	f	(param × state → bool) → param × state → bool
param	state+param	s
pm	state+param	v	param
s	state+param	v	state
s0	RG-I-2-Theory	v	state
s1	RG-I-2-Theory	v	state
stable	Progress-I-2-Theory	p	param × (param × state → bool) × (param × state × state → bool)
state	state+param	s