Specification store-union

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

enrich
   store

with
   

   
   
   functions  . ∪ . : store × store → store;
             comment: gives precedence to the values in the left operand;
   predicates  . ⊥ . : store × store;
   
   
   
   

   

   axioms disjoint :  ⊦ st0 ⊥ st1 ↔ (∀ a. ¬ a ∈ st0 ∨ ¬ a ∈ st1);
          union-in :  ⊦ a ∈ st0 ∪ st1 ↔ a ∈ st0 ∨ a ∈ st1;
          used for: s, ls;
          union-at-left :  ⊦ (st0 ∪ st1)[a] = (a ∈ st0 ⊃ st0[a];st1[a]);
          used for: ls;

   

   
end enrich