Proof step 37 from proof pseq-subset (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ 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 ']))

• Proof step 36:

  st2[r -- _type] = st1[r1 -- _type], st[r -- _type] = st1[r1 -- _type], st1[r1 -- _type] .type = mkclasstype(class), st2[r -- fs '] = refval(jvmref), st[r -- fs '] = refval(jvmref), ps=(jvmref, st, st1[r1 -- fs '] .refval, st1), r -- fs ' ∈ st, r -- fs ' ∈ st2, fs ' ∈ instfields(class), r -- _type ∈ st, r -- _type ∈ st2, r ∈ st, r ∈ st2, is_obj(str, r1, st1), is_obj(str, r, st), is_reftype(fs .type), ∀ rk. rk ∈ st → rk ∈ st2 ∧ st[rk] = st2[rk], ∀ fs. fs ' ∈ instfields(class) ∧ ¬ is_referencevalue(st[r -- fs ']) → st[r -- fs '] = st1[r1 -- fs '], ∀ fs. fs ' ∈ instfields(class) ∧ is_referencevalue(st[r -- fs ']) → ps=(st[r -- fs '] .refval, st, st1[r1 -- fs '] .refval, st1), junkref(str, st1[r1 -- fs '] .refval, st1) ∨ cyclic(str, st1[r1 -- fs '] .refval, st1), ∀ st1, r1, st2, st0, r0, str0. maxpath(str0, r0, st0) < maxpath(str, r, st) → ( st0 ⊆ st2 ∧ ps=(r0, st0, r1, st1) → junkref(str0, r0, st0) ∨ cyclic(str0, r0, st0) ∨ junkref(str0, r1, st1) ∨ cyclic(str0, r1, st1) ∨ ps=(r0, st2, r1, st1)) ⊦ r1 = jvmref, r = jvmref, jvmref = jvmref ∧ st1[r1 -- fs '] .refval = jvmref ∨ jvmref ≠ jvmref ∧ st1[r1 -- fs '] .refval ≠ jvmref ∧ st2[jvmref -- _type] = st1[st1[r1 -- fs '] .refval -- _type] ∧ ( is_classtype(st2[jvmref -- _type] .type) → (∀ fs0. fs0 ' ∈ instfields(st2[jvmref -- _type] .type .class) ∧ is_referencevalue(st2[jvmref -- fs0 ']) → ps=(st2[jvmref -- fs0 '] .refval, st2, st1[st1[r1 -- fs '] .refval -- fs0 '] .refval, st1)) ∧ (∀ fs0. fs0 ' ∈ instfields(st2[jvmref -- _type] .type .class) ∧ ¬ is_referencevalue(st2[jvmref -- fs0 ']) → st2[jvmref -- fs0 '] = st1[st1[r1 -- fs '] .refval -- fs0 '])) ∧ ( is_arraytype(st2[jvmref -- _type] .type) → st2[jvmref -- _length] .intval = st1[st1[r1 -- fs '] .refval -- _length] .intval ∧ (∀ i. 0 ≤ i ∧ i < st2[jvmref -- _length] .intval ∧ is_referencevalue(st2[jvmref -- i ']) → ps=(st2[jvmref -- i '] .refval, st2, st1[st1[r1 -- fs '] .refval -- i '] .refval, st1)) ∧ (∀ i. 0 ≤ i ∧ i < st2[jvmref -- _length] .intval ∧ ¬ is_referencevalue(st2[jvmref -- i ']) → st2[jvmref -- i '] = st1[st1[r1 -- fs '] .refval -- i '])), cyclic(str, r1, st1), junkref(str, r1, st1), cyclic(str, r, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st1, st1[r1 -- fs '] .refval, st2, jvmref)]]