Proof step 24 from proof exactarray-put-02 (previous step)

exactarray(val, byte_type, i, st) ⊦ exactarray(val, byte_type, i, st[r0 -- j ', byteval(by)])

User applied rule insert rewrite lemma

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 23:
exactarray(val, byte_type, i, st) ⊦ exactreftype(val, mkarraytype(byte_type), st[r0 -- j ', byteval(by)]) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st[r0 -- j ', byteval(by)] ∧ is_arrayref(val .refval, i, st[r0 -- j ', byteval(by)])

[crewrite-arg: exactarray-01 , F , [st, i, ty, val] → [st[r0 -- j ', byteval(by)], i, byte_type, val] ]

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r0 -- j ', byteval(by)], i, byte_type, val)]]