Specification set-nogen-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
   set-nogen-basic

with
   

   
   
   functions  { . } : elem → setnogen;
              . ∪ . : setnogen × setnogen → setnogen;
              . ∩ . : setnogen × setnogen → setnogen;
              . \ . : setnogen × setnogen → setnogen;
              . -- . : setnogen × elem → setnogen prio 9 left;
   
   
   
   
   

   

   axioms One :  ⊦ {a}  = ∅ ++ a;
          used for: ls;
          Union :  ⊦ a ∈ sng1 ∪ sng2 ↔ a ∈ sng1 ∨ a ∈ sng2;
          used for: s, ls;
          Intersect :  ⊦ a ∈ sng1 ∩ sng2 ↔ a ∈ sng1 ∧ a ∈ sng2;
          used for: s, ls;
          Difference :  ⊦ a ∈ sng1 \ sng2 ↔ a ∈ sng1 ∧ ¬ a ∈ sng2;
          used for: s, ls;
          Delete :  ⊦ a ∈ sng -- b ↔ a ≠ b ∧ a ∈ sng;
          used for: s, ls;

   

   
end enrich