enrich javavalue with
   functions 
      s→r : string → reference;
      flatten : javavalue → javavalue;
      comment: shift to left, i.e. (((v0 ++ v1) ++ v2) ++ v3) ++ v4;
       
      shiftright : javavalue → javavalue;
      comment: shift to right, i.e. v0 ++ (v1 ++ (v2 ++ (v3 ++ v4)));
       
      initial_value : javatype → javavalue;
      comment: return default value for a type;
       
      type4value : javavalue → javatype;
      comment: return primtype for (prim) value;
       
      incdec : javavalue × int → javavalue;
      comment: for incdec. result depends on 1. arg.;
       
      val2int : javavalue → int;
      comment: convert byte, short, int to int;
       
      get : nat × javavalue → javavalue;
      getrange : nat × nat × javavalue → javavalue;
      . [ . ] : javavalue × reference × reference → javavalue;
      coerce : javavalue × javatype → javavalue;
      comment: coerce javavalue to given type,
                            i.e. boolvalue if type is boolean etc.;
       
   predicates 
      is_normal_mode : javavalue;
      refp : javavalue;
      comment: true if val is a reference ≠ null;
       
       . ∈ . : reference × javavalue;
      okprimtype : javavalue × javatype;
      okval : javavalue × javatype;
      comment: checks if a Java value `matches' 
                     the given type. okval(val, ty) must behave as 
                     okval(val.sval, j2stype(ty)) in java-all (fulltc/statefuns).
                     The only issue is whether void_type is acceptable or not. See the
                     corresponding axiom.;
       
   
   axioms 
      refval-xtra :  ⊦ ¬ is_referencevalue(val) → val .refval = jvmref;
      used for : s, ls;
       
      intval-xtra :  ⊦ ¬ is_integervalue(val) → val .intval = 0;
      used for : s, ls;
       
      boolval-xtra :  ⊦ ¬ is_boolvalue(val) → (val .boolval ↔ false);
      used for : s, ls;
       
      typeval-xtra :  ⊦ ¬ is_typevalue(val) → val .type = void_type;
      used for : s, ls;
       
      string2ref :  ⊦ s→r(str) = s→r(str0) ↔ str = str0;
      used for : s, ls;
       
      val2int-byte :  ⊦ val2int(byteval(by)) = b2i(by);
      used for : s, ls;
       
      val2int-short :  ⊦ val2int(shortval(sho)) = s2i(sho);
      used for : s, ls;
       
      val2int-int :  ⊦ val2int(intval(i)) = i;
      used for : s, ls;
       
      val2int-xtra :  ⊦ ¬ is_bytevalue(val) ∧ ¬ is_shortvalue(val) ∧ ¬ is_integervalue(val) → val2int(val) = 0;
      used for : s, ls;
       
      coerce-bool :  ⊦ coerce(val, boolean_type) = boolval(val .boolval);
      used for : s, ls;
       
      coerce-int :  ⊦ coerce(val, int_type) = intval(val .intval);
      used for : s, ls;
       
      coerce-short :  ⊦ coerce(val, short_type) = shortval(val .shortval);
      used for : s, ls;
       
      coerce-byte :  ⊦ coerce(val, byte_type) = byteval(val .byteval);
      used for : s, ls;
       
      coerce-long :  ⊦ coerce(val, long_type) = longval(val .longval);
      used for : s, ls;
       
      coerce-float :  ⊦ coerce(val, float_type) = floatval(val .floatval);
      used for : s, ls;
       
      coerce-double :  ⊦ coerce(val, double_type) = doubleval(val .doubleval);
      used for : s, ls;
       
      coerce-char :  ⊦ coerce(val, char_type) = charval(val .charval);
      used for : s, ls;
       
      coerce-class :  ⊦ coerce(val, mkclasstype(class)) = refval(val .refval);
      used for : s, ls;
       
      coerce-array :  ⊦ coerce(val, mkarraytype(ty)) = refval(val .refval);
      used for : s, ls;
       
      coerce-void :  ⊦ coerce(val, void_type) = refval(val .refval);
      comment: void is used for null, i.e. a reference.;
      used for : s, ls;
       
      coerce-abstract :  ⊦ coerce(val, abstract_type) = noval;
      used for : s, ls;
       
      init_val_bool :  ⊦ initial_value(boolean_type) = boolval(false);
      used for : s, ls;
       
      init_val_int :  ⊦ initial_value(int_type) = intval(0);
      used for : s, ls;
       
      init_val_short :  ⊦ initial_value(short_type) = shortval(0s);
      used for : s, ls;
       
      init_val_byte :  ⊦ initial_value(byte_type) = byteval(0b);
      used for : s, ls;
       
      init_val_class :  ⊦ initial_value(mkclasstype(class1)) = refval(jvmref);
      used for : s, ls;
       
      init_val_array :  ⊦ initial_value(mkarraytype(ty)) = refval(jvmref);
      used for : s, ls;
       
      init_val_long :  ⊦ initial_value(long_type) = longval(0l);
      used for : s, ls;
       
      init_val_char :  ⊦ initial_value(char_type) = charval(mkchar(0));
      used for : s, ls;
       
      init_val_float :  ⊦ initial_value(float_type) = floatval(0f);
      used for : s, ls;
       
      init_val_double :  ⊦ initial_value(double_type) = doubleval(0d);
      used for : s, ls;
       
      init_val_void :  ⊦ initial_value(void_type) = refval(jvmref);
      used for : s, ls;
       
      init_val_abst :  ⊦ initial_value(abstract_type) = noval;
      used for : s, ls;
       
      type4value-int :  ⊦ type4value(intval(i)) = int_type;
      used for : s, ls;
       
      type4value-byte :  ⊦ type4value(byteval(by)) = byte_type;
      used for : s, ls;
       
      type4value-short :  ⊦ type4value(shortval(sho)) = short_type;
      used for : s, ls;
       
      type4value-bool :  ⊦ type4value(boolval(boolvar)) = boolean_type;
      used for : s, ls;
       
      incdec-byte :  ⊦ is_bytevalue(val) → incdec(val, i) = byteval(i2b(b2i(val .byteval) + i));
      used for : s, ls;
       
      incdec-short :  ⊦ is_shortvalue(val) → incdec(val, i) = shortval(i2s(s2i(val .shortval) + i));
      used for : s, ls;
       
      incdec-other :  ⊦ ¬ is_bytevalue(val) ∧ ¬ is_shortvalue(val) → incdec(val, i) = intval(val .intval + i);
      used for : s, ls;
       
      refp :  ⊦ refp(val) ↔ is_referencevalue(val) ∧ val .refval ≠ jvmref;
      normal_mode :  ⊦ is_normal_mode(val) ↔ val = noval;
      used for : s, ls;
       
      base :  ⊦ ¬ is_valuelist(val) → flatten(val) = val;
      used for : s, ls, ls;
       
      flatten-shift :  ⊦ ¬ is_valuelist(val0) → flatten(val ++ val0) = flatten(val) ++ val0;
      used for : s, ls, lc;
       
      flatten-rec :  ⊦ flatten(val ++ (val0 ++ val1)) = flatten(val ++ val0 ++ val1);
      used for : s, ls;
       
      shiftright-base :  ⊦ ¬ is_valuelist(val) → shiftright(val) = val;
      used for : s, ls, ls;
       
      shiftright-shift :  ⊦ ¬ is_valuelist(val) → shiftright(val ++ val0) = shiftright(val) ++ val0;
      used for : s, ls, lc;
       
      shiftright-rec :  ⊦ shiftright(val ++ val0 ++ val1) = shiftright(val ++ (val0 ++ val1));
      used for : s, ls;
       
      refin-int :  ⊦ ¬ r ∈ intval(i);
      used for : s, ls;
       
      refin-byte :  ⊦ ¬ r ∈ byteval(by);
      used for : s, ls;
       
      refin-short :  ⊦ ¬ r ∈ shortval(sho);
      used for : s, ls;
       
      refin-ref :  ⊦ r ∈ refval(r0) ↔ r = r0;
      used for : s, ls;
       
      refin-bool :  ⊦ ¬ r ∈ boolval(boolvar);
      used for : s, ls;
       
      refin-string :  ⊦ ¬ r ∈ stringval(stringvar);
      used for : s, ls;
       
      refin-list :  ⊦ r ∈ val ++ val0 ↔ r ∈ val ∨ r ∈ val0;
      used for : s, ls;
       
      refin-noval :  ⊦ ¬ r ∈ noval;
      used for : s, ls;
       
      refin-type :  ⊦ ¬ r ∈ typeval(ty);
      used for : s, ls;
       
      refin-initval :  ⊦ ¬ r ∈ initval(istate);
      used for : s, ls;
       
      refin-break :  ⊦ ¬ r ∈ break(lbl);
      used for : s, ls;
       
      refin-continue :  ⊦ ¬ r ∈ continue(lbl);
      used for : s, ls;
       
      refin-return :  ⊦ r ∈ return(val, ty) ↔ r ∈ val;
      used for : s, ls;
       
      refin-throw :  ⊦ r ∈ throw(r0, ty) ↔ r = r0;
      used for : s, ls;
       
      refin-long :  ⊦ ¬ r ∈ longval(lo);
      used for : s, ls;
       
      refin-float :  ⊦ ¬ r ∈ floatval(floatvar);
      used for : s, ls;
       
      refin-double :  ⊦ ¬ r ∈ doubleval(doublevar);
      used for : s, ls;
       
      refin-char :  ⊦ ¬ r ∈ charval(jchar);
      used for : s, ls;
       
      replref-int :  ⊦ (intval(i)[r, r0]) = intval(i);
      used for : s, ls;
       
      replref-byte :  ⊦ (byteval(by)[r, r0]) = byteval(by);
      used for : s, ls;
       
      replref-short :  ⊦ (shortval(sho)[r, r0]) = shortval(sho);
      used for : s, ls;
       
      replref-ref :  ⊦ (refval(r1)[r, r0]) = refval((r1 = r ⊃ r0; r1));
      used for : s, ls;
       
      replref-bool :  ⊦ (boolval(boolvar)[r, r0]) = boolval(boolvar);
      used for : s, ls;
       
      replref-string :  ⊦ (stringval(stringvar)[r, r0]) = stringval(stringvar);
      used for : s, ls;
       
      replref-list :  ⊦ (val ++ val0)[r, r0] = val[r, r0] ++ val0[r, r0];
      used for : s, ls;
       
      replref-noval :  ⊦ noval[r, r0] = noval;
      used for : s, ls;
       
      replref-type :  ⊦ (typeval(ty)[r, r0]) = typeval(ty);
      used for : s, ls;
       
      replref-initval :  ⊦ (initval(istate)[r, r0]) = initval(istate);
      used for : s, ls;
       
      replref-break :  ⊦ (break(lbl)[r, r0]) = break(lbl);
      used for : s, ls;
       
      replref-continue :  ⊦ (continue(lbl)[r, r0]) = continue(lbl);
      used for : s, ls;
       
      replref-return :  ⊦ (return(val, ty)[r, r0]) = return(val[r, r0], ty);
      used for : s, ls;
       
      replref-throw :  ⊦ (throw(r1, ty)[r, r0]) = throw((r1 = r ⊃ r0; r1), ty);
      used for : s, ls;
       
      replref-long :  ⊦ (longval(lo)[r, r0]) = longval(lo);
      used for : s, ls;
       
      replref-float :  ⊦ (floatval(floatvar)[r, r0]) = floatval(floatvar);
      used for : s, ls;
       
      replref-double :  ⊦ (doubleval(doublevar)[r, r0]) = doubleval(doublevar);
      used for : s, ls;
       
      replref-char :  ⊦ (charval(jchar)[r, r0]) = charval(jchar);
      used for : s, ls;
       
      getRange-base :  ⊦ getrange(m, m, val) = get(m, val);
      getRange-rec :  ⊦ m < n → getrange(m, n, val) = getrange(m, n -1, val) ++ get(n, val);
      get-zero :  ⊦ get(0, val) = shiftright(val) .firstval;
      get-rec :  ⊦ get(m +1, val) = get(m, shiftright(val) .restval);
      okprimtype-bool :  ⊦ okprimtype(val, boolean_type) ↔ is_boolvalue(val);
      used for : s, ls;
       
      okprimtype-int :  ⊦ okprimtype(val, int_type) ↔ is_integervalue(val);
      used for : s, ls;
       
      okprimtype-short :  ⊦ okprimtype(val, short_type) ↔ is_shortvalue(val);
      used for : s, ls;
       
      okprimtype-byte :  ⊦ okprimtype(val, byte_type) ↔ is_bytevalue(val);
      used for : s, ls;
       
      okprimtype-long :  ⊦ okprimtype(val, long_type) ↔ is_longvalue(val);
      used for : s, ls;
       
      okprimtype-float :  ⊦ okprimtype(val, float_type) ↔ is_floatvalue(val);
      used for : s, ls;
       
      okprimtype-double :  ⊦ okprimtype(val, double_type) ↔ is_doublevalue(val);
      used for : s, ls;
       
      okprimtype-char :  ⊦ okprimtype(val, char_type) ↔ is_charvalue(val);
      used for : s, ls;
       
      okprimtype-class :  ⊦ ¬ okprimtype(val, mkclasstype(class1));
      used for : s, ls;
       
      okprimtype-array :  ⊦ ¬ okprimtype(val, mkarraytype(ty));
      used for : s, ls;
       
      okprimtype-void :  ⊦ ¬ okprimtype(val, void_type);
      used for : s, ls;
       
      okprimtype-abstract :  ⊦ ¬ okprimtype(val, abstract_type);
      used for : s, ls;
       
      okval-bool :  ⊦ okval(val, boolean_type) ↔ is_boolvalue(val);
      used for : s, ls;
       
      okval-int :  ⊦ okval(val, int_type) ↔ is_integervalue(val);
      used for : s, ls;
       
      okval-short :  ⊦ okval(val, short_type) ↔ is_shortvalue(val);
      used for : s, ls;
       
      okval-byte :  ⊦ okval(val, byte_type) ↔ is_bytevalue(val);
      used for : s, ls;
       
      okval-long :  ⊦ okval(val, long_type) ↔ is_longvalue(val);
      used for : s, ls;
       
      okval-float :  ⊦ okval(val, float_type) ↔ is_floatvalue(val);
      used for : s, ls;
       
      okval-double :  ⊦ okval(val, double_type) ↔ is_doublevalue(val);
      used for : s, ls;
       
      okval-char :  ⊦ okval(val, char_type) ↔ is_charvalue(val);
      used for : s, ls;
       
      okval-class :  ⊦ okval(val, mkclasstype(class1)) ↔ is_referencevalue(val);
      used for : s, ls;
       
      okval-array :  ⊦ okval(val, mkarraytype(ty)) ↔ is_referencevalue(val);
      used for : s, ls;
       
      okval-void :  ⊦ okval(val, void_type) ↔ is_referencevalue(val);
      comment: null has type void, and is compatible with references.;
      used for : s, ls;
       
      okval-abstract :  ⊦ ¬ okval(val, abstract_type);
      used for : s, ls;
       
end enrich