Proof step 29 from proof okarray-copy (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ okarray(r, ty, st) ↔ okreftype(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) ∧ (∀ j. 0 ≤ j ∧ j < st[r -- _length] .intval → oktype(st[r -- j '], ty, st))

• Proof step 28:

  ⊦ r1 = r0, okreftype(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)) ∧ (∀ j0. 0 ≤ j0 ∧ j0 < (arraycopy(r, i, r0, i0, j, st)[r1 -- _length]) .intval → oktype(arraycopy(r, i, r0, i0, j, st)[r1 -- j0 '], ty, arraycopy(r, i, r0, i0, j, st))) ↔ okarray(r1, ty, st)

Rule argument

Additional information

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