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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 110:

  ⊦ 0 ≤ i ∧ i < n→i(# vals) → (addarray(r, ty, vals, st)[r -- i ']) = vals[i→n(i)]

• Proof step 116:

  ¬ (0 ≤ i ∧ i < n→i(# (val ' + mklist(initial_value(ty), i→n(i0))))), 0 ≤ i0 ⊦ (addarray(r, ty, 1 + i0, st)[r -- i ']) = (addarray(r, ty, val ' + mklist(initial_value(ty), i→n(i0)), st)[r -- i ']), i = 0

• Proof step 133:

  0 ≤ i ∧ i < n→i(# (val ' + mklist(initial_value(ty), i→n(i0)))), 0 ≤ i0 ⊦ (addarray(r, ty, 1 + i0, st)[r -- i ']) = (val ' + mklist(initial_value(ty), i→n(i0)))[i→n(i)], i = 0

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (i, st, val ' + mklist(initial_value(ty), i→n(i0)), ty, r)]]