Proof step 30 from proof okarray-putbar-01 (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 29:

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

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (putByteArray(bytes, r1, 0, st), byte_type, r)]]