Proof step 50 from proof addarrays-at-other-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 6:

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

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

• Proof step 49:

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

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, i, ints, ty, newref_list(i→n(countrefs(ints)), st))]]