Proof step 14 from proof exactarray-put-05 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

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

  ⊦ r = r0, exactreftype(refval(r), mkarraytype(byte_type), st[r0 -- sk, val]) ∧ r ≠ jvmref ∧ r -- _length ∈ st[r0 -- sk, val] ∧ is_integervalue(st[r0 -- sk, val][r -- _length]) ∧ 0 ≤ (st[r0 -- sk, val][r -- _length]) .intval ∧ is_arrayref(r, (st[r0 -- sk, val][r -- _length]) .intval, st[r0 -- sk, val]) ↔ exactarray(r, byte_type, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r0 -- sk, val], byte_type, r)]]