Specification iter-map

[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
   ex-maplet, 
   map
with
   functions 
       . ⊗_ . : (A × B → Heap[A] → Bool) × Map[A, B] → Heap[A] → Bool prio 12 right;
       . ∧_ . : (A × B → Heap[A] → Bool) × Map[A, B] → Heap[A] → Bool prio 11 right;
   
   variables 
       adP : A × B → Heap[A] → Bool;
       a : A;
       st : Map[A, B];
       d : B;
       h : Heap[A];
       hP : Heap[A] → Bool;
   
   
   axioms 
      Sep-emp: adP ⊗_ ∅ = emp;
      used for: s, ls;
      
      Sep-ins: ¬ a ∈ st → adP ⊗_ st(a := d) = adP(a, d) * adP ⊗_ st;
      used for: s, ls;
      
      And-emp: adP ∧_ ∅ = true;
      used for: s, ls;
      
      And-ins: ¬ a ∈ st → adP ∧_ st(a := d) = (adP(a, d) ∧ adP ∧_ st);
      used for: s, ls;
   
   
end enrich