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

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

User applied rule insert rewrite lemma

And obtained the following new goals

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

Rule argument

[x0lemmaarg: spec-name: storefuns instance-name: lemma-name: lookup-put-other antecedent: succedent: ¬ (∃ sks0, sks1. sks = sks0 + (sk + sks1) ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks2. sks2 + sk ⊑ sks0 → st[r -- sks2] .refval ≠ r0)) → (st[r0 -- sk, val][r -- sks]) = st[r -- sks] substlist: [sks, r, val, sk, r0, st] → [sks0, r2, refval(r2), i ', r0, st] add preconditions?: F is rewrite lemma?: T current spec?: F rotate lemma?: F replace all?: T paths: ((0, 0, 0, 1, 0)) dummy: () ]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (sks0, r2, refval(r2), i ', r0, st)]]