Proof step 16 from proof isobj-put-samefield-03 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ is_obj(r, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_classtype(st[r -- _type] .type) ∧ is_obj(r, st[r -- _type] .type .class, st)

• Proof step 15:

  is_obj(r, st), okval(val, ty) ⊦ mkfs(class, ty, fieldvar) ' = _type, r ≠ jvmref ∧ r -- _type ∈ st[r -- mkfs(class, ty, fieldvar) ', val] ∧ is_typevalue(st[r -- mkfs(class, ty, fieldvar) ', val][r -- _type]) ∧ is_classtype((st[r -- mkfs(class, ty, fieldvar) ', val][r -- _type]) .type) ∧ is_obj(r, (st[r -- mkfs(class, ty, fieldvar) ', val][r -- _type]) .type .class, st[r -- mkfs(class, ty, fieldvar) ', val])

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r -- mkfs(class, ty, fieldvar) ', val], r)]]