Proof step 53 from proof initsubset-initerror-04 (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 52:

  init⊆(str, st, st0) ⊦ initdone(class, st), (∀ class0. initdone(class0, st) → initdone(class0, st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) ∧ (∀ class0. initerror(class0, st) → initerror(class0, st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) ∧ (∀ class0. ¬ initdone(class0, st) ∧ initdone(class0, st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]) ∧ tdname∃(str, class0) → validstatfields(str, statfields(class0), st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) ∧ (∀ class0, sk. initdone(class0, st) ∧ initdone(class0, st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]) ∧ tdname∃(str, class0) ∧ sk ∈ statfields(class0) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st0[ jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)], st, str)]]