[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-basic2	function, nat × nat → nat
+1	nat-basic1	function, nat → nat
-	nat	function, nat × nat → nat
-1	nat-basic1	function, nat → nat
<	nat-basic1	predicate, nat × nat
>	nat	predicate, nat × nat
Act	CSPAWN+Preds	variable, nat → bool,flexible
Act4	RG-I-n-Instance	variable, nat → bool,flexible
Boolvar	RG-I-n-Instance	variable, bool,flexible
CGuar	CSPAWN+Preds	predicate, nat × nat → bool × cstate × nat → bool × cstate
CGuarto	CSPAWN+Preds	predicate, nat × nat → bool × cstate × nat → bool × cstate
CInit	CSPAWN+Preds	predicate, nat × nat → bool × cstate
CInitto	CSPAWN+Preds	predicate, nat × nat → bool × cstate
CInv	CSPAWN+Preds	predicate, nat × nat → bool × cstate
COP	RGI-Conds	procedure, nat × (nat → input) : cstate × (nat → output)
CRely	CSPAWN+Preds	predicate, nat × nat → bool × cstate × nat → bool × cstate
CRelyto	CSPAWN+Preds	predicate, nat × nat → bool × cstate × nat → bool × cstate
CS	RGI-Conds	variable, cstate,flexible
CS4	RG-I-n-Instance	variable, cstate,flexible
CSEQ	CSPAWN+Preds	procedure, nat : (nat → bool) × (nat → input) × cstate × (nat → output)
CSPAWN	CSPAWN+Preds	procedure, nat : (nat → bool) × (nat → input) × cstate × (nat → output)
G	RG2+DF-Theory	variable, state × state → bool
G	RG-I-2-Theory	variable, param × state × state → bool
G	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
G1	RG2+DF-Theory	variable, state × state → bool
G1	RG2+DF-Theory-Ext	predicate, state × state
G1	RG-I-2-Theory	variable, param × state × state → bool
G1	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
G2	RG2+DF-Theory	variable, state × state → bool
G2	RG2+DF-Theory-Ext	predicate, state × state
G2	RG-I-2-Theory	variable, param × state × state → bool
G2	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
GInit	RGn	predicate, state
GInv	RGn	predicate, state
Gr	RGn	function, nat → state × state → bool
Gton	RGn-Decomp-Partial	function, nat → state × state → bool
Guar	RGI-Conds	predicate, nat × cstate × cstate
I	RG-I-2-Theory	variable, param × state → bool
IV	RG-I-n-Instance	variable, nat × (nat → bool) × cstate → bool
Idle	RGI-Conds	predicate, nat × cstate
Init	RG2+DF-Theory	variable, state → bool
Init	RG2+DF-Theory-Ext	predicate, state
Init	RGI-Conds	predicate, cstate
Inp	RGn	variable, input,flexible
Inp	IOfun	variable, nat → input,flexible
Inpf	SPAWN	variable, nat → input,flexible
Inv	RG2+DF-Theory	variable, state → bool
Inv	RG2+DF-Theory-Ext	predicate, state
Inv	RGI-Conds	predicate, cstate
Invfun	CSPAWN+Preds	variable, (nat → bool) × cstate → bool
N	RG2+DF-Theory	variable, nat,flexible
N	RG2+DF-Theory-Ext	variable, nat,flexible
N	RG-I-2-Theory	variable, nat,flexible
Out	RGn	variable, output,flexible
Outf	SPAWN	variable, nat → output,flexible
Outp	IOfun	variable, nat → output,flexible
P	Progress-I-2-Theory	variable, param × state → bool
P-restr	Progress-I-2-Theory	predicate, param × param × state → bool × param × state → bool × param × state × state → bool
Po	RGn	function, nat → state → bool
Post	RG2+DF-Theory	variable, state → bool
Post	RG-I-2-Theory	variable, param × state × state → bool
Post	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
Post1	RG2+DF-Theory	variable, state → bool
Post1	RG2+DF-Theory-Ext	predicate, state × state
Post1	RG-I-2-Theory	variable, param × state × state → bool
Post1	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
Post2	RG2+DF-Theory	variable, state → bool
Post2	RG2+DF-Theory-Ext	predicate, state × state
Post2	RG-I-2-Theory	variable, param × state × state → bool
Post2	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
Poton	RGn-Decomp-Partial	function, nat → state → bool
Pr	RGn	function, nat → state → bool
Pre	RG2+DF-Theory	variable, state → bool
Pre	RG-I-2-Theory	variable, param × state → bool
Pre	RG-I-n-Instance	variable, nat × (nat → bool) × cstate → bool
Pre1	RG2+DF-Theory	variable, state → bool
Pre1	RG2+DF-Theory-Ext	predicate, state × state
Pre1	RG-I-2-Theory	variable, param × state → bool
Pre1	RG-I-n-Instance	variable, nat × (nat → bool) × cstate → bool
Pre2	RG2+DF-Theory	variable, state → bool
Pre2	RG2+DF-Theory-Ext	predicate, state × state
Pre2	RG-I-2-Theory	variable, param × state → bool
Pre2	RG-I-n-Instance	variable, nat × (nat → bool) × cstate → bool
Proc1	RG2+DF-Theory-Ext	procedure, : state
Proc2	RG2+DF-Theory-Ext	procedure, : state
Prton	RGn-Decomp-Partial	function, nat → state → bool
R	RG2+DF-Theory	variable, state × state → bool
R	RG-I-2-Theory	variable, param × state × state → bool
R	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
R1	RG2+DF-Theory	variable, state × state → bool
R1	RG2+DF-Theory-Ext	predicate, state × state
R1	RG-I-2-Theory	variable, param × state × state → bool
R1	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
R2	RG2+DF-Theory	variable, state × state → bool
R2	RG2+DF-Theory-Ext	predicate, state × state
R2	RG-I-2-Theory	variable, param × state × state → bool
R2	RG-I-n-Instance	variable, nat × (nat → bool) × cstate × (nat → bool) × cstate → bool
RG-restr	RG2+DF-Theory	predicate, 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
RG-restr	RG-I-2-Theory	predicate, 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
RG-restr	RG-I-n-Instance	predicate, 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	predicate, nat × cstate × cstate
Rfun	CSPAWN+Preds	variable, (nat → bool) × cstate × (nat → bool) × cstate → bool
Rton	RGn-Decomp-Partial	function, nat → state × state → bool
Runs	RG2+DF-Theory	variable, state → bool
Runs1	RG2+DF-Theory	variable, state → bool
Runs1	RG2+DF-Theory-Ext	predicate, state
Runs2	RG2+DF-Theory	variable, state → bool
Runs2	RG2+DF-Theory-Ext	predicate, state
Ry	RGn	function, nat → state × state → bool
S	state	variable, state,flexible
S	RG-I-2-Theory	variable, state,flexible
SEQ#	SEQ	procedure, nat × input : state × output
SPAWN#	SPAWN	procedure, nat : (nat → input) × state × (nat → output)
act	CSPAWN+Preds	variable, nat → bool
act0	CSPAWN+Preds	variable, nat → bool
act1	CSPAWN+Preds	variable, nat → bool
act2	CSPAWN+Preds	variable, nat → bool
act3	CSPAWN+Preds	variable, nat → bool
act4	RG-I-n-Instance	variable, nat → bool
act5	RG-I-n-Instance	variable, nat → bool
boolvar	RG-I-n-Instance	variable, bool
boolvar0	RG-I-n-Instance	variable, bool
boolvar1	RG-I-n-Instance	variable, bool
bv	RG2+DF-Theory	variable, bool
bv	IOfun	variable, bool
bv	RG-I-2-Theory	variable, bool
cs	cstate	variable, cstate
cs0	CSPAWN+Preds	variable, cstate
cs1	RGI-Conds	variable, cstate
cs2	RGI-Conds	variable, cstate
cs3	RGI-Conds	variable, cstate
cs4	RG-I-n-Instance	variable, cstate
cs5	RG-I-n-Instance	variable, cstate
cstate	cstate	sort,
i	IOfun	variable, input
inp	IO	variable, input
inp	IOfun	variable, nat → input
inpf	RGn-Decomp-Partial	variable, nat → input
input	IO	sort,
input	IOfun	sort,
m	nat-basic1	variable, nat
m0	RGI-Conds	variable, nat
n	nat-basic1	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
n2	RG-I-n-Instance	variable, nat
nat	nat-basic1	sort,
o	IOfun	variable, output
out	IO	variable, output
outf	RGn-Decomp-Partial	variable, nat → output
outp	IOfun	variable, nat → output
output	IO	sort,
output	IOfun	sort,
param	state+param	sort,
pm	state+param	variable, param
s	state	variable, state
s	state+param	variable, state
s0	state	variable, state
s0	RG-I-2-Theory	variable, state
s1	state	variable, state
s1	RG-I-2-Theory	variable, state
s2	state	variable, state
sstob	RGn	variable, state × state → bool
stable	Progress-I-2-Theory	predicate, param × param × state → bool × param × state × state → bool
state	state	sort,
state	state+param	sort,
stob	RGn	variable, state → bool
¬	Progress-I-2-Theory	function, param × state → bool → param × state → bool
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat