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	RG2+DF-Theory	v	state × state → bool
G1	RG2+DF-Theory	v	state × state → bool
G2	RG2+DF-Theory	v	state × state → bool
Init	RG2+DF-Theory	v	state → bool
Inv	RG2+DF-Theory	v	state → bool
N	RG2+DF-Theory	v	nat,flexible
Post	RG2+DF-Theory	v	state → bool
Post1	RG2+DF-Theory	v	state → bool
Post2	RG2+DF-Theory	v	state → bool
Pre	RG2+DF-Theory	v	state → bool
Pre1	RG2+DF-Theory	v	state → bool
Pre2	RG2+DF-Theory	v	state → bool
R	RG2+DF-Theory	v	state × state → bool
R1	RG2+DF-Theory	v	state × state → bool
R2	RG2+DF-Theory	v	state × state → bool
RG-restr	RG2+DF-Theory	p	(state → bool) × (state → bool) × (state × state → bool) × (state × state → bool) × (state → bool) × (state → bool) × (state → bool) × (state × state → bool) × (state × state → bool) × (state → bool) × (state → bool) × (state → bool)
Runs	RG2+DF-Theory	v	state → bool
Runs1	RG2+DF-Theory	v	state → bool
Runs2	RG2+DF-Theory	v	state → bool
S	state	v	state,flexible
bv	RG2+DF-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
s	state	v	state
s0	state	v	state
s1	state	v	state
s2	state	v	state
state	state	s