Proof step 4 from proof onlymod-other (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ onlyModified(r, st1, st2) ↔ (∀ rk. rk ∈ st1 ↔ rk ∈ st2) ∧ (∀ r0, sk. r0 ≠ r → st1[r0 -- sk] = st2[r0 -- sk]) ∧ (r -- _type ∈ st1 → st1[r -- _type] = st2[r -- _type]) ∧ (r -- _length ∈ st1 → st1[r -- _length] = st2[r -- _length])

• Proof step 3:

  (∀ rk. rk ∈ st ↔ rk ∈ st0) ∧ (∀ r0, sk. r0 ≠ r → st[r0 -- sk] = st0[r0 -- sk]) ∧ (r -- _type ∈ st → st[r -- _type] = st0[r -- _type]) ∧ (r -- _length ∈ st → st[r -- _length] = st0[r -- _length]) ⊦ r = r0, st[r0 -- sk] = st0[r0 -- sk]

Rule argument

Additional information

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