enrich pointers with
   predicates 
      fits : reference × storekeys × store;
      fits : reference × fieldinits × store;
      hasSharing : reference × store;
      comment: true if pointer structure has
                   any kind of sharing (two different fields of the same object with
                   the same references is considered sharing).;
       
      hasSharing : references × store;
      comment: one of the refs has sharing.;
       
      hasRefSharing : string × reference × store;
      comment: true if the pointer structure
                      beginning with r has sharing when only references are considered,
                      i.e. two different fields of the same object with the same
                      references is NOT sharing.;
       
      disjoint : string × references × store;
      comment: true if two different refs
                     in the list are disjoint, i.e. the same reference cannot be reached.;
       
      onlyModified : string × reference × store × store;
      comment: true iff every st[r0 -- sks] is the same if no path exists to r0 from r;
       
   
   axioms 
      hasSharing-def
      : ⊦ 
          hasSharing(r, st)
        ↔ (∃ sks1, sks2. 
              fits(r, sks1, st) ∧ fits(r, sks2, st) ∧ sks1 ≠ sks2 ∧ sks1 ≠ [] ∧ sks2 ≠ [] ∧ st[r -- sks1] .refval ≠ jvmref
            ∧ st[r -- sks1] = st[r -- sks2]);
      hasSharing-list-def :  ⊦ hasSharing(refs, st) ↔ (∃ r. r ∈ refs ∧ hasSharing(r, st));
      hasRefSharing-def
      : ⊦ 
          hasRefSharing(str, r, st)
        ↔ (∃ refs, refs0. 
              refs ≠ [] ∧ refs0 ≠ [] ∧ refs ≠ refs0 ∧ refs .first = r ∧ refs0 .first = r ∧ refs .last = refs0 .last ∧ refs0 .last ≠ jvmref
            ∧ validrefs(str, refs, st[r -- _type] .type, st) ∧ validrefs(str, refs0, st[r -- _type] .type, st));
      disjoint-def
      : ⊦ 
          disjoint(str, refs, st)
        ↔ ¬ (∃ refs1, refs2. 
                refs1 ≠ [] ∧ refs2 ≠ [] ∧ refs1 .first ∈ refs ∧ refs2 .first ∈ refs ∧ refs1 .first ≠ refs2 .first ∧ refs1 .last = refs2 .last
              ∧ refs1 .last ≠ jvmref ∧ validrefs(str, refs1, st[refs1 .first -- _type] .type, st)
              ∧ validrefs(str, refs2, st[refs2 .first -- _type] .type, st));
      fits-storekeys-empty :  ⊦ fits(r, [], st);
      used for : s, ls;
       
      fits-storekeys-rec
      : ⊦ 
          fits(r, sk ' + sks, st)
        ↔   r ≠ jvmref ∧ is_referencevalue(st[r -- sk]) ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class))
          ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval)
          ∧ fits(st[r -- sk] .refval, sks, st);
      fits-fieldinits-empty :  ⊦ fits(r, [], st);
      used for : s, ls;
       
      fits-fieldinits-rec
      : ⊦ 
          fits(r, (sk × val) ' + fis, st)
        ↔   r ≠ jvmref ∧ st[r -- sk] = val ∧ is_referencevalue(val)
          ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class))
          ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval)
          ∧ fits(st[r -- sk] .refval, fis, st);
      onlymodified-def :  ⊦ onlyModified(str, r, st, st0) ↔ (∀ r0, sk. ¬ path∃(str, r, r0, st) → st[r0 -- sk] = st0[r0 -- sk]);
end enrich