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

   

   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, nokodkodax;
          Two :  ⊦ a +2 b = a ' + b ';
          used for: s, ls, nokodkodax;
          in-empty :  ⊦ ¬ a ∈ [];
          used for: s, ls;
          in-rec :  ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x;
          used for: s, ls;

   

   
end enrich