[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,
generic specification
parameter
state+param
using nat
target
predicates RG-restr
: 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)
;
variables bv : bool;
R : param × state × state → bool;
G : param × state × state → bool;
R1 : param × state × state → bool;
G1 : param × state × state → bool;
R2 : param × state × state → bool;
G2 : param × state × state → bool;
I : param × state → bool;
Pre : param × state → bool;
Pre1 : param × state → bool;
Pre2 : param × state → bool;
Post : param × state × state → bool;
Post1 : param × state × state → bool;
Post2 : param × state × state → bool;
s : state;
s0 : state;
s1 : state;
S : state flexible;
N : nat flexible;
axioms RG-restr-def
: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2)
↔ ¬
¬
( (∀ s, s0.
(Pre1(pm, s) ∧ R1(pm, s, s0) → Pre1(pm, s0)) ∧ (R1(pm, s, s0) ∧ I(pm, s) → I(pm, s0)) ∧ (R2(pm, s, s0) ∧ I(pm, s) → I(pm, s0))
∧ (Pre2(pm, s) ∧ R2(pm, s, s0) → Pre2(pm, s0)) ∧ (G1(pm, s, s0) ∧ I(pm, s) → R2(pm, s, s0))
∧ (G2(pm, s, s0) ∧ I(pm, s) → R1(pm, s, s0)))
∧ (∀ s, s0, s1.
(Pre1(pm, s) ∧ Post1(pm, s, s0) ∧ I(pm, s0) ∧ R1(pm, s0, s1) → Post1(pm, s, s1))
∧ (Pre2(pm, s) ∧ Post2(pm, s, s0) ∧ I(pm, s0) ∧ R2(pm, s0, s1) → Post2(pm, s, s1))
∧ (R1(pm, s, s0) ∧ R1(pm, s0, s1) ∧ I(pm, s) → R1(pm, s, s1)) ∧ (R2(pm, s, s0) ∧ R2(pm, s0, s1) ∧ I(pm, s) → R2(pm, s, s1)))
∧ (∀ s. (I(pm, s) → R1(pm, s, s) ∧ R2(pm, s, s)) ∧ (Pre1(pm, s) → I(pm, s)) ∧ (Pre2(pm, s) → I(pm, s))));
end generic specification