Proof step 42 from proof isarray-update (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ okarray(r, ty, st) ↔ okreftype(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) ∧ (∀ j. 0 ≤ j ∧ j < st[r -- _length] .intval → oktype(st[r -- j '], ty, st))

• Proof step 41:

  st[r -- _type] = typeval(mkarraytype(ty)), r -- _type ∈ st, r ∈ st ⊦ r = r0, okreftype(refval(r), mkarraytype(ty), update(r0, fis, st)) ∧ r ≠ jvmref ∧ r -- _length ∈ update(r0, fis, st) ∧ is_integervalue(update(r0, fis, st)[r -- _length]) ∧ 0 ≤ (update(r0, fis, st)[r -- _length]) .intval ∧ is_arrayref(r, (update(r0, fis, st)[r -- _length]) .intval, update(r0, fis, st)) ∧ (∀ j. 0 ≤ j ∧ j < (update(r0, fis, st)[r -- _length]) .intval → oktype(update(r0, fis, st)[r -- j '], ty, update(r0, fis, st))) ↔ okarray(r, ty, st), r = jvmref

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (update(r0, fis, st), ty, r)]]