| st[r -- sks1] = refval(r0), (st[r0 -- i ', refval(r3)][r3 -- (sks + i ' ' + sks0)]) = refval(r1), st[r0 -- _type] .type = mkarraytype(ty), st[r3 -- sks2] = refval(r1), st[r3 -- sks] = refval(r0), (st[r0 -- i ', refval(r3)][r3 -- sks]) = refval(r2), 0 < st[r0 -- _length] .intval, is_referencevalue(st[r0 -- i ', refval(r3)][r0 -- (i ' ' + sks2)]), fits(r3, sks2, st), is_referencevalue(st[r0 -- i ', refval(r3)][r0 -- (i ' ' + sks + i ' ' + sks0)]), 0 ≤ i, i < st[r0 -- _length] .intval, fits(r3, sks, st), fits(r2, i ' ' + sks0, st[r0 -- i ', refval(r3)]), fits(r, sks1, st), validref(str, r3, ty, st), validref(str, r, mkclasstype(`java.lang.Object' .class), st), validref(str, r3, mkclasstype(`java.lang.Object' .class), st), ∀ r4, sks3, r5, sks4. r4 ≠ r ∧ r4 ≠ r3 ∨ r5 ≠ r ∧ r5 ≠ r3 ∨ r4 = r5 ∨ ¬ fits(r4, sks3, st) ∨ ¬ fits(r5, sks4, st) ∨ st[r4 -- sks3] ≠ st[r5 -- sks4] ∨ st[r4 -- sks3] .refval = jvmref ⊦ r3 = jvmref, sks1 = [], r0 = jvmref, r = r3, r1 = jvmref, sks2 = sks + i ' ' + sks0, junkref(str, r, st), hasSharing(r3, st), hasSharing(r, st), ∃ sks0, sks4. sks1 = sks0 + i ' ' + sks4 ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks5. sks5 + i ' ' ⊑ sks0 → st[r -- sks5] .refval ≠ st[r -- sks0] .refval), ∃ sks4. ¬ (sks4 + i ' ' ⊑ sks1 → st[r -- sks4] .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), ∃ sks2. ¬ (sks2 + i ' ' ⊑ sks1 → st[r -- sks2] .refval ≠ r0), ∃ sks1, sks0. sks2 = sks1 + i ' ' + sks0 ∧ st[r3 -- sks1] .refval = r0 ∧ (∀ sks4. sks4 + i ' ' ⊑ sks1 → st[r3 -- sks4] .refval ≠ st[r3 -- sks1] .refval), ∃ sks4. ¬ (sks4 + i ' ' ⊑ sks → st[r3 -- sks4] .refval ≠ r0), ∃ sks3, sks4. sks = sks3 + i ' ' + sks4 ∧ st[r3 -- sks3] .refval = r0 ∧ (∀ sks5. sks5 + i ' ' ⊑ sks3 → st[r3 -- sks5] .refval ≠ st[r3 -- sks3] .refval) |
[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : javavalue, , sel-09, ⊦ refval(r) .refval = r])], [EXTRATERMS : (r, sks1, r3, sks)]]