enrich pointers , 
       javatypes with
   predicates 
      contains : string × javatype × javatype;
      contains : string × javatypes;
      contains : string × javatype × fieldspec;
      same-subclasses-contains : classname × string × string;
      comment: same-subclasses-contains(class, str, str0): 
                                class has the same subclasses at level str0 as at level str,
                                and the same is true for all contained classes.;
       
   
   axioms 
      contains-type-def :  ⊦ contains(str, ty, ty0) ↔ (∃ tys. contains(str, ty ' + (tys + ty0)));
      comment: contains(str, ty, ty0) is true only if ty contains a 
                             (recursive) field of type ty0 (or a super type).
                             Note that ty0 may be a primitive type.;
       
      contains-one :  ⊦ contains(str, ty ') ↔ type∃(str, ty);
      contains-rec
      : ⊦ 
          contains(str, ty ' + ty0 ' + tys)
        ↔   type∃(str, ty) ∧ is_reftype(ty)
          ∧ (∃ ty1. 
                ty1 ≤ ty ∧ type∃(str, ty1)
              ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ ty0 ≤ fs .type))
              ∧ (is_arraytype(ty1) → ty0 ≤ ty1 .type) ∧ contains(str, ty0 ' + tys));
      comment: this version ignores int in array length fields.
                         We explicitly exclude interfaces because instfields is not specified for interfaces.;
       
      contains-field-def
      : ⊦ 
          contains(str, ty, fs)
        ↔   type∃(str, ty)
          ∧ (∃ tys. 
                tys ≠ [] ∧ tys .first ≤ ty ∧ contains(str, tys) ∧ is_reftype(tys .last)
              ∧ (is_classtype(tys .last) → ¬ interface∃(str, tys .last .class) ∧ fs ' ∈ instfields(tys .last .class))
              ∧ (is_arraytype(tys .last) → fs ' = _length));
      comment: we do not use contains(str, ty, ty0) because we want to allow that ty contains the field.
                    We explicitly exclude interfaces because instfields is not specified for interfaces.;
       
      same-subclasses-all-def
      : ⊦ 
          same-subclasses-contains(class, str, str0)
        ↔ same-subclasses(class, str, str0) ∧ (∀ class0. contains(str0, mkclasstype(class), mkclasstype(class0)) → same-subclasses(class0, str, str0));
end enrich