Proof step 27 from proof isarray-put-field (previous step)

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 26:

  ⊦ fs ' = _length, fs ' = _type, r ≠ jvmref ∧ r -- _type ∈ st[r0 -- fs ', val] ∧ is_typevalue(st[r0 -- fs ', val][r -- _type]) ∧ is_arraytype((st[r0 -- fs ', val][r -- _type]) .type) ∧ okarray(r, (st[r0 -- fs ', val][r -- _type]) .type .type, st[r0 -- fs ', val]) ↔ is_array(r, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r0 -- fs ', val], r)]]