[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-basic
generic specification
   

   
parameter
   elem

   using nat
target
   sorts set;
   constants  ∅ : set;
   functions  . ++ . : set × elem → set prio 9 left;
              # . : set → nat;
   predicates  . ∈ . : elem × set;
               . ⊆ . : set × set;
   
   variables  s : set;
              s0 : set;
              s1 : set;
              s2 : set;
   
   

   induction set generated by ∅, ++;

   axioms Extension :  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2);
          used for: ls;
          In-empty :  ⊦ ¬ a ∈ ∅;
          used for: s, ls;
          In-insert :  ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s;
          used for: s, ls;
          Size-empty :  ⊦ # ∅ = 0;
          used for: s, ls;
          Size-insert :  ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1;
          used for: s, ls;
          Subset :  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2);
          used for: ls;

   

   
end generic specification