enrich
   array, 
   tid, 
   nat-div, 
   elem
with
   functions 
       mkar : Nat × Elem → Array(Elem);
       get_hash : Elem × Nat → Nat;
   
   predicates 
       allslotsfull : Array(Elem) × Nat × Nat × Elem × Bool;
       between : Nat × Nat × Nat × Bool;
       htok : Array(Elem);
       rely : Array(Elem) × Array(Elem);
   
   variables 
       ar : Array(Elem);
       e : Elem;
       tid : Tid;
       Tid : Tid flexible;
       n : Nat;
       m : Nat;
       sz : Nat;
       b : Bool;
       done : Bool;
   
   
   axioms 
      rely-def: rely(ar, ar0) ↔ # ar = # ar0 ∧ (∀ n. n < # ar → ar[n] ≠ ⊥ → ar0[n] = ar[n]);
      used for: ls;
      
      between-def: between(n0, m, n, b) ↔ n0 = n ∧ b ∨ (n < n0 ⊃ m < n ∨ n0 ≤ m;n0 ≤ m ∧ m < n);
      used for: ls;
      comment: m is between n0 (inclusive) and n (inclusive, when b is true, exclusive otherwise);
      
      allslotsfull-def: allslotsfull(ar, n0, n, e, b) ↔ (∀ m. between(n0, m, n, b) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥);
      used for: ls;
      comment: all slots between hash value and index of element are not ⊥ and not the given element.;
      
      htok-def: htok(ar) ↔ (∀ n. n < # ar ∧ ar[n] ≠ ⊥ → allslotsfull(ar, get_hash(ar[n], # ar), n, ar[n], false));
      used for: ls;
      comment: for all elements ar[n], the slots between its hash and n are occupied with different elements;
      
      hash-ok: n ≠ 0 → get_hash(e, n) < n;
      
      size-mkar: # mkar(n, e) = n;
      used for: s, ls;
      
      get-mkar: m < n → mkar(n, e)[m] = e;
      used for: s, ls;
   
   
end enrich