[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 Step
enrich ASM , 
       dominterference
 , 
       eqd with
   procedures 
      STEP#  (name × Agent → Data) × action : (name × Agent → Data);
   
   axioms 
      extensionality :  ⊦ s = s0 ↔ (∀ nam, ag. s(nam, ag) = s0(nam, ag));
      used for : generated;
       
      Term-stepjsiz :  ⊦ 〈STEP#(s, a; s1)〉 true;
      used for : generated;
       
      RMA-3 :  ⊦ ¬ 〈STEP#(s, a; s2)〉 s2(nam, ag) = s(nam, ag) → alter(dom(a), nam, ag);
      used for : generated;
       
      RMA-2
      :  ⊦ eqd(s, dom(a), s0) ∧ s(nam, ag) = s0(nam, ag) ∧ alter(dom(a), nam, ag) → 〈STEP#(s, a; s2)〉 〈STEP#(s0, a; s3)〉 s2(nam, ag) = s3(nam, ag);
      used for : generated;
       
declaration 
   STEP-decl : STEP# (s, a; s0)
                 { 
                    EXEC(a; s) ; s0 := s
                 };
end enrich