Proof step 10 from proof onlymod-put (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 9:

  onlyModified(r, st, st0), r -- sk ∈ st, r ∈ st ⊦ sk = _length, sk = _type, (∀ 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]))

Rule argument

Additional information

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