[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
Act	CSPAWN+Preds	v	nat → bool,flexible
Act4	RG-I-n-Instance	v	nat → bool,flexible
Boolvar	RG-I-n-Instance	v	bool,flexible
CGuar	CSPAWN+Preds	p	nat × (nat → bool) × cstate × (nat → bool) × cstate
CGuarto	CSPAWN+Preds	p	nat × (nat → bool) × cstate × (nat → bool) × cstate
CInit	CSPAWN+Preds	p	nat × (nat → bool) × cstate
CInitto	CSPAWN+Preds	p	nat × (nat → bool) × cstate
CInv	CSPAWN+Preds	p	nat × (nat → bool) × cstate
COP	RGI-Conds	pr	nat × (nat → input) : cstate × (nat → output) (nondeterministic nonfunctional)
CRely	CSPAWN+Preds	p	nat × (nat → bool) × cstate × (nat → bool) × cstate
CRelyto	CSPAWN+Preds	p	nat × (nat → bool) × cstate × (nat → bool) × cstate
CS	RGI-Conds	v	cstate,flexible
CS4	RG-I-n-Instance	v	cstate,flexible
CSEQ	CSPAWN+Preds	pr	nat : (nat → bool) × (nat → input) × cstate × (nat → output) (nondeterministic nonfunctional)
CSPAWN	CSPAWN+Preds	pr	nat : (nat → bool) × (nat → input) × cstate × (nat → output) (nondeterministic nonfunctional)
G	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
G1	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
G2	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
Guar	RGI-Conds	p	nat × cstate × cstate
IV	RG-I-n-Instance	v	nat × (nat → bool) × cstate → bool
Idle	RGI-Conds	p	nat × cstate
Init	RGI-Conds	p	cstate
Inp	IOfun	v	nat → input,flexible
Inv	RGI-Conds	p	cstate
Invfun	CSPAWN+Preds	v	(nat → bool) × cstate → bool
N	RG-I-2-Theory	v	nat,flexible
Outp	IOfun	v	nat → output,flexible
Post	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
Post1	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
Post2	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
Pre	RG-I-n-Instance	v	nat × (nat → bool) × cstate → bool
Pre1	RG-I-n-Instance	v	nat × (nat → bool) × cstate → bool
Pre2	RG-I-n-Instance	v	nat × (nat → bool) × cstate → bool
R	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
R1	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
R2	RG-I-n-Instance	v	nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
RG-restr	RG-I-n-Instance	p	nat × (nat × (nat → bool) × cstate × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate → bool) × (nat × (nat → bool) × cstate × (nat → bool) × cstate → bool)
Rely	RGI-Conds	p	nat × cstate × cstate
Rfun	CSPAWN+Preds	v	(nat → bool) × cstate × (nat → bool) × cstate → bool
act	CSPAWN+Preds	v	nat → bool
act0	CSPAWN+Preds	v	nat → bool
act1	CSPAWN+Preds	v	nat → bool
act2	CSPAWN+Preds	v	nat → bool
act3	CSPAWN+Preds	v	nat → bool
act4	RG-I-n-Instance	v	nat → bool
act5	RG-I-n-Instance	v	nat → bool
boolvar	RG-I-n-Instance	v	bool
boolvar0	RG-I-n-Instance	v	bool
boolvar1	RG-I-n-Instance	v	bool
bv	RG-I-2-Theory	v	bool
cs	cstate	v	cstate
cs0	CSPAWN+Preds	v	cstate
cs1	RGI-Conds	v	cstate
cs2	RGI-Conds	v	cstate
cs3	RGI-Conds	v	cstate
cs4	RG-I-n-Instance	v	cstate
cs5	RG-I-n-Instance	v	cstate
cstate	cstate	s
i	IOfun	v	input
inp	IOfun	v	nat → input
input	IOfun	s
m	nat-basic1	v	nat
m0	RGI-Conds	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
n2	RG-I-n-Instance	v	nat
nat	nat-basic1	s
o	IOfun	v	output
outp	IOfun	v	nat → output
output	IOfun	s