enrich
   list-last, 
   list-getput
with
   functions 
       . -l . : list('a) × 'a → list('a);
       . -1l . : list('a) × 'a → list('a);
       . -p . : list('a) × nat → list('a);
      comment: delete element at position;
       pos : 'a × list('a) → nat;
      comment: pos is zero based;
       frome : list('a) × 'a → list('a);
      comment: return list starting with elem;
   
   variables 
       x : list('a);
       y : list('a);
       z : list('a);
       a : 'a;
       b : 'a;
       n : nat;
       m : nat;
   
   partial functions 
       firstn : nat × list('a) → list('a) with λ n, x. n ≤ # x;
      comment: return first n elements of list;
       restn : nat × list('a) → list('a) with λ n, x. n ≤ # x;
      comment: apply .tail n times;
       lastn : nat × list('a) → list('a) with λ n, x. n ≤ # x;
      comment: return last n elements of list;
       sublist : nat × nat × list('a) → list('a) with λ n, m, x. n + m ≤ # x;
      comment: sublist(offset, length, l) returns sublist from offset with length;
   
   
   axioms 
      del-e: [] -l a = [];
      used for: s, ls;
      
      del-y: (a ' + x) -l a = x -l a;
      used for: s, ls;
      
      del-n: a ≠ b → (b ' + x) -l a = b ' + (x -l a);
      used for: s, ls;
      
      del1-e: [] -1l a = [];
      used for: s, ls;
      
      del1-y: (a ' + x) -1l a = x;
      used for: s, ls;
      
      del1-n: a ≠ b → (b ' + x) -1l a = b ' + (x -1l a);
      used for: s, ls;
      
      delpos-empty: [] -p n = [];
      used for: s, ls;
      
      delpos-base: (a ' + x) -p 0 = x;
      used for: s, ls;
      
      delpos-rec: (a ' + x) -p (n + 1) = a + (x -p n);
      used for: s, ls;
      
      pos-e: pos(a, []) = 0;
      used for: s, ls;
      
      pos-y: pos(a, a ' + x) = 0;
      used for: s, ls;
      
      pos-n: a ≠ b → pos(a, b ' + x) = pos(a, x) + 1;
      used for: s, ls, lc;
      
      sublist-def: sublist(m, n, x) = firstn(n, restn(m, x));
      
      firstN-zero: firstn(0, x) = [];
      used for: s, ls;
      
      firstN-rec: firstn(n + 1, x) = x.head + firstn(n, x.tail);
      used for: ls;
      
      restN-zero: restn(0, x) = x;
      used for: s, ls;
      
      restN-rec: restn(n + 1, x) = restn(n, x.tail);
      used for: ls;
      
      lastN-zero: lastn(0, x) = [];
      used for: s, ls;
      
      lastN-rec: lastn(n + 1, x) = lastn(n, x.butlast) + x.last;
      used for: ls;
      
      fromE-empty: frome([], a) = [];
      used for: s, ls;
      
      fromE-yes: frome(a ' + x, a) = a ' + x;
      used for: s, ls;
      
      fromE-no: a ≠ b → frome(a ' + x, b) = frome(x, b);
      used for: s, ls, lc;
   
   
end enrich