Proof step 14 from proof exactarray-copy (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ exactarray(r, ty, st) ↔ exactreftype(refval(r), mkarraytype(ty), st) ∧ r ≠ jvmref ∧ r -- _length ∈ st ∧ is_integervalue(st[r -- _length]) ∧ 0 ≤ st[r -- _length] .intval ∧ is_arrayref(r, st[r -- _length] .intval, st)

• Proof step 13:

  ⊦ r1 = r0, exactreftype(refval(r1), mkarraytype(ty), arraycopy(r, i, r0, i0, j, st)) ∧ r1 ≠ jvmref ∧ r1 -- _length ∈ arraycopy(r, i, r0, i0, j, st) ∧ is_integervalue(arraycopy(r, i, r0, i0, j, st)[r1 -- _length]) ∧ 0 ≤ (arraycopy(r, i, r0, i0, j, st)[r1 -- _length]) .intval ∧ is_arrayref(r1, (arraycopy(r, i, r0, i0, j, st)[r1 -- _length]) .intval, arraycopy(r, i, r0, i0, j, st)) ↔ exactarray(r1, ty, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (arraycopy(r, i, r0, i0, j, st), ty, r1)]]