Proof step 7 from proof isarray-union (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

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

  st[r -- _type] = typeval(mkarraytype(ty)), r -- _type ∈ st, okarray(r, ty, st), r ∈ st ⊦ r = jvmref, r ≠ jvmref ∧ r -- _type ∈ st0 ∪ st ∧ is_typevalue((st0 ∪ st)[r -- _type]) ∧ is_arraytype((st0 ∪ st)[r -- _type] .type) ∧ okarray(r, (st0 ∪ st)[r -- _type] .type .type, st0 ∪ st)

Rule argument

Additional information

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