Proof step 141 from proof addarray-put-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 104:

  ⊦ is_fskey(sk) ∧ sk ≠ _type ∧ sk ≠ _length → (addarray(r, ty, i, st)[r0 -- sk]) = st[r0 -- sk]

• Proof step 137:

  ¬ (is_fskey(sk) ∧ sk ≠ _type ∧ sk ≠ _length), 0 ≤ i0 ⊦ sk = 0 ', (addarray(r, ty, 1 + i0, st)[r -- sk]) = (addarray(r, ty, val ' + mklist(initial_value(ty), i→n(i0)), st)[r -- sk])

• Proof step 140:

  is_fskey(sk) ∧ sk ≠ _type ∧ sk ≠ _length, 0 ≤ i0 ⊦ sk = 0 ', st[r -- sk] = (addarray(r, ty, val ' + mklist(initial_value(ty), i→n(i0)), st)[r -- sk])

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (sk, r, st, 1 + i0, ty, r)]]