Proof step 25 from proof init-put-field (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ init(st) ↔ ¬ _uninit ∈ st ∧ (∀ rk. rk ∈ st ∧ rk .ref = jvmref ∧ is_fskey(rk .key) ∧ rk .key .fs .type = void_type ∧ rk .key .fs .field = `initstate' .field → st[rk] ≠ initval(undone) ∧ st[rk] ≠ initval(error))

• Proof step 24:

  ⊦ ty = void_type, ¬ _uninit ∈ st[r -- mkfs(class, ty, fieldvar) ', val] ∧ (∀ rk. rk ∈ st[r -- mkfs(class, ty, fieldvar) ', val] ∧ rk .ref = jvmref ∧ is_fskey(rk .key) ∧ rk .key .fs .type = void_type ∧ rk .key .fs .field = `initstate' .field → (st[r -- mkfs(class, ty, fieldvar) ', val][rk]) ≠ initval(undone) ∧ (st[r -- mkfs(class, ty, fieldvar) ', val][rk]) ≠ initval(error)) ↔ init(st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r -- mkfs(class, ty, fieldvar) ', val])]]