[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 360 from proof hasSharing-put-index-refval (previous step)

¬ ¬ (∃ sks0, sks1. sks = sks0 + (i ' + sks1) ∧ st[r3 -- sks0] .refval = r0 ∧ (∀ sks2. sks2 + i ' ⊑ sks0 → st[r3 -- sks2] .refval ≠ r0)), (st[r0 -- i ', refval(r3)][r3 -- sks]) = refval(r2), st[r3 -- sks] = refval(r0), (st[r0 -- i ', refval(r3)][r3 -- (sks + i ' ' + sks0)]) = refval(r1), st[r0 -- _type] .type = mkarraytype(ty), (st[r0 -- i ', refval(r3)][r3 -- sks3]) = refval(r1), st[r -- sks1] = refval(r0), (st[r0 -- i ', refval(r3)][r2 -- i ']) = refval(r4), fits(r4, sks0, st[r0 -- i ', refval(r3)]), fits(r3, sks, st), is_referencevalue(st[r0 -- i ', refval(r3)][r0 -- (i ' ' + sks + i ' ' + sks0)]), 0 < st[r0 -- _length] .intval, validref(str, r3, ty, st), disjoint(str, r ' + r3 ', st), fits(r, sks1, st), fits(r3, sks3, st[r0 -- i ', refval(r3)]), i < st[r0 -- _length] .intval, 0 ≤ i, is_referencevalue(st[r0 -- i ', refval(r3)][r0 -- (i ' ' + sks3)]), is_arraytype(st[r2 -- _type] .type) → i < st[r2 -- _length] .intval ⊦ r2 = jvmref, sks + i ' ' + sks0 = sks3, r1 = jvmref, r = r3, r0 = jvmref, sks1 = [], r3 = jvmref, is_classtype(st[r2 -- _type] .type), hasSharing(r, st), hasSharing(r3, st), junkref(str, r, st), ∃ sks4, sks5. sks = sks4 + i ' ' + sks5 ∧ st[r3 -- sks4] .refval = r0 ∧ (∀ sks2. sks2 + i ' ' ⊑ sks4 → st[r3 -- sks2] .refval ≠ st[r3 -- sks4] .refval), ∃ sks4. ¬ (sks4 + i ' ' ⊑ sks → st[r3 -- sks4] .refval ≠ r0), ∃ sks2. ¬ (sks2 + i ' ' ⊑ sks1 → st[r -- sks2] .refval ≠ r0), ∃ sks0, sks2. sks1 = sks0 + i ' ' + sks2 ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks4. sks4 + i ' ' ⊑ sks0 → st[r -- sks4] .refval ≠ st[r -- sks0] .refval), ∃ sks4. ¬ (sks4 + i ' ' ⊑ sks1 → st[r -- sks4] .refval ≠ r0), ∃ sks0, sks4. sks1 = sks0 + i ' ' + sks4 ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks5. sks5 + i ' ' ⊑ sks0 → st[r -- sks5] .refval ≠ st[r -- sks0] .refval)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 359:
st[st[r3 -- sks4] .refval -- _type] .type = mkarraytype(ty), (st[st[r3 -- sks4] .refval -- i ', refval(r3)][r3 -- sks3]) = refval(r1), st[r -- sks1] = refval(st[r3 -- sks4] .refval), (st[st[r3 -- sks4] .refval -- i ', refval(r3)][r2 -- i ']) = refval(r4), (st[st[r3 -- sks4] .refval -- i ', refval(r3)][r3 -- (sks4 + i ' ' + sks2)]) = refval(r2), st[r3 -- (sks4 + i ' ' + sks2)] = refval(st[r3 -- sks4] .refval), (st[st[r3 -- sks4] .refval -- i ', refval(r3)][r3 -- (sks4 + (i ' ' + sks2) + i ' ' + sks0)]) = refval(r1), validref(str, r3, ty, st), disjoint(str, r ' + r3 ', st), fits(r, sks1, st), fits(r3, sks3, st[st[r3 -- sks4] .refval -- i ', refval(r3)]), i < st[st[r3 -- sks4] .refval -- _length] .intval, 0 ≤ i, is_referencevalue(st[st[r3 -- sks4] .refval -- i ', refval(r3)][st[r3 -- sks4] .refval -- (i ' ' + sks3)]), fits(r4, sks0, st[st[r3 -- sks4] .refval -- i ', refval(r3)]), fits(r3, sks4 + i ' ' + sks2, st), is_referencevalue(st[st[r3 -- sks4] .refval -- i ', refval(r3)][st[r3 -- sks4] .refval -- (i ' ' + sks4 + (i ' ' + sks2) + i ' ' + sks0)]), 0 < st[st[r3 -- sks4] .refval -- _length] .intval, is_arraytype(st[r2 -- _type] .type) → i < st[r2 -- _length] .intval, ∀ sks. sks + i ' ' ⊑ sks4 → st[r3 -- sks] .refval ≠ st[r3 -- sks4] .refval ⊦ r1 = jvmref, r = r3, st[r3 -- sks4] .refval = jvmref, sks1 = [], r3 = jvmref, r2 = jvmref, sks4 + (i ' ' + sks2) + i ' ' + sks0 = sks3, is_classtype(st[r2 -- _type] .type), hasSharing(r, st), hasSharing(r3, st), junkref(str, r, st), ∃ sks2. ¬ (sks2 + i ' ' ⊑ sks1 → st[r -- sks2] .refval ≠ st[r3 -- sks4] .refval), ∃ sks0, sks2. sks1 = sks0 + i ' ' + sks2 ∧ st[r -- sks0] .refval = st[r3 -- sks4] .refval ∧ (∀ sks4. sks4 + i ' ' ⊑ sks0 → st[r -- sks4] .refval ≠ st[r -- sks0] .refval), ∃ sks. ¬ (sks + i ' ' ⊑ sks1 → st[r -- sks] .refval ≠ st[r3 -- sks4] .refval), ∃ sks0, sks. sks1 = sks0 + i ' ' + sks ∧ st[r -- sks0] .refval = st[r3 -- sks4] .refval ∧ (∀ sks5. sks5 + i ' ' ⊑ sks0 → st[r -- sks5] .refval ≠ st[r -- sks0] .refval), ∃ sks, sks5. sks4 + i ' ' + sks2 = sks + i ' ' + sks5 ∧ st[r3 -- sks] .refval = st[r3 -- sks4] .refval ∧ (∀ sks2. sks2 + i ' ' ⊑ sks → st[r3 -- sks2] .refval ≠ st[r3 -- sks] .refval), ∃ sks. ¬ (sks + i ' ' ⊑ sks4 + i ' ' + sks2 → st[r3 -- sks] .refval ≠ st[r3 -- sks4] .refval)

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDFORWARD : int-abs, , forward-lels, ⊦ i ≤ j ∧ j < j0 → i < j0], [CSIMPNAMEDSEQ : list, storekeys, Last, ⊦ sks + sk = sks + sk '], [CSIMPNAMEDSEQ : list, storekeys, a, ⊦ (sks + sks0) + sks1 = sks + sks0 + sks1], [CSIMPNAMEDSEQ : list, storekeys, c, ⊦ sk + sks = sk ' + sks])]]