[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 151 from proof pseq-subset (previous step)

st2[r -- i '] = st[r -- i '], st[r -- _type] = st1[r1 -- _type], st2[r -- _type] = st1[r1 -- _type], st[r -- _length] .intval = st1[r1 -- _length] .intval, st2[r -- _length] .intval = st1[r1 -- _length] .intval, is_referencevalue(st1[r1 -- i ']), r -- i ' ∈ st2, r -- i ' ∈ st, ps=(st[r -- i '] .refval, st, st1[r1 -- i '] .refval, st1), 0 < st1[r1 -- _length] .intval, 0 ≤ i, is_arraytype(st1[r1 -- _type] .type), r ∈ st2, r ∈ st, r -- _type ∈ st2, r -- _type ∈ st, is_array(str, r1, st1), is_array(str, r, st), is_referencevalue(st[r -- i ']), i < st1[r1 -- _length] .intval, junkref(str, st[r -- i '] .refval, st) ∨ cyclic(str, st[r -- i '] .refval, st) ∨ junkref(str, st1[r1 -- i '] .refval, st1) ∨ cyclic(str, st1[r1 -- i '] .refval, st1), ∀ i. ¬ i < 0 ∧ ¬ st1[r1 -- _length] .intval ≤ i ∧ is_referencevalue(st[r -- i ']) → ps=(st[r -- i '] .refval, st, st1[r1 -- i '] .refval, st1), ∀ i. ¬ i < 0 ∧ ¬ st1[r1 -- _length] .intval ≤ i ∧ ¬ is_referencevalue(st[r -- i ']) → st[r -- i '] = st1[r1 -- i '], ∀ rk. rk ∈ st → rk ∈ st2 ∧ st[rk] = st2[rk], ∀ 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)) ⊦ st1[r1 -- i '] .refval ≠ jvmref, r = jvmref, r1 = jvmref, cyclic(str, r, st), cyclic(str, r1, st1), ps=(st[r -- i '] .refval, st2, st1[r1 -- i '] .refval, st1), cyclic(str, st[r -- i '] .refval, st) ∧ is_reftype(st1[r1 -- _type] .type .type) ∧ st[st[r -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type, st[r -- i '] .refval ≠ jvmref ∧ (¬ st[st[r -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type ∨ junkref(str, st[r -- i '] .refval, st)), cyclic(str, st1[r1 -- i '] .refval, st1) ∧ is_reftype(st1[r1 -- _type] .type .type) ∧ st1[st1[r1 -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type, st1[r1 -- i '] .refval ≠ jvmref ∧ (¬ st1[st1[r1 -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type ∨ junkref(str, st1[r1 -- i '] .refval, st1))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 150:
st2[r -- _length] .intval = st1[r1 -- _length] .intval, st[r -- _length] .intval = st1[r1 -- _length] .intval, st2[r -- _type] = st1[r1 -- _type], st[r -- _type] = st1[r1 -- _type], st2[r -- i '] = st[r -- i '], st1[r1 -- i '] .refval = jvmref, i < st1[r1 -- _length] .intval, is_referencevalue(st[r -- i ']), is_array(str, r, st), is_array(str, r1, st1), r -- _type ∈ st, r -- _type ∈ st2, r ∈ st, r ∈ st2, is_arraytype(st1[r1 -- _type] .type), 0 ≤ i, 0 < st1[r1 -- _length] .intval, ps=(st[r -- i '] .refval, st, jvmref, st1), r -- i ' ∈ st, r -- i ' ∈ st2, is_referencevalue(st1[r1 -- i ']), ∀ rk. rk ∈ st → rk ∈ st2 ∧ st[rk] = st2[rk], ∀ i. ¬ i < 0 ∧ ¬ st1[r1 -- _length] .intval ≤ i ∧ ¬ is_referencevalue(st[r -- i ']) → st[r -- i '] = st1[r1 -- i '], ∀ i. ¬ i < 0 ∧ ¬ st1[r1 -- _length] .intval ≤ i ∧ is_referencevalue(st[r -- i ']) → ps=(st[r -- i '] .refval, st, st1[r1 -- i '] .refval, st1), junkref(str, st[r -- i '] .refval, st) ∨ cyclic(str, st[r -- i '] .refval, st), ∀ 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, ps=(st[r -- i '] .refval, st2, jvmref, st1), cyclic(str, r1, st1), cyclic(str, r, st), st[r -- i '] .refval ≠ jvmref ∧ (¬ st[st[r -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type ∨ junkref(str, st[r -- i '] .refval, st)), cyclic(str, st[r -- i '] .refval, st) ∧ is_reftype(st1[r1 -- _type] .type .type) ∧ st[st[r -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ ¬ cyclic(str, jvmref, st)], [CSIMPSEQ : ⊦ ¬ junkref(str, jvmref, st)])]]