Proof step 23 from proof isarray-keyin (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ is_array(r, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_arraytype(st[r -- _type] .type) ∧ okarray(r, st[r -- _type] .type .type, st)

• Proof step 22:

  st[r -- sk] = refval(r0), 0 < st[r -- (sk ' + _length ')] .intval, 0 ≤ i, i < st[r -- (sk ' + _length ')] .intval, r0 ≠ jvmref ∧ r0 -- _type ∈ st ∧ is_typevalue(st[r0 -- _type]) ∧ is_arraytype(st[r0 -- _type] .type) ∧ okarray(r0, st[r0 -- _type] .type .type, st) ⊦ r0 -- i ' ∈ st

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, r0)]]