Specification iter-set

[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, 
   set-union
with
   functions 
       . ⊗_ . : (A → Heap[A] → Bool) × Set[A] → Heap[A] → Bool prio 12 right;
       . ∧_ . : (A → Heap[A] → Bool) × Set[A] → Heap[A] → Bool prio 11 right;
   
   variables 
       aP : A → Heap[A] → Bool;
       a : A;
       s : Set[A];
       h : Heap[A];
       hP : Heap[A] → Bool;
   
   
   axioms 
      Sep-emp: aP ⊗_ ∅ = emp;
      used for: s, ls;
      
      Sep-ins: ¬ a ∈ s → aP ⊗_ (s ++ a) = aP(a) * aP ⊗_ s;
      used for: s, ls;
      
      And-emp: aP ∧_ ∅ = true;
      used for: s, ls;
      
      And-ins: ¬ a ∈ s → aP ∧_ (s ++ a) = (aP(a) ∧ aP ∧_ s);
      used for: s, ls;
   
   
end enrich