enrich
   array
with
   functions 
       fill : array × elem → array;
      comment: fill complete array;
   
   predicates 
       id○ : array × array × nat;
      comment: id○(ar0, ar1, n) is true if all elements except those at offset n are equal;
       id○ : array × array × nat × nat;
      comment: id○(ar0, ar1, n, m) is true if all elements except those at indices [n, n + m[ are equal;
       cmp : array × elem;
   
   variables 
       m : nat;
       n : nat;
       ar : array;
       a : elem;
   
   partial functions 
       fill : array × elem × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar;
      comment: fill(ar, a, offset, len) sets len indices from offset (inclusive) to a;
       copy : array × nat × array × nat × nat → array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0;
      comment: copy(ar, m, ar0, m0, n) copy from ar at offset m into ar0 at offset m0
                   n elements and return new ar0;
       subarray : array × nat × nat → array with λ ar, m, n. m + n ≤ # ar;
      comment: subarray(ar, m, n) returns subarray of ar from offset m with length n;
   
   partial predicates 
       cmp : array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0;
      comment: cmp(ar, m, ar0, m0, n) compares n elements of ar from offset m with ar0
                    from offset m0;
       cmp : array × elem × nat × nat with λ ar, a, m, n. m + n ≤ # ar;
      comment: cmp(ar, a, m, n) is true if all elements in the range at offset m 
                    with length n are equal to a;
       idrange : array × nat × nat with λ ar, m, n. m + n ≤ # ar;
      comment: idrange(ar, m, n) is true if all elements
                    in the range at offset m with length n are equal;
   
   axioms 
      Fill-zero: fill(ar, a, m, 0) = ar;
      used for: s, ls;
      
      Fill-succ: fill(ar, a, m, n + 1) = fill(ar, a, m, n)[m + n, a];
      used for: s, ls;
      
      Fill-all: fill(ar, a) = fill(ar, a, 0, # ar);
      used for: ls;
      
      Copy-zero: copy(ar, m, ar0, m0, 0) = ar0;
      used for: s, ls;
      
      Copy-succ: copy(ar, m, ar0, m0, n + 1) = copy(ar, m, ar0, m0, n)[m0 + n, ar[m + n]];
      used for: ls;
      
      Subarray: subarray(ar, m, n) = copy(ar, m, mkarray(n), 0, n);
      used for: ls;
      
      Compare: cmp(ar, m, ar0, m0, n) ↔ (∀ n0. n0 < n → ar[m + n0] = ar0[m0 + n0]);
      
      Cmp: cmp(ar, a) ↔ (∀ n. n < # ar → ar[n] = a);
      used for: ls;
      
      Cmp-elem: cmp(ar, a, m, n) ↔ (∀ n0. n0 < n → ar[m + n0] = a);
      
      Idrange: idrange(ar, m, n) ↔ (∀ n0. n0 < n → ar[m + n0] = ar[m]);
      
      Idexcept: id○(ar0, ar1, n) ↔ # ar0 = # ar1 ∧ (∀ m. m < # ar0 ∧ m ≠ n → ar0[m] = ar1[m]);
      used for: ls;
      
      Idexcept-n: 
      id○(ar0, ar1, m, n) ↔ # ar0 = # ar1 ∧ m + n ≤ # ar0 ∧ (∀ m0. (m0 < m ∨ m + n ≤ m0) ∧ m0 < # ar0 → ar0[m0] = ar1[m0]);
      used for: ls;
   
   
end enrich