Proof step 1 from proof allwritesOK-ind-add-read (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  allWritesOKInd(pending, persisted, h), ¬ allWritesOKInd(pending, persisted, h + (R(t, l, v), b) ') ⊦

Rule argument

Additional information

Proof step 2 from proof allwritesOK-ind-add-read (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  allWritesOKInd(pending, persisted, vpe + h0), ¬ allWritesOKInd(pending, persisted, (vpe + h0) + (R(t, l, v), b) '), ∀ pending, persisted, t, l, v, b. ¬(allWritesOKInd(pending, persisted, h0) ∧ ¬ allWritesOKInd(pending, persisted, h0 + (R(t, l, v), b) ')) ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-base: ⊦ allWritesOKInd(pending, persisted, []); allwritesOK-ind-one: ⊦ allWritesOKInd(pending, persisted, (e, b) ') ↔ e.R? ∨ e.W? ∧ ¬ pending(e.t) ∧ (b → persisted(e.l)); List('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ R(t, l, v).R?; (s)

Proof step 3 from proof allwritesOK-ind-add-read (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  allWritesOKInd(pending, persisted, vpe ' + h0), ¬ allWritesOKInd(pending, persisted, (vpe ' + h0) + (R(t, l, v), b) '), ∀ pending0, persisted0, t0, l0, v0, b0. ¬ allWritesOKInd(pending0, persisted0, h0) ∨ allWritesOKInd(pending0, persisted0, h0 + (R(t0, l0, v0), b0) ') ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

Proof step 4 from proof allwritesOK-ind-add-read (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  vpe = (e, b1), allWritesOKInd(pending, persisted, vpe ' + h0), ¬ allWritesOKInd(pending, persisted, (vpe ' + h0) + (R(t, l, v), b) '), ∀ pending0, persisted0, t0, l0, v0, b0. ¬ allWritesOKInd(pending0, persisted0, h0) ∨ allWritesOKInd(pending0, persisted0, h0 + (R(t0, l0, v0), b0) ') ⊦

Rule argument

Additional information

Proof step 5 from proof allwritesOK-ind-add-read (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  allWritesOKInd(pending, persisted, (e, b1) ' + h0), ¬ allWritesOKInd(pending, persisted, ((e, b1) ' + h0) + (R(t, l, v), b) '), ∀ pending0, persisted0, t0, l0, v0, b0. ¬ allWritesOKInd(pending0, persisted0, h0) ∨ allWritesOKInd(pending0, persisted0, h0 + (R(t0, l0, v0), b0) ') ⊦

Rule argument

Additional information

Proof step 6 from proof allwritesOK-ind-add-read (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

  e = R(t1, l1, v1), allWritesOKInd(pending, persisted, (e, b1) ' + h0), ¬ allWritesOKInd(pending, persisted, ((e, b1) ' + h0) + (R(t, l, v), b) '), ∀ pending0, persisted0, t0, l0, v0, b0. ¬ allWritesOKInd(pending0, persisted0, h0) ∨ allWritesOKInd(pending0, persisted0, h0 + (R(t0, l0, v0), b0) ') ⊦

• Proof step 9:

  e = W(t1, l1, v1), allWritesOKInd(pending, persisted, (e, b1) ' + h0), ¬ allWritesOKInd(pending, persisted, ((e, b1) ' + h0) + (R(t, l, v), b) '), ∀ pending0, persisted0, t0, l0, v0, b0. ¬ allWritesOKInd(pending0, persisted0, h0) ∨ allWritesOKInd(pending0, persisted0, h0 + (R(t0, l0, v0), b0) ') ⊦

Rule argument

Additional information

Used simplifier rules: RWevent freely generated by R, W;;

Proof step 7 from proof allwritesOK-ind-add-read (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  allWritesOKInd(pending, persisted, h0), ¬ allWritesOKInd(pending, persisted, h0 + (R(t, l, v), b) '), ∀ pending0, persisted0, t0, l0, v0, b0. ¬ allWritesOKInd(pending0, persisted0, h0) ∨ allWritesOKInd(pending0, persisted0, h0 + (R(t0, l0, v0), b0) ') ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recR: ⊦ allWritesOKInd(pending, persisted, (R(t, l, v), b) ' + h) ↔ allWritesOKInd(pending, persisted, h); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 8 from proof allwritesOK-ind-add-read (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pending, persisted, t, l, v, b

Proof step 9 from proof allwritesOK-ind-add-read (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  allWritesOKInd(pending(t1 := ¬ b1), persisted(l1 := b1), h0), ¬ allWritesOKInd(pending(t1 := ¬ b1), persisted(l1 := b1), h0 + (R(t, l, v), b) '), ¬ pending(t1), b1 → persisted(l1), ∀ pending0, persisted0, t0, l0, v0, b0. ¬ allWritesOKInd(pending0, persisted0, h0) ∨ allWritesOKInd(pending0, persisted0, h0 + (R(t0, l0, v0), b0) ') ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recW: ⊦ allWritesOKInd(pending, persisted, (W(t, l, v), b) ' + h) ↔ ¬ pending(t) ∧ (b → persisted(l)) ∧ allWritesOKInd(pending(t := ¬ b), persisted(l := b), h); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 10 from proof allwritesOK-ind-add-read (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pending(t1 := ¬ b1), persisted(l1 := b1), t, l, v, b