Proof step 11 from proof validmode-superset (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 4:

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

  _mode ∈ st0, st ⊆ st0, validmode(str, st[_mode], st), _mode ∈ st ⊦ 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, st0) ∨ is_throw_mode(st[_mode]) ∧ st[_mode] .refval ≠ jvmref ∧ validref(str, st[_mode] .refval, st[_mode] .type, st0) ∧ st[_mode] .type ≤ mkclasstype(`java.lang.Throwable' .class)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st0, st[_mode], str)]]