Proof step 30 from proof endfinallymode (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ ints ≠ [] ∧ n→i(# refs) = countrefs(ints) ∧ posints(ints) → addarrays(refs, ty, ints, i, st) = addmultiarrays(refs, ints .first, [], mktype_from_dims(ty, countdims(ints, i)), getdims(ints), st)

• Proof step 29:

  ints ≠ [] ∧ n→i(# refs) = countrefs(ints) ∧ posints(ints), n→i(# refs) = countrefs(ints), posints(ints) ⊦ ints = [], (addmultiarrays(refs, ints .first, [], mktype_from_dims(ty, countdims(ints, i)), getdims(ints), st)[_endfinallymode]) = st[_endfinallymode]

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, i, ints, ty, refs)]]