Specification infset-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
   infset-basic
with
   functions 
       { . } : A → Iset[A];
       . ∪ . : Iset[A] × Iset[A] → Iset[A];
       . ∩ . : Iset[A] × Iset[A] → Iset[A];
       . \ . : Iset[A] × Iset[A] → Iset[A];
       . -- . : Iset[A] × A → Iset[A] prio 9 left;
   
   variables 
       a : A;
       b : A;
       c : A;
       s : Iset[A];
   
   axioms 
      One: {a}  = ∅ ++ a;
      used for: s, ls;
      
      Union: a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2;
      used for: ws, ls;
      
      Intersect: a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2;
      used for: ws, ls;
      
      Difference: a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2;
      used for: ws, ls;
      
      Delete: a ∈ s -- b ↔ a ≠ b ∧ a ∈ s;
      used for: s, ls;
   
   
end enrich