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

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

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 722:
⊦ validreflist(str, mkjavavalues(refs), mkclasstype(`java.lang.Object' .class), st) → ( disjoint(str, refs, st) ↔ ¬ (∃ r1, sks1, r2, sks2. r1 ∈ refs ∧ r2 ∈ refs ∧ r1 ≠ r2 ∧ fits(r1, sks1, st) ∧ fits(r2, sks2, st) ∧ st[r1 -- sks1] = st[r2 -- sks2] ∧ st[r1 -- sks1] .refval ≠ jvmref))
Proof step 729:
¬ validreflist(str, mkjavavalues(r ' + r4 '), mkclasstype(`java.lang.Object' .class), st), st[r3 -- _type] .type = mkarraytype(ty), st[r -- sks] = refval(r1), st[r -- sks1] = refval(r3), (st[r3 -- i ', refval(r4)][r4 -- (sks0 + i ' ' + sks3)]) = refval(r1), st[r4 -- sks0] = refval(r3), 0 < st[r3 -- _length] .intval, 0 ≤ i, i < st[r3 -- _length] .intval, validref(str, r4, ty, st), disjoint(str, r ' + r4 ', st), fits(r, sks, st), fits(r, sks1, st), fits(r4, sks0, st), fits(r4, sks3, st[r3 -- i ', refval(r4)]) ⊦ sks1 = [], sks1 + i ' ' + sks0 + i ' ' + sks3 = sks, sks = [], r1 = jvmref, r = r4, r3 = jvmref, r4 = jvmref, hasSharing(r, st), hasSharing(r4, st), junkref(str, r, st), ∃ sks1, sks3. sks = sks1 + i ' ' + sks3 ∧ st[r -- sks1] .refval = r3 ∧ (∀ sks2. sks2 + i ' ' ⊑ sks1 → st[r -- sks2] .refval ≠ st[r -- sks1] .refval), ∃ sks3. ¬ (sks3 + i ' ' ⊑ sks1 → st[r -- sks3] .refval ≠ r3), ∃ sks, sks3. sks1 = sks + i ' ' + sks3 ∧ st[r -- sks] .refval = r3 ∧ (∀ sks4. sks4 + i ' ' ⊑ sks → st[r -- sks4] .refval ≠ st[r -- sks] .refval), ∃ sks4. ¬ (sks4 + i ' ' ⊑ sks0 → st[r4 -- sks4] .refval ≠ r3), ∃ sks2, sks4. sks0 = sks2 + i ' ' + sks4 ∧ st[r4 -- sks2] .refval = r3 ∧ (∀ sks5. sks5 + i ' ' ⊑ sks2 → st[r4 -- sks5] .refval ≠ st[r4 -- sks2] .refval)
Proof step 731:
validreflist(str, mkjavavalues(r ' + r4 '), mkclasstype(`java.lang.Object' .class), st), st[r3 -- _type] .type = mkarraytype(ty), st[r -- sks] = refval(r1), st[r -- sks1] = refval(r3), (st[r3 -- i ', refval(r4)][r4 -- (sks0 + i ' ' + sks3)]) = refval(r1), st[r4 -- sks0] = refval(r3), 0 < st[r3 -- _length] .intval, 0 ≤ i, i < st[r3 -- _length] .intval, validref(str, r4, ty, 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), fits(r, sks, st), fits(r, sks1, st), fits(r4, sks0, st), fits(r4, sks3, st[r3 -- i ', refval(r4)]) ⊦ sks1 = [], sks1 + i ' ' + sks0 + i ' ' + sks3 = sks, sks = [], r1 = jvmref, r = r4, r3 = jvmref, r4 = jvmref, hasSharing(r, st), hasSharing(r4, st), junkref(str, r, st), ∃ sks1, sks3. sks = sks1 + i ' ' + sks3 ∧ st[r -- sks1] .refval = r3 ∧ (∀ sks2. sks2 + i ' ' ⊑ sks1 → st[r -- sks2] .refval ≠ st[r -- sks1] .refval), ∃ sks3. ¬ (sks3 + i ' ' ⊑ sks1 → st[r -- sks3] .refval ≠ r3), ∃ sks, sks3. sks1 = sks + i ' ' + sks3 ∧ st[r -- sks] .refval = r3 ∧ (∀ sks4. sks4 + i ' ' ⊑ sks → st[r -- sks4] .refval ≠ st[r -- sks] .refval), ∃ sks4. ¬ (sks4 + i ' ' ⊑ sks0 → st[r4 -- sks4] .refval ≠ r3), ∃ sks2, sks4. sks0 = sks2 + i ' ' + sks4 ∧ st[r4 -- sks2] .refval = r3 ∧ (∀ sks5. sks5 + i ' ' ⊑ sks2 → st[r4 -- sks5] .refval ≠ st[r4 -- sks2] .refval)

Rule argument

[x0lemmaarg: spec-name: instance-name: lemma-name: disjoint-def-fits antecedent: succedent: validreflist (str, mkjavavalues(refs), mkclasstype(`java.lang.Object' .class), st) → ( disjoint(str, refs, st) ↔ ¬ (∃ r1, sks1, r2, sks2. r1 ∈ refs ∧ r2 ∈ refs ∧ r1 ≠ r2 ∧ fits(r1, sks1, st) ∧ fits(r2, sks2, st) ∧ st[r1 -- sks1] = st[r2 -- sks2] ∧ st[r1 -- sks1] .refval ≠ jvmref)) substlist: [st, refs, str] → [st, r ' + r4 ', str] add preconditions?: F is rewrite lemma?: T current spec?: T rotate lemma?: F replace all?: T paths: ((0, 0, 9)) dummy: () ]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, r ' + r4 ', str)]]