[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
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
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)
Guar	RGI-Conds	p	nat × cstate × cstate
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
Outp	IOfun	v	nat → output,flexible
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
bv	IOfun	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
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
nat	nat-basic1	s
o	IOfun	v	output
outp	IOfun	v	nat → output
output	IOfun	s