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('a) × 'a → list('a) prio 9 left;
       rmdup : list('a) → list('a);
      comment: removes from the beginning, i.e. the last occurrence of an
                                     element remains in the list.;
   
   predicates 
       dups : list('a);
       disj : list('a) × list('a);
   
   variables 
       a : 'a;
       b : 'a;
       c : 'a;
       x : list('a);
       y : list('a);
       z : list('a);
   
   
   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