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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 195:
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 ' ∈ 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 ']))

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ()]]