Proof step 10 from proof exactarray-length-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ exactarray(val, ty, i, st) ↔ exactreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ is_arrayref(val .refval, i, st)

• Proof step 9:

  exactreftype(refval(r), mkarraytype(ty), st) ∧ refval(r) .refval ≠ jvmref ∧ (refval(r) .refval -- _length) × intval(st[r -- _length] .intval) ∈ st ∧ is_arrayref(refval(r) .refval, st[r -- _length] .intval, st) ⊦ val2int(st[r -- _length]) = st[r -- _length] .intval, r = jvmref

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, st[r -- _length] .intval, ty, refval(r))]]