enrich javavalues , 
       intlist
 , 
       valuetypes with
   functions 
      val2vals : javavalue → javavalues;
      bytevalues : javavalues → bytelist;
      intvalues : javavalues → intlist;
      intvalues : intlist → javavalues;
      mkjavavalues : bytelist → javavalues;
      mkjavavalues : references → javavalues;
      vals2ints : javavalues → intlist;
      mkjavavalue : bytelist → javavalue;
      vals2val : javavalues → javavalue;
      is2bs : intlist → bytelist;
      bs2is : bytelist → intlist;
       . .nonnullrefs : javavalues → references;
      comment: select non-null references, discard other values.;
       
   predicates 
      posints : intlist;
      posints : javavalue;
      posints : javavalues;
      is_bytelist : javavalues;
      is_bytelistlist : javavalues;
   
   axioms 
      mkjval-def :  ⊦ mkjavavalue(bytes) = vals2val(mkjavavalues(bytes));
      vals2val-empty :  ⊦ vals2val([]) = noval;
      used for : s, ls;
       
      vals2val-rec :  ⊦ vals2val(val ' + vals) = val ++ vals2val(vals);
      used for : s, ls;
       
      vals-empty :  ⊦ val2vals(noval) = [];
      used for : s, ls;
       
      vals-rec :  ⊦ val2vals(val ++ val0) = val + val2vals(val0);
      used for : s, ls;
       
      bytevalues-empty :  ⊦ bytevalues([]) = [];
      used for : s, ls;
       
      bytevalues-rec :  ⊦ bytevalues(val ' + vals) = val .byteval + bytevalues(vals);
      used for : s, ls;
       
      is_bytelist-empty :  ⊦ is_bytelist([]);
      used for : s, ls;
       
      is_bytelist-rec :  ⊦ is_bytelist(val ' + vals) ↔ is_bytevalue(val) ∧ is_bytelist(vals);
      used for : s, ls;
       
      is_bytelistlist-empty :  ⊦ is_bytelistlist([]);
      used for : s, ls;
       
      is_bytelistlist-rec :  ⊦ is_bytelistlist(val ' + vals) ↔ is_bytelist(val2vals(val)) ∧ is_bytelistlist(vals);
      used for : s, ls;
       
      intvalues-empty :  ⊦ intvalues([]) = [];
      used for : s, ls;
       
      intvalues-rec :  ⊦ intvalues(val ' + vals) = val .intval + intvalues(vals);
      used for : s, ls;
       
      intvalues-empty :  ⊦ intvalues([]) = [];
      used for : s, ls;
       
      intvalues-rec :  ⊦ intvalues(i ' + ints) = intval(i) + intvalues(ints);
      used for : s, ls;
       
      vals2ints-empty :  ⊦ vals2ints([]) = [];
      used for : s, ls;
       
      vals2ints-rec :  ⊦ vals2ints(val ' + vals) = val2int(val) + vals2ints(vals);
      used for : s, ls;
       
      posints-value :  ⊦ posints(val) ↔ posints(intvalues(val2vals(val)));
      used for : s, ls;
       
      posints-values :  ⊦ posints(vals) ↔ posints(intvalues(vals));
      used for : s, ls;
       
      posints-empty :  ⊦ posints([]);
      used for : s, ls;
       
      posints-rec :  ⊦ posints(i ' + ints) ↔ 0 ≤ i ∧ posints(ints);
      used for : s, ls;
       
      mkvalsb-empty :  ⊦ mkjavavalues([]) = [];
      used for : s, ls;
       
      mkvalsb-rec :  ⊦ mkjavavalues(by ' + bytes) = byteval(by) ' + mkjavavalues(bytes);
      used for : s, ls;
       
      mkvalsr-empty :  ⊦ mkjavavalues([]) = [];
      used for : s, ls;
       
      mkvalsr-rec :  ⊦ mkjavavalues(r ' + refs) = refval(r) ' + mkjavavalues(refs);
      used for : s, ls;
       
      ints2bytes-empty :  ⊦ is2bs([]) = [];
      used for : s, ls;
       
      ints2bytes-rec :  ⊦ is2bs(i ' + ints) = i2b(i) ' + is2bs(ints);
      used for : s, ls;
       
      bytes2ints-empty :  ⊦ bs2is([]) = [];
      used for : s, ls;
       
      bytes2ints-rec :  ⊦ bs2is(by ' + bytes) = b2i(by) ' + bs2is(bytes);
      used for : s, ls;
       
      nonnullrefs-empty :  ⊦ [] .nonnullrefs = [];
      used for : s, ls;
       
      nonnullrefs-no :  ⊦ ¬ is_referencevalue(val) ∨ val .refval = jvmref → (val ' + vals) .nonnullrefs = vals .nonnullrefs;
      nonnullrefs-yes :  ⊦ is_referencevalue(val) ∧ val .refval ≠ jvmref → (val ' + vals) .nonnullrefs = val .refval + vals .nonnullrefs;
      used for : s, ls;
       
end enrich