| st[r -- sks0] = refval(r1), st[r0 -- _type] .type = mkarraytype(ty), (st[r0 -- i ', refval(r4)][r4 -- ((sks3 + i ' ' + sks5) + i ' ' + sks4)]) = refval(r1), st[r -- sks1] = refval(r0), st[r4 -- (sks3 + i ' ' + sks5)] = refval(r0), (st[r0 -- i ', refval(r4)][r4 -- (sks3 + i ' ' + sks5)]) = refval(r2), st[r4 -- sks3] = refval(r0), 0 < st[r0 -- _length] .intval, is_referencevalue(st[r0 -- i ', refval(r4)][r0 -- (i ' ' + (sks3 + i ' ' + sks5) + i ' ' + sks4)]), fits(r, sks0, st), validref(str, r4, ty, st), disjoint(str, r ' + r4 ', st), fits(r, sks1, st), fits(r4, sks3 + i ' ' + sks5, st[r0 -- i ', refval(r4)]), fits(r2, i ' ' + sks4, st[r0 -- i ', refval(r4)]), i < st[r0 -- _length] .intval, 0 ≤ i ⊦ r4 = jvmref, sks1 = [], sks0 = sks1 + i ' ' + (sks3 + i ' ' + sks5) + i ' ' + sks4, sks0 = [], r1 = jvmref, r = r4, r0 = jvmref, hasSharing(r, st), hasSharing(r4, st), junkref(str, r, st), ∃ 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), ∃ sks1, sks2. sks0 = sks1 + i ' ' + sks2 ∧ st[r -- sks1] .refval = r0 ∧ (∀ sks4. sks4 + i ' ' ⊑ sks1 → st[r -- sks4] .refval ≠ st[r -- sks1] .refval), ∃ sks2. ¬ (sks2 + i ' ' ⊑ sks3 + i ' ' + sks5 → st[r4 -- sks2] .refval ≠ r0), ∃ sks2. ¬ (sks2 + i ' ' ⊑ sks3 → st[r4 -- sks2] .refval ≠ r0) |
[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : list-last, storekeys, app-01-02, ⊦ sks + sks0 ⊑ sks + sks1 ↔ sks0 ⊑ sks1], [CSIMPNAMEDSEQ : list-last, storekeys, prefix-one, ⊦ sk ' ⊑ sk0 ' + sks ↔ sk = sk0], [CSIMPNAMEDSEQ : list, storekeys, a, ⊦ (sks + sks0) + sks1 = sks + sks0 + sks1], [CSIMPNAMEDSEQ : javavalue, , sel-09, ⊦ refval(r) .refval = r])], [EXTRATERMS : (sks3)]]