Proof step 42 from proof initsubset-trans (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 41:

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

Rule argument

Additional information

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