[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

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

st[r -- _type] = st1[r1 -- _type], ∀ rk. rk ∈ st → rk ∈ st2 ∧ st[rk] = st2[rk], is_classtype(st1[r1 -- _type] .type) → (∀ fs. fs ' ∈ instfields(st1[r1 -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) → ps=(st[r -- fs '] .refval, st, st1[r1 -- fs '] .refval, st1)) ∧ (∀ fs. fs ' ∈ instfields(st1[r1 -- _type] .type .class) ∧ ¬ is_referencevalue(st[r -- fs ']) → st[r -- fs '] = st1[r1 -- fs ']), is_arraytype(st1[r1 -- _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 ']), ∀ 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, cyclic(str, r1, st1), junkref(str, r1, st1), cyclic(str, r, st), junkref(str, r, st), st2[r -- _type] = st1[r1 -- _type] ∧ ( is_classtype(st2[r -- _type] .type) → ( fs ' ∈ instfields(st2[r -- _type] .type .class) ∧ is_referencevalue(st2[r -- fs ']) → ps=(st2[r -- fs '] .refval, st2, st1[r1 -- fs '] .refval, st1)) ∧ (fs0 ' ∈ instfields(st2[r -- _type] .type .class) ∧ ¬ is_referencevalue(st2[r -- fs0 ']) → st2[r -- fs0 '] = st1[r1 -- fs0 '])) ∧ ( is_arraytype(st2[r -- _type] .type) → st2[r -- _length] .intval = st1[r1 -- _length] .intval ∧ (0 ≤ i ∧ i < st2[r -- _length] .intval ∧ is_referencevalue(st2[r -- i ']) → ps=(st2[r -- i '] .refval, st2, st1[r1 -- i '] .refval, st1)) ∧ (0 ≤ i0 ∧ i0 < st2[r -- _length] .intval ∧ ¬ is_referencevalue(st2[r -- i0 ']) → st2[r -- i0 '] = st1[r1 -- i0 ']))

User applied rule all left

And obtained the following new goals

Proof step 207:
st[r -- _type] = st1[r1 -- _type], r -- _type ∈ st → r -- _type ∈ st2 ∧ st[r -- _type] = st2[r -- _type], ∀ rk. rk ∈ st → rk ∈ st2 ∧ st[rk] = st2[rk], is_classtype(st1[r1 -- _type] .type) → (∀ fs. fs ' ∈ instfields(st1[r1 -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) → ps=(st[r -- fs '] .refval, st, st1[r1 -- fs '] .refval, st1)) ∧ (∀ fs. fs ' ∈ instfields(st1[r1 -- _type] .type .class) ∧ ¬ is_referencevalue(st[r -- fs ']) → st[r -- fs '] = st1[r1 -- fs ']), is_arraytype(st1[r1 -- _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 ']), ∀ 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, cyclic(str, r1, st1), junkref(str, r1, st1), cyclic(str, r, st), junkref(str, r, st), st2[r -- _type] = st1[r1 -- _type] ∧ ( is_classtype(st2[r -- _type] .type) → ( fs ' ∈ instfields(st2[r -- _type] .type .class) ∧ is_referencevalue(st2[r -- fs ']) → ps=(st2[r -- fs '] .refval, st2, st1[r1 -- fs '] .refval, st1)) ∧ (fs0 ' ∈ instfields(st2[r -- _type] .type .class) ∧ ¬ is_referencevalue(st2[r -- fs0 ']) → st2[r -- fs0 '] = st1[r1 -- fs0 '])) ∧ ( is_arraytype(st2[r -- _type] .type) → st2[r -- _length] .intval = st1[r1 -- _length] .intval ∧ (0 ≤ i ∧ i < st2[r -- _length] .intval ∧ is_referencevalue(st2[r -- i ']) → ps=(st2[r -- i '] .refval, st2, st1[r1 -- i '] .refval, st1)) ∧ (0 ≤ i0 ∧ i0 < st2[r -- _length] .intval ∧ ¬ is_referencevalue(st2[r -- i0 ']) → st2[r -- i0 '] = st1[r1 -- i0 ']))

Rule argument

[EXRARG : pos: left 2, [extquanttermlist: (r -- _type) abort:F , discard:F , computed:T ]]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (r -- _type)]]