Proof step 10 from proof init-total (conclusion)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 1:

  ⊦ initundone(class1, st) ↔ (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(undone) ∈ st ∨ ¬ jvmref -- mkfs(class1, void_type, `initstate' .field) ' ∈ st ∧ _uninit ∈ st

• Proof step 2:

  ⊦ initerror(class1, st) ↔ (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(error) ∈ st

• Proof step 3:

  ⊦ initdone(class1, st) ↔ ¬ ¬ (¬ initerror(class1, st) ∧ ¬ initundone(class1, st))

• Proof step 4:

  ⊦ initundone(class1, st) ↔ ¬ ¬ ( (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(undone) ∈ st ∨ ¬ jvmref -- mkfs(class1, void_type, `initstate' .field) ' ∈ st ∧ _uninit ∈ st)

• Proof step 9:

  ¬ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ st ∧ _uninit ∈ st ∨ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ st ∧ st[jvmref -- mkfs(class, void_type, `initstate' .field) '] = initval(undone) ∨ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ st ∧ st[jvmref -- mkfs(class, void_type, `initstate' .field) '] = initval(error) ⊦ (¬ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ st ∨ st[jvmref -- mkfs(class, void_type, `initstate' .field) '] ≠ initval(undone)) ∧ (jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ st ∨ ¬ _uninit ∈ st) ↔ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ st ∧ st[jvmref -- mkfs(class, void_type, `initstate' .field) '] = initval(error)

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ rk × val ∈ st ↔ rk ∈ st ∧ st[rk] = val], [CSIMPSEQ : ⊦ rk × val ∈ st ↔ ¬ ¬ (rk ∈ st ∧ st[rk] = val)])]]