Proof step 22 from proof exactarray-08 (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 21:

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

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, int_type, r)]]