Proof step 46 from proof hasSharing-put-statfield (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 45:

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

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[jvmref -- sk, val], r)]]