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;
       . [ . ]r : 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]r = a;
      used for: s, ls;
      
      rassoc-no: d ≠ d0 → ((a, d0) ' + ax)[d]r = ax[d]r;
      used for: s, ls;
      
      empty: ¬ a ∈ [];
      used for: s, ls;
      
      inrec: a ∈ (b, d0) ' + ax ↔ a = b ∨ a ∈ ax;
      used for: s, ls;
      
      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