Proof step 27 from proof getarray-subset-02 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

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

  st ⊆ st0, r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_arraytype(st[r -- _type] .type) ∧ okarray(r, st[r -- _type] .type .type, st), i + j ≤ st[r -- _length] .intval, 0 ≤ i ⊦ getarray(r, i, j, st) = getarray(r, i, j, st0), is_arrayref(r, i + j, st)

Rule argument

Additional information

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