Specification assoclist

[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-del
with
   functions 
       . [ . := . ] : list(('a, 'b)) × 'a × 'b → list(('a, 'b));
   
   predicates 
       . ∈ . : 'a × list(('a, 'b));
       unique_al : list(('a, 'b));
   
   variables 
       ax : list(('a, 'b));
       a : 'a;
       b : 'a;
       d : 'b;
       p : ('a, 'b);
   
   partial functions 
       . [ . ] : list(('a, 'b)) × 'a → 'b with λ ax, a. a ∈ ax;
       . [ . ] : list(('a, 'b)) × 'b → 'a with λ ax, d. ∃ a. (a, d) ∈ ax;
   
   
   axioms 
      assoc-yes: ((a, d) ' + ax)[a] = d;
      used for: s, ls;
      
      assoc-no: a ≠ b → ((b, d) ' + ax)[a] = ax[a];
      used for: s, ls;
      
      rassoc-yes: ((a, d) ' + ax)[d] = a;
      used for: s, ls;
      
      rassoc-no: d ≠ d0 → ((a, d0) ' + ax)[d] = ax[d];
      used for: s, ls;
      
      inassoc: a ∈ ax ↔ (∃ d. (a, d) ∈ ax);
      
      put-empty: [][a := d] = (a, d) ';
      used for: s, ls;
      
      put-yes: ((a, d0) ' + ax)[a := d] = (a, d) ' + ax;
      used for: s, ls;
      
      put-no: a ≠ b → ((b, d0) ' + ax)[a := d] = (b, d0) ' + ax[a := d];
      used for: s, ls;
      
      unique-e: unique_al([]);
      used for: s, ls;
      
      unique-r: unique_al((a, d) ' + ax) ↔ ¬ a ∈ ax ∧ unique_al(ax);
      used for: ws, lws;
   
   
end enrich