Proof step 23 from proof addarrays-refin-01 (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 22:

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

Rule argument

Additional information

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