enrich cyclic , 
       reflistset with
   functions 
      validrefset : string × reference × store → referencesset;
      maxpath : string × reference × store → nat;
   predicates 
      ps= : reference × store × reference × store;
      unchanged : string × reference × store × store;
      unchangedNorec : reference × store × store;
      comment: all fields or indices of r are the same in 
                                                           both stores. Used in unchanged for
                                                           the recursive version.;
       
   
   axioms 
      pseq-def
      : ⊦ 
          ps=(r, st, r1, st1)
        ↔   r = jvmref ∧ r1 = jvmref
          ∨   r ≠ jvmref ∧ r1 ≠ jvmref ∧ st[r -- _type] = st1[r1 -- _type]
            ∧ (  is_classtype(st[r -- _type] .type)
               →   (∀ fs. 
                       fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs '])
                     → ps=(st[r -- fs '] .refval, st, st1[r1 -- fs '] .refval, st1))
                 ∧ (∀ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ ¬ is_referencevalue(st[r -- fs ']) → st[r -- fs '] = st1[r1 -- fs ']))
            ∧ (  is_arraytype(st[r -- _type] .type)
               →   st[r -- _length] .intval = st1[r1 -- _length] .intval
                 ∧ (∀ i. 
                       0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i '])
                     → ps=(st[r -- i '] .refval, st, st1[r1 -- i '] .refval, st1))
                 ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ ¬ is_referencevalue(st[r -- i ']) → st[r -- i '] = st1[r1 -- i ']));
      unchangedNorec-def
      : ⊦ 
          unchangedNorec(r, st, st0)
        ↔   r = jvmref
          ∨   r ≠ jvmref ∧ st[r -- _type] = st0[r -- _type]
            ∧ (is_classtype(st[r -- _type] .type) → (∀ fs. fs ' ∈ instfields(st[r -- _type] .type .class) → st[r -- fs '] = st0[r -- fs ']))
            ∧ (  is_arraytype(st[r -- _type] .type)
               → st[r -- _length] = st0[r -- _length] ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] = st0[r -- i ']));
      unchanged-def
      : ⊦ 
        unchanged(str, r, st, st0) ↔ (∀ r0. (path∃(str, r, r0, st) ↔ path∃(str, r, r0, st0)) ∧ (path∃(str, r, r0, st) → unchangedNorec(r0, st, st0)));
      validrefset-empty :  ⊦ ¬ is_valid_ref(str, r, st) → validrefset(str, r, st) = ∅;
      validrefset-def
      : ⊦ 
          is_valid_ref(str, r, st)
        → (  refs ∈ validrefset(str, r, st)
           ↔ refs ≠ [] ∧ refs .first = r ∧ ¬ has_reffield(refs .last, st) ∧ ¬ dups(refs) ∧ validrefs(str, refs, st[r -- _type] .type, st));
      maxpath-zero :  ⊦ validrefset(str, r, st) = ∅ → maxpath(str, r, st) = 0;
      maxpath-in :  ⊦ validrefset(str, r, st) ≠ ∅ → (∃ refs. refs ∈ validrefset(str, r, st) ∧ maxpath(str, r, st) = # refs);
      maxpath-max :  ⊦ refs ∈ validrefset(str, r, st) → # refs ≤ maxpath(str, r, st);
end enrich