[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,

Specification Progress-I-2-Theory
enrich
   RG-I-2-Theory

with
   

   
   
   functions  not . : (param × state → bool) → param × state → bool;
   predicates  P-restr : param × (param × state → bool) × (param × state → bool) × (param × state × state → bool);
               stable : param × (param × state → bool) × (param × state × state → bool);
   
   variables  P : param × state → bool;
              I : param × state → bool;
   
   

   

   axioms notP-def :  ⊦ (¬ P)(pm, s) ↔ ¬ P(pm, s);
          used for: s, ls;
          stable-def :  ⊦ stable(pm, I, R) ↔ (∀ s, s0. I(pm, s) ∧ R(pm, s, s0) → I(pm, s0));
          P-restr-def :  ⊦ P-restr(pm, P, I, R) ↔ (∀ s, s0. I(pm, s) ∧ I(pm, s0) ∧ P(pm, s) ∧ R(pm, s, s0) → P(pm, s0));

   

   
end enrich