Proof step 46 from proof putarray-add-same (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ r ≠ r0 ∨ r = r0 ∧ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type ∨ r = r0 ∧ is_indexkey(sk) ∧ (sk .index < 0 ∨ n→i(# vals) ≤ sk .index) → (addarray(r, ty, vals, st)[r0 -- sk]) = st[r0 -- sk]

• Proof step 32:

  ¬ (r ≠ r0 ∨ r = r0 ∧ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type ∨ r = r0 ∧ is_indexkey(sk) ∧ (sk .index < 0 ∨ n→i(# vals) ≤ sk .index)) ⊦ (putArray(vals, r, 0, addarray(r, ty, n→i(# vals), st))[r0 -- sk]) = (addarray(r, ty, vals, st)[r0 -- sk])

• Proof step 45:

  r ≠ r0 ∨ r = r0 ∧ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type ∨ r = r0 ∧ is_indexkey(sk) ∧ (sk .index < 0 ∨ n→i(# vals) ≤ sk .index) ⊦ (putArray(vals, r, 0, addarray(r, ty, n→i(# vals), st))[r0 -- sk]) = st[r0 -- sk]

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (sk, r0, st, vals, ty, r)]]