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

¬ ( cyclic(str, st1[r1 -- i '] .refval, st1) ∧ is_array(str, r1, st1) ∧ st1[r1 -- i '] = refval(st1[r1 -- i '] .refval) ∧ 0 ≤ i ∧ i < st1[r1 -- _length] .intval ∧ is_reftype(st1[r1 -- _type] .type .type) ∧ st1[st1[r1 -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type), 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, 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)) ⊦ r = jvmref, r1 = jvmref, junkref(str, r, st), cyclic(str, r, st), junkref(str, r1, st1), 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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 162:
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, 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)) ⊦ r = jvmref, r1 = jvmref, junkref(str, r, st), cyclic(str, r, st), junkref(str, r1, st1), 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, cyclic(str, st1[r1 -- i '] .refval, st1) ∧ st1[r1 -- i '] = refval(st1[r1 -- i '] .refval) ∧ is_reftype(st1[r1 -- _type] .type .type) ∧ st1[st1[r1 -- i '] .refval -- _type] .type ≤ st1[r1 -- _type] .type .type

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ i < j → (¬ ¬ j ≤ i ↔ false)], [CSIMPSEQ : ⊦ ¬ i < j ↔ j ≤ i], [CSIMPSEQ : ⊦ i ≤ j → (¬ ¬ j < i ↔ false)], [CSIMPSEQ : ⊦ ¬ i ≤ j ↔ j < i])]]