Proof step 44 from proof subset-okarray (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

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

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

Rule argument

Additional information

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