Proof step 14 from proof is_array-byte-noref (conclusion)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ is_array(r, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_arraytype(st[r -- _type] .type) ∧ okarray(r, st[r -- _type] .type .type, st)

• Proof step 13:

  ⊦ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_arraytype(st[r -- _type] .type) ∧ okarray(r, st[r -- _type] .type .type, st) ∧ st[r -- _type] .type = mkarraytype(byte_type) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] ≠ refval(r1)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, r)]]