Proof step 9 from proof validmode-addobj (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ validmode(str, val, st) ↔ val = noval ∨ is_break_mode(val) ∨ val = return(noval, void_type) ∨ is_return_mode(val) ∧ validref(str, val .refval, val .type, st) ∨ is_throw_mode(val) ∧ val .refval ≠ jvmref ∧ validref(str, val .refval, val .type, st) ∧ val .type ≤ mkclasstype(`java.lang.Throwable' .class)

• Proof step 8:

  newref(r, st), _mode ∈ st ⊦ r = jvmref, st[_mode] = noval ∨ is_break_mode(st[_mode]) ∨ st[_mode] = return(noval, void_type) ∨ is_return_mode(st[_mode]) ∧ validref(str, st[_mode] .refval, st[_mode] .type, addobj(r, class, fis, st)) ∨ is_throw_mode(st[_mode]) ∧ st[_mode] .refval ≠ jvmref ∧ validref(str, st[_mode] .refval, st[_mode] .type, addobj(r, class, fis, st)) ∧ st[_mode] .type ≤ mkclasstype(`java.lang.Throwable' .class) ↔ validmode(str, st[_mode], st)

Rule argument

Additional information

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