Proof step 29 from proof okarray-08 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 4:

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

  is_integervalue(val), okarray(r0, int_type, st), r0 ∈ st ⊦ r0 = jvmref, okreftype(refval(r0), mkarraytype(int_type), st[r0 -- j ', val]) ∧ r0 ≠ jvmref ∧ r0 -- _length ∈ st[r0 -- j ', val] ∧ is_integervalue(st[r0 -- j ', val][r0 -- _length]) ∧ 0 ≤ (st[r0 -- j ', val][r0 -- _length]) .intval ∧ is_arrayref(r0, (st[r0 -- j ', val][r0 -- _length]) .intval, st[r0 -- j ', val]) ∧ (∀ j0. 0 ≤ j0 ∧ j0 < (st[r0 -- j ', val][r0 -- _length]) .intval → oktype(st[r0 -- j ', val][r0 -- j0 '], int_type, st[r0 -- j ', val]))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r0 -- j ', val], int_type, r0)]]