Proof step 23 from proof exactarray-put (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ 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 22:

  exactarray(r, byte_type, st), r ∈ st ⊦ r = jvmref, exactreftype(refval(r), mkarraytype(byte_type), st[r0 -- i ', byteval(by)]) ∧ r ≠ jvmref ∧ r -- _length ∈ st[r0 -- i ', byteval(by)] ∧ is_integervalue(st[r0 -- i ', byteval(by)][r -- _length]) ∧ 0 ≤ (st[r0 -- i ', byteval(by)][r -- _length]) .intval ∧ is_arrayref(r, (st[r0 -- i ', byteval(by)][r -- _length]) .intval, st[r0 -- i ', byteval(by)])

Rule argument

Additional information

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