Proof step 30 from proof subset-exactarray (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 29:

  st ⊆ st0, 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), r ∈ st ⊦ r = jvmref, exactarray(r, ty, st0)

Rule argument

Additional information

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