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

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

User applied rule insert rewrite lemma

And obtained the following new goals

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

Rule argument

[x0lemmaarg: spec-name: instance-name: lemma-name: fits-put-other antecedent: succedent: ¬ (∃ sks0, sks1. sks = sks0 + (sk + sks1) ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks2. sks2 + sk ⊑ sks0 → st[r -- sks2] .refval ≠ r0)) ∧ sk ≠ _type ∧ sk ≠ _length → (fits(r, sks, st[r0 -- sk, val]) ↔ fits(r, sks, st)) substlist: [val, sk, r0, st, sks, r] → [refval(r3), i ', r2, st, sks3, r3] 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 : (refval(r3), i ', r2, st, sks3, r3)]]