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;
       . .distinct : 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: [].distinct = [];
      used for: s, ls;
      
      rmdup-y: a ∈ x → (a ' + x).distinct = x.distinct;
      used for: s, ls;
      
      rmdup-n: ¬ a ∈ x → (a ' + x).distinct = a + x.distinct;
      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