enrich okfuns with
   functions 
      addobj : reference × classname × fieldinits × store → store;
      addobj : reference × classname × storekeys × store → store;
      addobj : reference × classname × store → store;
      addclass : classname × fieldinits × store → store;
      statfields : classname → storekeys;
      comment: only trivial axioms, others are added by Java classes.;
       
      instfields : classname → storekeys;
      comment: only trivial axioms, others are added by Java classes.;
       
   predicates 
      is_obj : reference × classname × storekeys × store;
      comment: not null, runtime type = class.;
       
      is_obj : reference × classname × store;
      comment: not null, runtime type must be = class, not ≤.;
       
      is_obj : reference × store;
      comment: not null, arbitrary object.;
       
      is_obj : string × reference × store;
      comment: not null, arbitrary object, no interface, not abstract
.;
       
      is_obj_exact : reference × classname × storekeys × store;
      is_valid_ref : string × reference × store;
      is_valid_ref : reference × store;
      has_reffield : reference × store;
      okfieldinits : classname × fieldinits;
      okstatfields : classname × store;
      validfieldinits : fieldinits × store;
   
   axioms 
      addobj-simple :  ⊦ addobj(r, class, st) = addobj(r, class, instfields(class), st);
      addobj-keysempty :  ⊦ addobj(r, class, [], st) = st[r -- _type, typeval(mkclasstype(class))];
      used for : ls;
       
      addobj-keysrec :  ⊦ addobj(r, class, sk ' + sks, st) = (addobj(r, class, sks, st)[r -- sk, initial_value(sk .fs .type)]);
      addobj-base :  ⊦ addobj(r, class1, [], st) = st[r -- _type, typeval(mkclasstype(class1))];
      used for : ls;
       
      addobj-rec :  ⊦ addobj(r, class1, (sk × val) ' + fis, st) = (addobj(r, class1, fis, st)[r -- sk, val]);
      used for : ls;
       
      addclass-base :  ⊦ addclass(class1, [], st) = st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)];
      used for : ls;
       
      addclass-yes
      : ⊦ 
        addclass(class1, (mkfs(class1, ty, fieldvar) ' × val) ' + fis, st) = (addclass(class1, fis, st)[jvmref -- mkfs(class1, ty, fieldvar) ', val]);
      used for : ls;
       
      addclass-no1 :  ⊦ class1 ≠ class2 → addclass(class1, (mkfs(class2, ty, fieldvar) ' × val) ' + fis, st) = addclass(class1, fis, st);
      used for : ls;
       
      addclass-no2 :  ⊦ addclass(class1, (i ' × val) ' + fis, st) = addclass(class1, fis, st);
      used for : ls;
       
      is_obj :  ⊦ is_obj(r, class1, sks, st) ↔ r ≠ jvmref ∧ (r -- _type) × typeval(mkclasstype(class1)) ∈ st ∧ goodfieldsandtypes(r, sks, st);
      is_obj_exact
      :  ⊦ is_obj_exact(r, class1, sks, st) ↔ r ≠ jvmref ∧ (r -- _type) × typeval(mkclasstype(class1)) ∈ st ∧ exactfieldsandtypes(r, sks, st);
      is_obj-def
      :  ⊦ is_obj(r, class, st) ↔ r ≠ jvmref ∧ (r -- _type) × typeval(mkclasstype(class)) ∈ st ∧ goodfieldsandtypes(r, instfields(class), st);
      is-any-object
      : ⊦ 
          is_obj(r, st)
        ↔   r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_classtype(st[r -- _type] .type)
          ∧ is_obj(r, st[r -- _type] .type .class, st);
      is-real-object-def
      :  ⊦ is_obj(str, r, st) ↔ class+∃(str, st[r -- _type] .type .class) ∧ ¬ is_abstract(st[r -- _type] .type .class) ∧ is_obj(r, st);
      is-valid-ref :  ⊦ is_valid_ref(r, st) ↔ is_obj(r, st) ∨ is_array(r, st);
      is-valid-ref-stronger-def :  ⊦ is_valid_ref(str, r, st) ↔ is_obj(str, r, st) ∨ is_array(str, r, st);
      has_reffield-no :  ⊦ ¬ is_valid_ref(r, st) → ¬ has_reffield(r, st);
      has_reffield-class :  ⊦ is_obj(r, st) → (has_reffield(r, st) ↔ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_reftype(fs .type)));
      has_reffield-array
      : ⊦ 
          is_array(r, st)
        → (has_reffield(r, st) ↔ st[r -- _length] .intval > 0 ∧ (is_reftype(st[r -- _type] .type .type) ∨ st[r -- _type] .type .type = void_type));
      okfieldinits-empty :  ⊦ okfieldinits(class, []);
      used for : s, ls;
       
      okfieldinits-rec
      : ⊦ 
          okfieldinits(class, (sk × val) ' + fis)
        ↔ is_fskey(sk) ∧ val = initial_value(sk .fs .type) ∧ sk .fs .class = class ∧ sk .fs .type ≠ abstract_type ∧ okfieldinits(class, fis);
      okstatfields-def :  ⊦ okstatfields(class, st) ↔ goodfieldsandtypes(jvmref, statfields(class), st);
      validfieldinits-all
      : ⊦ 
          validfieldinits(fis, st)
        ↔ (∀ sk, val. 
              sk × val ∈ fis
            →   is_fskey(sk) ∧ oktype(val, sk .fs .type, st)
              ∧ (  is_referencevalue(val)
                 →   val .refval = jvmref
                   ∨ val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type ≤ sk .fs .type));
      statfields-predef :  ⊦ is_predefined_class(class) → statfields(class) = [];
      used for : s, ls;
       
      instfields-predef :  ⊦ is_predefined_class(class) → instfields(class) = [];
      used for : s, ls;
       
      statfields-special :  ⊦ ¬ mkfs(class0, void_type, fieldvar) ' ∈ statfields(class);
      used for : s, ls;
       
      instfields-special :  ⊦ ¬ mkfs(class0, void_type, fieldvar) ' ∈ instfields(class);
      used for : s, ls;
       
      statfields-abstract :  ⊦ ¬ mkfs(class0, abstract_type, fieldvar) ' ∈ statfields(class);
      used for : s, ls;
       
      instfields-abstract :  ⊦ ¬ mkfs(class0, abstract_type, fieldvar) ' ∈ instfields(class);
      used for : s, ls;
       
      statfields-index :  ⊦ ¬ i ' ∈ statfields(class);
      used for : s, ls;
       
      instfields-index :  ⊦ ¬ i ' ∈ instfields(class);
      used for : s, ls;
       
      statfields-nodups :  ⊦ ¬ dups(statfields(class));
      used for : s, ls;
       
      instfields-nodups :  ⊦ ¬ dups(instfields(class));
      used for : s, ls;
       
      statfields-typeex :  ⊦ mkfs(class0, ty, fieldvar) ' ∈ statfields(class0) ∧ tdname+∃(str, class0) → type∃(str, ty);
      instfields-typeex :  ⊦ mkfs(class0, ty, fieldvar) ' ∈ instfields(class) ∧ tdname+∃(str, class) → type∃(str, ty);
      statfields-same-class :  ⊦ mkfs(class0, ty, fieldvar) ' ∈ statfields(class) → class = class0;
      instfields-subclass :  ⊦ fs ' ∈ instfields(class) ∧ class0 ≤ class → fs ' ∈ instfields(class0);
      used for : s, ls;
       
end enrich