Proof step 5 from proof initsubset-addobj-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ init⊆(str, st, st0) ↔ (∀ class. initdone(class, st) → initdone(class, st0)) ∧ (∀ class. initerror(class, st) → initerror(class, st0)) ∧ (∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0)) ∧ (∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0))

• Proof step 4:

  newref(r, st0) ⊦ r = jvmref, (∀ class0. initdone(class0, st0) → initdone(class0, addobj(r, class, fis, st0))) ∧ (∀ class0. initerror(class0, st0) → initerror(class0, addobj(r, class, fis, st0))) ∧ (∀ class0. ¬ initdone(class0, st0) ∧ initdone(class0, addobj(r, class, fis, st0)) ∧ tdname∃(str, class0) → validstatfields(str, statfields(class0), addobj(r, class, fis, st0))) ∧ (∀ class0, sk. initdone(class0, st0) ∧ initdone(class0, addobj(r, class, fis, st0)) ∧ tdname∃(str, class0) ∧ sk ∈ statfields(class0) ∧ validstatfield(str, sk, st0) → validstatfield(str, sk, addobj(r, class, fis, st0)))

Rule argument

Additional information

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