Proof step 22 from proof exactarray-putbar (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ exactarray(val, ty, i, st) ↔ exactreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ is_arrayref(val .refval, i, st)

• Proof step 21:

  ⊦ r = r1, exactreftype(refval(r1), mkarraytype(byte_type), putByteArray(bytes, r, i, st)) ∧ refval(r1) .refval ≠ jvmref ∧ (refval(r1) .refval -- _length) × intval(j) ∈ putByteArray(bytes, r, i, st) ∧ is_arrayref(refval(r1) .refval, j, putByteArray(bytes, r, i, st)) ↔ exactarray(refval(r1), byte_type, j, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (putByteArray(bytes, r, i, st), j, byte_type, refval(r1))]]