Proof step 4 from proof eqmode-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ st =mode st0 ↔ st = st0 ∨ (∃ r, class1. st = (st0[r -- _type, typeval(mkclasstype(class1))][_mode, throw(r, mkclasstype(class1))]) ∧ newref(r, st0))

• Proof step 3:

  newref(r, st) ⊦ r = jvmref, (st[r -- _type, typeval(mkclasstype(class1))][_mode, throw(r, mkclasstype(class1))]) = st ∨ (∃ r0, class. (st[r -- _type, typeval(mkclasstype(class1))][_mode, throw(r, mkclasstype(class1))]) = (st[r0 -- _type, typeval(mkclasstype(class))][_mode, throw(r0, mkclasstype(class))]) ∧ newref(r0, st))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, st[r -- _type, typeval(mkclasstype(class1))] [_mode, throw(r, mkclasstype(class1)) ])]]