Proof step 46 from proof addarrays-at-other (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ 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 4:

  ¬ (ints ≠ [] ∧ n→i(# refs) = countrefs(ints) ∧ posints(ints)), # refs = i→n(countrefs(ints)), posints(ints), 0 ≤ i ⊦ (addarrays(refs, ty, ints, i, st)[r -- sk]) = st[r -- sk], ints = [], r ∈ refs

• Proof step 45:

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

Rule argument

Additional information

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