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

⊦ r = r0, okarray(refval(r0), ty, i, putByteArray(bytes, r, i1, st)) ↔ okarray(refval(r0), ty, i, st)

User applied rule insert rewrite lemma

Proof step 2:
⊦ okarray(val, ty, i, st) ↔ okreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ 0 ≤ i ∧ is_arrayref(val .refval, i, st) ∧ (∀ j. 0 ≤ j ∧ j < i → oktype(st[val .refval -- j '], ty, st))
Proof step 28:
⊦ r = r0, okreftype(refval(r0), mkarraytype(ty), putByteArray(bytes, r, i1, st)) ∧ refval(r0) .refval ≠ jvmref ∧ (refval(r0) .refval -- _length) × intval(i) ∈ putByteArray(bytes, r, i1, st) ∧ 0 ≤ i ∧ is_arrayref(refval(r0) .refval, i, putByteArray(bytes, r, i1, st)) ∧ (∀ j. 0 ≤ j ∧ j < i → oktype(putByteArray(bytes, r, i1, st)[refval(r0) .refval -- j '], ty, putByteArray(bytes, r, i1, st))) ↔ okarray(refval(r0), ty, i, st)

[crewrite-arg: okarrayOfLength , F , [st, i, ty, val] → [putByteArray(bytes, r, i1, st), i, ty, refval(r0)] ]

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (putByteArray(bytes, r, i1, st), i, ty, refval(r0))]]