[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 37 from proof initsubset-trans (previous step)

∀ 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), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class. initerror(class, st) → initerror(class, st0), ∀ class. initdone(class, st) → initdone(class, st0) ⊦ (∀ class. initdone(class, st) → initdone(class, st1)) ∧ (∀ class. initerror(class, st) → initerror(class, st1)) ∧ (∀ class. ¬ initdone(class, st) ∧ initdone(class, st1) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st1)) ∧ (∀ class, sk. initdone(class, st) ∧ initdone(class, st1) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st1))

User applied rule case distinction

And obtained the following new goals

Proof step 7:
∀ 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), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class. initerror(class, st) → initerror(class, st0), ∀ class. initdone(class, st) → initdone(class, st0) ⊦ ∀ class. initdone(class, st) → initdone(class, st1)
Proof step 11:
∀ 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), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class. initerror(class, st) → initerror(class, st0), ∀ class. initdone(class, st) → initdone(class, st0) ⊦ ∀ class. initerror(class, st) → initerror(class, st1)
Proof step 30:
∀ 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), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class. initerror(class, st) → initerror(class, st0), ∀ class. initdone(class, st) → initdone(class, st0) ⊦ ∀ class. ¬ initdone(class, st) ∧ initdone(class, st1) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st1)
Proof step 36:
∀ 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), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class. initerror(class, st) → initerror(class, st0), ∀ class. initdone(class, st) → initdone(class, st0) ⊦ ∀ class, sk. initdone(class, st) ∧ initdone(class, st1) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st1)

Rule argument

[CASEDARG : pos: right 1, ()]

Additional information

[[CONCRETESIMPRULES : ()]]