Proof step 1 from proof init-state-inv (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, pcf = (λ t. idle), ¬ PLIBInv(gs, lsf, pcf), ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Proof step 2 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ¬ PLIBInv(gs, lsf, λ t. idle), ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Proof step 3 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ PLIBInv(gs, lsf, pcf) ↔ PLIBGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ PLIBLInv(gs, lsf(t), pcf(t)))

• Proof step 5:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ PLIBGInv(gs) ∨ (∃ t. ¬(lsf(t).t = t ∧ PLIBLInv(gs, lsf(t), idle))) ⊦

Rule argument

Additional information

Used terms: gs, lsf, λ t. idle

Proof step 4 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ PLIBGInv(gs) ∨ lsf(t).t ≠ t ∨ ¬ PLIBLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Proof step 6 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ PLIBGInv(gs) ↔ allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)

• Proof step 8:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬(allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∨ lsf(t).t ≠ t ∨ ¬ PLIBLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Used terms: gs

Proof step 7 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ allReadsOK([]) ∨ ¬ allWritesOK([]) ∨ lsf(t).t ≠ t ∨ ¬ PLIBLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mem ⊕ [] = mem; (s) ⊦ [] | b = []; (s)

Proof step 9 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ allReadsOK(h) ↔ allReadsOKInd(∅, λ l. true, h)

• Proof step 11:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ allReadsOKInd(∅, λ l. true, []) ∨ ¬ allWritesOK([]) ∨ lsf(t).t ≠ t ∨ ¬ PLIBLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Used terms: []

Proof step 10 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ allWritesOK([]) ∨ lsf(t).t ≠ t ∨ ¬ PLIBLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ allReadsOKInd(mem, persisted, []); (s)

Proof step 12 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ PLIBLInv(gs, ls, pc) ↔ pc = resWrite → (gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) '

• Proof step 14:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ allWritesOK([]) ∨ lsf(t).t ≠ t ∨ ¬(idle = resWrite → (gs.h | lsf(t).t) | false = [] ∨ (gs.h | lsf(t).t) | false = (W(lsf(t).t, lsf(t).il, lsf(t).iv), false) ') ⊦

Rule argument

Additional information

Used terms: gs, lsf(t), idle

Proof step 13 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ allWritesOK([]) ∨ lsf(t).t ≠ t ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ idle ≠ resWrite; (s)

Proof step 15 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ allWritesOK(h) ↔ allWritesOKInd(λ t. false, λ l. true, h)

• Proof step 17:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, ∀ t. t = lsf(t).t, ¬ allWritesOKInd(λ t. false, λ l. true, []) ∨ lsf(t).t ≠ t ⊦

Rule argument

Additional information

Used terms: []

Proof step 16 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  gs.h = [], gs.pm = ∅, gs.vm = ∅, lsf(t).t ≠ t, ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ allWritesOKInd(pending, persisted, []); (s)

Proof step 18 from proof init-state-inv (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t