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

Specification set-nogen-basic
generic specification
   

   
parameter
   elem

   
target
   sorts setnogen;
   constants  ∅ : setnogen;
   functions  . ++ . : setnogen × elem → setnogen prio 9 left;
   predicates  . ∈ . : elem × setnogen;
               . ⊆ . : setnogen × setnogen;
   
   variables  sng : setnogen;
              sng0 : setnogen;
              sng1 : setnogen;
              sng2 : setnogen;
   
   

   

   axioms Extension :  ⊦ sng1 = sng2 ↔ (∀ a. a ∈ sng1 ↔ a ∈ sng2);
          used for: ls;
          In-empty :  ⊦ ¬ a ∈ ∅;
          used for: s, ls;
          In-insert :  ⊦ a ∈ sng ++ b ↔ a = b ∨ a ∈ sng;
          used for: s, ls;
          Subset :  ⊦ sng1 ⊆ sng2 ↔ (∀ a. a ∈ sng1 → a ∈ sng2);
          used for: ls;

   

   
end generic specification