Proof step 38 from proof isobj-addobj-04 (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 37:

  fis .keys = instfields(class), validfieldinits(fis, st) ⊦ r = jvmref, r ≠ jvmref ∧ r -- _type ∈ addobj(r, class, fis, st) ∧ is_typevalue(addobj(r, class, fis, st)[r -- _type]) ∧ is_classtype((addobj(r, class, fis, st)[r -- _type]) .type) ∧ is_obj(r, (addobj(r, class, fis, st)[r -- _type]) .type .class, addobj(r, class, fis, st))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (addobj(r, class, fis, st), r)]]