specification
   using actualize
            list-del
         with
            pair
            
         by morphism
            :Elem → Pair; 
            :List → Assoclist; 
            [] → []; 
             . + .  : (Elem × List → List) →  . + .  : (Pair × Assoclist → Assoclist); 
            # .  → # . ; 
             . ' →  . '; 
             . + .  : (List × List → List) →  . + .  : (Assoclist × Assoclist → Assoclist); 
             . + .  : (List × Elem → List) →  . + .  : (Assoclist × Pair → Assoclist); 
             . +2 .  →  . +2 . ; 
             . ++ .  →  . ++ . ; 
            rmdup → rmdup; 
            rev → rev; 
            mklist → mklist; 
            fillfirst → fillfirst; 
             . -l .  →  . -l . ; 
             . -1l .  →  . -1l . ; 
             . -p .  →  . -p . ; 
            pos → pos; 
            frome → frome; 
             . < .  : (List × List → Bool) →  . < .  : (Assoclist × Assoclist → Bool); 
             . ∈ .  →  . ∈ . ; 
            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;
       p : Pair;
   
   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;
      
      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 specification