Proof step 41 from proof hasSharing-putbar (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ hasSharing(r, st) ↔ (∃ sks1, sks2. fits(r, sks1, st) ∧ fits(r, sks2, st) ∧ sks1 ≠ sks2 ∧ sks1 ≠ [] ∧ sks2 ≠ [] ∧ st[r -- sks1] .refval ≠ jvmref ∧ st[r -- sks1] = st[r -- sks2])

• Proof step 40:

  okbytearray(r0, st), hasSharing(r, putByteArray(bytes, r0, i, st)) ⊦ junkref(str, r, st), ∃ sks1, sks2. fits(r, sks1, st) ∧ fits(r, sks2, st) ∧ sks1 ≠ sks2 ∧ sks1 ≠ [] ∧ sks2 ≠ [] ∧ st[r -- sks1] .refval ≠ jvmref ∧ st[r -- sks1] = st[r -- sks2]

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, r)]]