Proof step 16 from proof onlymod-put-01 (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 15:

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

Rule argument

Additional information

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