enrich
   list-dup
with
   functions 
       rev : List → List;
       mklist : Elem × Nat → List;
      comment: mklist(a, n), return list with n times a.;
       fillfirst : Nat × Elem × List → List;
   
   predicates 
       . ⊑ . : List × List;
      comment: x ⊑ y = x is prefix of y;
       . ⊒ . : List × List;
      comment: x ⊒ y = x is postfix of y;
   
   variables 
       a : Elem;
       b : Elem;
       c : Elem;
       x : List;
       y : List;
       z : List;
       m : Nat;
       n : Nat;
   
   partial functions 
       . .last : List → Elem with λ x. x ≠ [];
       . .butlast : List → List with λ x. x ≠ [];
       butlastn : Nat × List → List with λ n, x. n ≤ # x;
      comment: return list except last n elements;
   
   
   axioms 
      butlast-one: a '.butlast = [];
      used for: s, ls;
      
      last-one: a '.last = a;
      used for: s, ls;
      
      butlast-rec: (a ' + b ' + x).butlast = a ' + (b ' + x).butlast;
      used for: s, ls;
      
      last-rec: (b ' + a ' + x).last = (a ' + x).last;
      used for: s, ls;
      
      rev-e: rev([]) = [];
      used for: s, ls;
      
      rev-r: rev(a ' + x) = rev(x) + a;
      used for: s, ls;
      
      mk-zero: mklist(a, 0) = [];
      used for: s, ls;
      
      mk-succ: mklist(a, n + 1) = a ' + mklist(a, n);
      
      butlastN-base: butlastn(0, x) = x;
      used for: s, ls;
      
      butlastN-rec: butlastn(n + 1, x) = butlastn(n, x.butlast);
      used for: s, ls;
      
      fillfirst-longer: n ≤ # x → fillfirst(n, a, x) = x;
      used for: s, ls;
      
      fillfirst-fill: # x < n → fillfirst(n, a, x) = mklist(a, n - # x) + x;
      
      prefix: x ⊑ y ↔ (∃ z. x + z = y);
      used for: ls;
      
      postfix: x ⊒ y ↔ (∃ z. z + x = y);
      used for: ls;
   
   
end enrich