Proof step 197 from proof pseq-sym-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ 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 196:

  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. ¬ i < 0 ∧ ¬ st[r -- _length] .intval ≤ i ∧ is_referencevalue(st[r -- i ']) → ps=(st[r -- i '] .refval, st, st1[r1 -- i '] .refval, st1)) ∧ (∀ i. ¬ i < 0 ∧ ¬ st[r -- _length] .intval ≤ i ∧ ¬ is_referencevalue(st[r -- i ']) → st[r -- i '] = st1[r1 -- i '])), ∀ st, r, st0, r0, str0. maxpath(str0, r0, st0) < maxpath(str, r1, st1) → ( true → ( ¬ cyclic(str0, r, st) ∧ ¬ cyclic(str0, r0, st0) ∧ ¬ junkref(str0, r, st) ∧ ¬ junkref(str0, r0, st0) → (ps=(r, st, r0, st0) → ps=(r0, st0, r, st)))) ⊦ cyclic(str, r, st), cyclic(str, r1, st1), junkref(str, r, st), junkref(str, r1, st1), r1 = jvmref ∧ r = jvmref ∨ r1 ≠ jvmref ∧ r ≠ jvmref ∧ st1[r1 -- _type] = st[r -- _type] ∧ ( is_classtype(st1[r1 -- _type] .type) → (∀ fs. fs ' ∈ instfields(st1[r1 -- _type] .type .class) ∧ is_referencevalue(st1[r1 -- fs ']) → ps=(st1[r1 -- fs '] .refval, st1, st[r -- fs '] .refval, st)) ∧ (∀ fs. fs ' ∈ instfields(st1[r1 -- _type] .type .class) ∧ ¬ is_referencevalue(st1[r1 -- fs ']) → st1[r1 -- fs '] = st[r -- fs '])) ∧ ( is_arraytype(st1[r1 -- _type] .type) → st1[r1 -- _length] .intval = st[r -- _length] .intval ∧ (∀ i. 0 ≤ i ∧ i < st1[r1 -- _length] .intval ∧ is_referencevalue(st1[r1 -- i ']) → ps=(st1[r1 -- i '] .refval, st1, st[r -- i '] .refval, st)) ∧ (∀ i. 0 ≤ i ∧ i < st1[r1 -- _length] .intval ∧ ¬ is_referencevalue(st1[r1 -- i ']) → st1[r1 -- i '] = st[r -- i ']))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, r, st1, r1)]]