Specification list-dup

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

enrich
   list
with
   functions 
       . ++ . : list × elem → list prio 9 left;
       rmdup : list → list;
      comment: removes from the beginning, i.e. the last occurrence of an
                                     element remains in the list.;
   
   predicates 
       dups : list;
       disj : list × list;
   
   variables 
       a : elem;
       b : elem;
       c : elem;
       x : list;
       y : list;
       z : list;
   
   
   axioms 
      rmdup-e: rmdup([]) = [];
      used for: s, ls;
      
      rmdup-y: a ∈ x → rmdup(a ' + x) = rmdup(x);
      used for: s, ls;
      
      rmdup-n: ¬ a ∈ x → rmdup(a ' + x) = a + rmdup(x);
      used for: s, ls;
      
      adjoin-in: a ∈ x → x ++ a = x;
      used for: s, ls, lc;
      
      adjoin-notin: ¬ a ∈ x → x ++ a = a + x;
      used for: s, ls;
      
      dups: dups(x) ↔ (∃ a, x0, y, z. x = x0 + (a + (y + (a + z))));
      
      disjoint: disj(x, y) ↔ (∀ a. ¬(a ∈ x ∧ a ∈ y));
   
   
end enrich