Proof step 33 from proof isarray-put (previous step)

is_array(r, st), okval(val, ty) ⊦ mkfs(class, ty, fieldvar) ' = _length, ty = void_type, is_array(r, st[r1 -- mkfs(class, ty, fieldvar) ', val])

User applied rule insert rewrite lemma

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 32:
r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_arraytype(st[r -- _type] .type) ∧ okarray(r, st[r -- _type] .type .type, st), okval(val, ty) ⊦ mkfs(class, ty, fieldvar) ' = _length, ty = void_type, is_array(r, st[r1 -- mkfs(class, ty, fieldvar) ', val])

[crewrite-arg: is-any-array, F, [st, r] → [st, r]]

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