Proof step 8 from proof add-refs (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ vals ≠ [] → addarray(r, ty, vals, st) = (addarray(r, ty, vals .butlast, st)[r -- n→i((# vals) -1) ', vals .last][r -- _length, intval(n→i(# vals))])

• Proof step 5:

  ¬ vals ≠ [], ∀ st, ty, r, vals0. # vals0 < # vals → (true → addarray(r, ty, vals0, st) .refs = st .refs ++ r) ⊦ addarray(r, ty, vals, st) .refs = st .refs ++ r

• Proof step 7:

  vals ≠ [], ∀ st, ty, r, vals0. # vals0 < # vals → (true → addarray(r, ty, vals0, st) .refs = st .refs ++ r) ⊦ (addarray(r, ty, vals .butlast, st)[r -- n→i((# vals) -1) ', vals .last][r -- _length, intval(n→i(# vals))]) .refs = st .refs ++ r

Rule argument

Additional information

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