Proof step 25 from proof okarray-putar (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

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

  ⊦ r = r1, okreftype(refval(r1), mkarraytype(byte_type), putArray(vals, r, i, st)) ∧ refval(r1) .refval ≠ jvmref ∧ (refval(r1) .refval -- _length) × intval(j) ∈ putArray(vals, r, i, st) ∧ 0 ≤ j ∧ is_arrayref(refval(r1) .refval, j, putArray(vals, r, i, st)) ∧ (∀ j0. 0 ≤ j0 ∧ j0 < j → oktype(putArray(vals, r, i, st)[refval(r1) .refval -- j0 '], byte_type, putArray(vals, r, i, st))) ↔ okarray(refval(r1), byte_type, j, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (putArray(vals, r, i, st), j, byte_type, refval(r1))]]