[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 list
enrich
   list-data
with
   functions 
       . ' : Elem → List;
       . + . : List × List → List;
       . + . : List × Elem → List;
       . +2 . : Elem × Elem → List;
   
   predicates 
       . ∈ . : Elem × List;
   
   variables 
       a : Elem;
       b : Elem;
       c : Elem;
       x : List;
       y : List;
       z : List;
   
   axioms 
      Nil: [] + x = x;
      used for: s, ls;
      
      Cons: (a + x) + y = a + (x + y);
      used for: ls;
      
      One: a ' = a + [];
      used for: ls;
      
      Last: x + a = x + a ';
      used for: s, ls;
      
      Two: a +2 b = a ' + b ';
      used for: s, ls;
      
      in-empty: ¬ a ∈ [];
      used for: s, ls;
      
      in-rec: a ∈ b ' + x ↔ a = b ∨ a ∈ x;
      used for: s, ls;
   
   
end enrich