Proof step 20 from proof hasSharing-object-rec (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 19:

  st[r -- sk] = refval(r0), st[r -- _type] .type = mkclasstype(class), ∃ sks1, sks2. fits(r0, sks1, st) ∧ fits(r0, sks2, st) ∧ sks1 ≠ sks2 ∧ sks1 ≠ [] ∧ sks2 ≠ [] ∧ st[r0 -- sks1] .refval ≠ jvmref ∧ st[r0 -- sks1] = st[r0 -- sks2], sk ∈ instfields(class) ⊦ r = jvmref, hasSharing(r, st)

Rule argument

Additional information

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