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

validreflist(str, mkjavavalues(r ' + r4 '), mkclasstype(`java.lang.Object' .class), st), 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), ∀ r1, sks1, r2, sks2. ¬ ( r1 ∈ r ' + r4 ' ∧ r2 ∈ r ' + r4 ' ∧ r1 ≠ r2 ∧ fits(r1, sks1, st) ∧ fits(r2, sks2, st) ∧ st[r1 -- sks1] = st[r2 -- sks2] ∧ st[r1 -- sks1] .refval ≠ jvmref), 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)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 509:
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), 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, validref(str, r, mkclasstype(`java.lang.Object' .class), st), validref(str, r4, mkclasstype(`java.lang.Object' .class), st), ∀ r2, sks2, r3, sks3. r2 ≠ r ∧ r2 ≠ r4 ∨ r3 ≠ r ∧ r3 ≠ r4 ∨ r2 = r3 ∨ ¬ fits(r2, sks2, st) ∨ ¬ fits(r3, sks3, st) ∨ st[r2 -- sks2] ≠ st[r3 -- sks3] ∨ st[r2 -- sks2] .refval = jvmref ⊦ 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 : list, references, in-17, ⊦ r ∈ r0 ' ↔ r = r0], [CSIMPNAMEDSEQ : list, references, in-06, ⊦ ¬ r ∈ r0 ' + refs ↔ r ≠ r0 ∧ ¬ r ∈ refs], [CSIMPNAMEDSEQ : list, javavalues, a, ⊦ (vals + vals0) + vals1 = vals + vals0 + vals1], [CSIMPNAMEDSEQ : junkrefs, , validreflist-one-01, ⊦ validreflist (str, refval(r) ', ty, st) ↔ validref(str, r, ty, st)], [CSIMPNAMEDSEQ : junkrefs, , validreflist-rec-01, ⊦ validreflist (str, refval(r) ' + vals, ty, st) ↔ validref(str, r, ty, st) ∧ validreflist (str, vals, ty, st)], [CSIMPNAMEDSEQ : list, references, a, ⊦ (refs + refs0) + refs1 = refs + refs0 + refs1], [CSIMPNAMEDSEQ : valuesfuns, , mkvalsr-one, ⊦ mkjavavalues(r ') = refval(r) '], [CSIMPNAMEDSEQ : valuesfuns, , mkvalsr-rec, ⊦ mkjavavalues(r ' + refs) = refval(r) ' + mkjavavalues(refs)])]]