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

i ' ' + sks4 ≠ [], st[r4 -- sks] = refval(r0), st[r -- sks0] = refval(r1), st[r0 -- _type] .type = mkarraytype(ty), (st[r0 -- i ', refval(r4)][r4 -- (sks + i ' ' + sks4)]) = refval(r1), st[r -- sks1] = refval(r0), 0 < st[r0 -- _length] .intval, is_referencevalue(st[r0 -- i ', refval(r4)][r0 -- (i ' ' + sks + i ' ' + sks4)]), fits(r, sks0, st), validref(str, r4, ty, st), disjoint(str, r ' + r4 ', st), fits(r, sks1, st), fits(r4, sks, st), r0 ≠ jvmref ∧ is_referencevalue(st[r0 -- i ', refval(r4)][r0 -- (i ' ' + sks4) .first]) ∧ ( is_classtype((st[r0 -- i ', refval(r4)][r0 -- _type]) .type) → (i ' ' + sks4) .first ∈ instfields((st[r0 -- i ', refval(r4)][r0 -- _type]) .type .class)) ∧ ( is_arraytype((st[r0 -- i ', refval(r4)][r0 -- _type]) .type) → is_indexkey((i ' ' + sks4) .first) ∧ 0 ≤ (i ' ' + sks4) .first .index ∧ (i ' ' + sks4) .first .index < (st[r0 -- i ', refval(r4)][r0 -- _length]) .intval) ∧ fits((st[r0 -- i ', refval(r4)][r0 -- (i ' ' + sks4) .first]) .refval, (i ' ' + sks4) .rest, st[r0 -- i ', refval(r4)]), i < st[r0 -- _length] .intval, 0 ≤ i ⊦ r4 = jvmref, sks1 = [], sks0 = sks1 + i ' ' + sks + 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 ' ' ⊑ sks → st[r4 -- sks2] .refval ≠ r0), ∃ sks3, sks5. sks = sks3 + i ' ' + sks5 ∧ st[r4 -- sks3] .refval = r0 ∧ (∀ sks2. sks2 + i ' ' ⊑ sks3 → st[r4 -- sks2] .refval ≠ st[r4 -- sks3] .refval)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 511:
st[r -- sks1] = refval(r0), (st[r0 -- i ', refval(r4)][r4 -- (sks + i ' ' + sks4)]) = refval(r1), st[r0 -- _type] .type = mkarraytype(ty), st[r -- sks0] = refval(r1), st[r4 -- sks] = refval(r0), fits(r4, sks4, st[r0 -- i ', refval(r4)]), fits(r4, sks, st), fits(r, sks1, st), disjoint(str, r ' + r4 ', st), validref(str, r4, ty, st), fits(r, sks0, st), is_referencevalue(st[r0 -- i ', refval(r4)][r0 -- (i ' ' + sks + i ' ' + sks4)]), 0 < st[r0 -- _length] .intval, 0 ≤ i, i < st[r0 -- _length] .intval ⊦ r0 = jvmref, r = r4, r1 = jvmref, sks0 = [], sks0 = sks1 + i ' ' + sks + i ' ' + sks4, sks1 = [], r4 = jvmref, junkref(str, r, st), hasSharing(r4, st), hasSharing(r, st), ∃ sks3, sks5. sks = sks3 + i ' ' + sks5 ∧ st[r4 -- sks3] .refval = r0 ∧ (∀ sks2. sks2 + i ' ' ⊑ sks3 → st[r4 -- sks2] .refval ≠ st[r4 -- sks3] .refval), ∃ sks2. ¬ (sks2 + i ' ' ⊑ sks → st[r4 -- sks2] .refval ≠ r0), ∃ sks1, sks2. sks0 = sks1 + i ' ' + sks2 ∧ st[r -- sks1] .refval = r0 ∧ (∀ sks4. sks4 + i ' ' ⊑ sks1 → st[r -- sks4] .refval ≠ st[r -- sks1] .refval), ∃ 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)

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : javatype, , test-16, ⊦ ¬ is_classtype (mkarraytype(ty))], [CSIMPNAMEDSEQ : javastore, , length-at, ⊦ (st[r -- i ', val] [r0 -- _length ] ) = st[r0 -- _length]], [CSIMPNAMEDSEQ : int-abs, , zero-gels-04, ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j], [CSIMPNAMEDSEQ : storekey, , sel-06, ⊦ i ' .index = i], [CSIMPNAMEDSEQ : storekey, , test-08, ⊦ is_indexkey(i ')], [CSIMPNAMEDSEQ : addfuns, , instfields-index, ⊦ ¬ i ' ∈ instfields(class)], [CSIMPNAMEDSEQ : javastore, , type-at, ⊦ (st[r -- i ', val] [r0 -- _type ] ) = st[r0 -- _type]], [CSIMPNAMEDSEQ : list, storekeys, c-07, ⊦ (sk ' + sks) .rest = sks], [CSIMPNAMEDSEQ : javavalue, , sel-09, ⊦ refval(r) .refval = r], [CSIMPNAMEDSEQ : javavalue, , test-19, ⊦ is_referencevalue(refval(r))], [CSIMPNAMEDSEQ : store, javastore, At-same, ⊦ (st[rk, val][rk]) = val], [CSIMPNAMEDSEQ : list, storekeys, c-08, ⊦ (sk ' + sks) .first = sk], [CSIMPNAMEDSEQ : list, storekeys, a, ⊦ (sks + sks0) + sks1 = sks + sks0 + sks1], [CSIMPNAMEDSEQ : list, storekeys, e-01, ⊦ sk ' + sks ≠ []])]]