Proof step 31 from proof initsubset-validstatfield-forward (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 30:

  validstatfield(str, sk, st), (∀ 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)) ⊦ validstatfield(str, sk, st0)

Rule argument

Additional information

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