Proof step 23 from proof subset-len-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

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

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

Rule argument

Additional information

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