[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 193 from proof pseq-sym-01 (previous step)

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

User applied rule case distinction

And obtained the following new goals

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

Rule argument

[CASEDARG : pos: right 7, ()]

Additional information

[[CONCRETESIMPRULES : ()]]