Proof step 27 from proof okarray-okarray-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ okarray(val, ty, i, st) ↔ okreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ 0 ≤ i ∧ is_arrayref(val .refval, i, st) ∧ (∀ j. 0 ≤ j ∧ j < i → oktype(st[val .refval -- j '], ty, st))

• Proof step 26:

  okarray(r, ty, st), r ∈ st ⊦ r = jvmref, okreftype(refval(r), mkarraytype(ty), st) ∧ refval(r) .refval ≠ jvmref ∧ (refval(r) .refval -- _length) × intval(st[r -- _length] .intval) ∈ st ∧ 0 ≤ st[r -- _length] .intval ∧ is_arrayref(refval(r) .refval, st[r -- _length] .intval, st) ∧ (∀ j. 0 ≤ j ∧ j < st[r -- _length] .intval → oktype(st[refval(r) .refval -- j '], ty, st))

Rule argument

Additional information

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