[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