enrich storefunsx , 
       valuesfuns with
   functions 
      arraycopy : reference × int × reference × int × int × store → store;
      getarrayv : reference × int × int × store → javavalue;
      getarrayv : reference × store → javavalue;
      getarray : reference × store → javavalues;
      getarray : reference × int × int × store → javavalues;
      putArray : javavalues × reference × store → store;
      putArray : javavalues × reference × int × store → store;
      getintarray : reference × store → intlist;
      getintarray : reference × int × int × store → intlist;
      comment: getintarray(r, offset, length, st);
       
      getbytearray : reference × store → bytelist;
      getbytearray : reference × int × int × store → bytelist;
      comment: getbytearray(r, offset, length, st);
       
      putByteArray : bytelist × reference × store → store;
      putByteArray : bytelist × reference × int × store → store;
      comment: int is the offset.;
       
   predicates 
      is_arrayref : reference × int × store;
      arraycomp : reference × int × reference × int × int × store;
   
   axioms 
      is_arrayref :  ⊦ is_arrayref(r, i, st) ↔ (∀ j. 0 ≤ j ∧ j < i → r -- j ' ∈ st);
      arrayComp :  ⊦ arraycomp(r1, i1, r2, i2, j, st) ↔ (∀ i. 0 ≤ i ∧ i < j → st[r1 -- (i1 + i) '] = st[r2 -- (i2 + i) ']);
      used for : ls;
       
      arrayCopy-base :  ⊦ j ≤ 0 → arraycopy(r1, i1, r2, i2, j, st) = st;
      arrayCopy-rec
      :  ⊦ 0 < j → arraycopy(r1, i1, r2, i2, j, st) = arraycopy(r1, i1, r2, i2, j - 1, st[r2 -- (i2 + j - 1) ', st[r1 -- (i1 + j - 1) ']]);
      getArray-zero :  ⊦ j ≤ 0 → getarray(r, i, j, st) = [];
      used for : s, ls;
       
      getArray-one :  ⊦ getarray(r, i, 1, st) = st[r -- i '] ';
      getArray-rec :  ⊦ 1 < j → getarray(r, i, j, st) = getarray(r, i, j - 1, st) + st[r -- (i + j - 1) '];
      getArray-all :  ⊦ getarray(r, st) = getarray(r, 0, st[r -- _length] .intval, st);
      putArray-all :  ⊦ putArray(vals, r, st) = putArray(vals, r, 0, st);
      putArray-empty :  ⊦ putArray([], r, i, st) = st;
      used for : s, ls;
       
      putArray-rec :  ⊦ putArray(val ' + vals, r, i, st) = (putArray(vals, r, i + 1, st)[r -- i ', val]);
      used for : s, ls;
       
      getintarray-def :  ⊦ getintarray(r, st) = getintarray(r, 0, st[r -- _length] .intval, st);
      getintarray :  ⊦ getintarray(r, i, j, st) = intvalues(getarray(r, i, j, st));
      used for : s, ls;
       
      getByteArray-all :  ⊦ getbytearray(r, st) = getbytearray(r, 0, st[r -- _length] .intval, st);
      getByteArray :  ⊦ getbytearray(r, i, j, st) = bytevalues(getarray(r, i, j, st));
      used for : s, ls;
       
      putByteArray-all :  ⊦ putByteArray(bytes, r, st) = putByteArray(bytes, r, 0, st);
      putByteArray :  ⊦ putByteArray(bytes, r, i, st) = putArray(mkjavavalues(bytes), r, i, st);
      getArrayv-zero :  ⊦ j ≤ 0 → getarrayv(r, i, j, st) = noval;
      getArrayv-one :  ⊦ getarrayv(r, i, 1, st) = st[r -- i '];
      getArrayv-rec :  ⊦ 1 < j → getarrayv(r, i, j, st) = getarrayv(r, i, j - 1, st) ++ st[r -- (i + j - 1) '];
      getArrayv-all :  ⊦ getarrayv(r, st) = getarrayv(r, 0, st[r -- _length] .intval, st);
end enrich