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

st[r2 -- _type] = st1[r1 -- _type], st[r2 -- _length] .intval = st1[r1 -- _length] .intval, validrefs(str, st[r2 -- i '] .refval ' + refs + r2 ', st[st[r2 -- i '] .refval -- _type] .type, st), 0 ≤ i, 0 < st1[r1 -- _length] .intval, ps=(st[r2 -- i '] .refval, st, st1[r1 -- i '] .refval, st1), is_arraytype(st1[r1 -- _type] .type), is_array(str, r2, st), is_array(str, r1, st1), i < st1[r1 -- _length] .intval, is_referencevalue(st[r2 -- i ']), validrefs(str, (st[r2 -- i '] .refval ' + refs) + r2 ', st1[r1 -- _type] .type .type, st), ∀ i. ¬ i < 0 ∧ ¬ st1[r1 -- _length] .intval ≤ i ∧ ¬ is_referencevalue(st[r2 -- i ']) → st[r2 -- i '] = st1[r1 -- i '], ∀ st, r, st0, r0, str0. maxpath(str0, r0, st0) < maxpath(str, r1, st1) → (ps=(r, st, r0, st0) ∧ cyclic(str0, r, st) → junkref(str0, r, st) ∨ junkref(str0, r0, st0) ∨ cyclic(str0, r0, st0)) ⊦ r2 = jvmref, r1 = jvmref, r2 = st[r2 -- i '] .refval, cyclic(str, r1, st1), junkref(str, r1, st1), junkref(str, r2, st), dups(refs), st[r2 -- i '] .refval ∈ refs, r2 ∈ refs, validrefs(str, st[r2 -- i '] .refval ' + refs + r2 ' + st[r2 -- i '] .refval ', st[st[r2 -- i '] .refval -- _type] .type, st)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 174:
⊦ validrefs(str, refs + r ', ty, st) ∧ st[r -- i '] .refval = r0 ∧ is_array(str, r, st) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ st[r0 -- _type] .type ≤ st[r -- _type] .type .type ∧ is_valid_ref(str, r0, st) ∧ type∃(str, st[r0 -- _type] .type) → validrefs(str, refs + r ' + r0 ', ty, st)
Proof step 179:
¬ ( validrefs(str, (st[r2 -- i '] .refval ' + refs) + r2 ', st[st[r2 -- i '] .refval -- _type] .type, st) ∧ st[r2 -- i '] .refval = st[r2 -- i '] .refval ∧ is_array(str, r2, st) ∧ 0 ≤ i ∧ i < st[r2 -- _length] .intval ∧ st[st[r2 -- i '] .refval -- _type] .type ≤ st[r2 -- _type] .type .type ∧ is_valid_ref(str, st[r2 -- i '] .refval, st) ∧ type∃(str, st[st[r2 -- i '] .refval -- _type] .type)), st[r2 -- _type] = st1[r1 -- _type], st[r2 -- _length] .intval = st1[r1 -- _length] .intval, validrefs(str, st[r2 -- i '] .refval ' + refs + r2 ', st[st[r2 -- i '] .refval -- _type] .type, st), 0 ≤ i, 0 < st1[r1 -- _length] .intval, ps=(st[r2 -- i '] .refval, st, st1[r1 -- i '] .refval, st1), is_arraytype(st1[r1 -- _type] .type), is_array(str, r2, st), is_array(str, r1, st1), i < st1[r1 -- _length] .intval, is_referencevalue(st[r2 -- i ']), validrefs(str, (st[r2 -- i '] .refval ' + refs) + r2 ', st1[r1 -- _type] .type .type, st), ∀ i. ¬ i < 0 ∧ ¬ st1[r1 -- _length] .intval ≤ i ∧ ¬ is_referencevalue(st[r2 -- i ']) → st[r2 -- i '] = st1[r1 -- i '], ∀ st, r, st0, r0, str0. maxpath(str0, r0, st0) < maxpath(str, r1, st1) → (ps=(r, st, r0, st0) ∧ cyclic(str0, r, st) → junkref(str0, r, st) ∨ junkref(str0, r0, st0) ∨ cyclic(str0, r0, st0)) ⊦ r2 = jvmref, r1 = jvmref, r2 = st[r2 -- i '] .refval, cyclic(str, r1, st1), junkref(str, r1, st1), junkref(str, r2, st), dups(refs), st[r2 -- i '] .refval ∈ refs, r2 ∈ refs, validrefs(str, st[r2 -- i '] .refval ' + refs + r2 ' + st[r2 -- i '] .refval ', st[st[r2 -- i '] .refval -- _type] .type, st)

Rule argument

[speclemmaarg: , validrefs(str, refs + r ', ty, st) ∧ st[r -- i '] .refval = r0 ∧ is_array(str, r, st) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ st[r0 -- _type] .type ≤ st[r -- _type] .type .type ∧ is_valid_ref(str, r0, st) ∧ type∃(str, st[r0 -- _type] .type) → validrefs(str, refs + r ' + r0 ', ty, st) ,[str, refs, r, ty, st, i, r0] → [str, st[r2 -- i '] .refval ' + refs, r2, st[st[r2 -- i '] .refval -- _type] .type, st, i, st[r2 -- i '] .refval] ,F ,cyclic , ,validrefs-applast-array ]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ (refs + refs0) + refs1 = refs + refs0 + refs1])], [EXTRATERMS : (str, st[r2 -- i '] .refval ' + refs, r2, st[st[r2 -- i '] .refval -- _type] .type, st, i, st[r2 -- i '] .refval)]]