specification
   using actualize
            list-del
         with
            pair
            
         by morphism
            :elem → pair; 
            :list → assoclist; 
            [] → []; 
            + → +; 
            # → #; 
            ' → '; 
            + → +; 
            + → +; 
            +2 → +2; 
            ++ → ++; 
            rmdup → rmdup; 
            rev → rev; 
            mklist → mklist; 
            fillfirst → fillfirst; 
            -l → -l; 
            -1l → -1l; 
            -p → -p; 
            pos → pos; 
            frome → frome; 
            < → <; 
            ∈ → ∈; 
            dups → dups; 
            disj → disj; 
            ⊑ → ⊑; 
            ⊒ → ⊒; 
            .head → .head; 
            .tail → .tail; 
            .last → .last; 
            .butlast → .butlast; 
            butlastn → butlastn; 
            [ ] → [ ]; 
            [ ] → [ ]; 
            firstn → firstn; 
            restn → restn; 
            lastn → lastn; 
            sublist → sublist; 
         end actualize
   functions 
       . [ . ] : assoclist × elem × data → assoclist;
   
   predicates 
       . ∈ . : elem × assoclist;
       unique_al : assoclist;
   
   variables 
       ax : assoclist;
       ay : assoclist;
       az : assoclist;
       a : elem;
       b : elem;
       d : data;
   
   partial functions 
       . [ . ] : assoclist × elem → data with λ ax, a. a ∈ ax;
       . [ . ] : assoclist × data → elem 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 specification