Proof step 15 from proof onlymod-del (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 14:

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

Rule argument

Additional information

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