[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 store-nogen
generic specification
   

   
parameter
   elemdata


   
target
   sorts storenogen;
         elemdata;
   
   functions  . × . : elem × data → elemdata;
              . [ . ] : storenogen × elem × data → storenogen;
              . [ . ] : storenogen × elem → data;
   predicates  . ∈ . : elemdata × storenogen;
               . ⊆ . : storenogen × storenogen;
   
   variables  stng : storenogen;
              stng0 : storenogen;
              stng1 : storenogen;
              stng2 : storenogen;
              elemdatavar : elemdata;
   
   

   induction elemdata freely generated by ×;

   axioms Extension :  ⊦ stng1 = stng2 ↔ (∀ a. stng1[a] = stng2[a]);
          used for: ls;
          At-same :  ⊦ stng[a, d][a] = d;
          used for: s, ls;
          At-other :  ⊦ a ≠ b → stng[b, d][a] = stng[a];
          used for: s, ls;
          In-store :  ⊦ a × d ∈ stng ↔ stng[a] = d;
          used for: s, ls;
          Subset :  ⊦ stng1 ⊆ stng2 ↔ (∀ a. stng1[a] = stng2[a]);
          used for: ls;

   

   
end generic specification