Proof step 1 from proof allwritesOK-ind-persist-dependent-reads (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  allWritesOKInd(pending, persisted, h1 + h2), ¬ allWritesOKInd(pending, persisted, h1 + persistDependentReads(l, h2)) ⊦

Rule argument

Additional information

Proof step 2 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  allWritesOKInd(pending, persisted, [] + h2), ¬ allWritesOKInd(pending, persisted, [] + persistDependentReads(l, h2)) ⊦

• Proof step 21:

  allWritesOKInd(pending, persisted, (vpe + h) + h2), ¬ allWritesOKInd(pending, persisted, (vpe + h) + persistDependentReads(l, h2)), ∀ pending, persisted, h2, l. ¬(allWritesOKInd(pending, persisted, h + h2) ∧ ¬ allWritesOKInd(pending, persisted, h + persistDependentReads(l, h2))) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

Proof step 3 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  allWritesOKInd(pending, persisted, h2), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, h2)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  allWritesOKInd(pending, persisted, vpe + h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, vpe + h)), ∀ pending, persisted, l. ¬(allWritesOKInd(pending, persisted, h) ∧ ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, h))) ⊦

Rule argument

Additional information

Used simplifier rules: persistDependentReads-base: ⊦ persistDependentReads(l, []) = []; allWritesOKInd-base: ⊦ allWritesOKInd(pending, persisted, []); List('a) freely generated by [], +;;

Proof step 5 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  allWritesOKInd(pending, persisted, vpe ' + h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, vpe ' + h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 6 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

  vpe = (e, b), allWritesOKInd(pending, persisted, vpe ' + h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, vpe ' + h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Proof step 7 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  allWritesOKInd(pending, persisted, (e, b) ' + h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, (e, b) ' + h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Proof step 8 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  e = R(t, l1, v), allWritesOKInd(pending, persisted, (e, b) ' + h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, (e, b) ' + h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

• Proof step 16:

  e = W(t, l1, v), allWritesOKInd(pending, persisted, (e, b) ' + h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, (e, b) ' + h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

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

Proof step 9 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  allWritesOKInd(pending, persisted, h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, (R(t, l1, v), b) ' + h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

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 10 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ l ≠ l0 → persistDependentReads(l, (R(t, l0, v), b) ' + h) = (R(t, l0, v), b) + persistDependentReads(l, h)

• Proof step 12:

  l = l1, allWritesOKInd(pending, persisted, h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, (R(t, l1, v), b) ' + h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

• Proof step 14:

  l ≠ l1, allWritesOKInd(pending, persisted, h), ¬ allWritesOKInd(pending, persisted, (R(t, l1, v), b) + persistDependentReads(l, h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Used terms: v, b, l, l1, t, h

Proof step 11 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Lemma persistDependentReads-otherread

Proof step 12 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  allWritesOKInd(pending, persisted, h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l1, h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Used simplifier rules: persistDependentReads-read: ⊦ persistDependentReads(l, (R(t, l, v), b) ' + h) = (R(t, l, v), true) ' + persistDependentReads(l, h); 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 13 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pending, persisted, l1

Proof step 14 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  l ≠ l1, allWritesOKInd(pending, persisted, h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, h)), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

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 ⊦ a + x = a ' + x; (s)

Proof step 15 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pending, persisted, l

Proof step 16 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  allWritesOKInd(pending(t := ¬ b), persisted(l1 := b), h), ¬ allWritesOKInd(pending, persisted, persistDependentReads(l, (W(t, l1, v), b) ' + h)), ¬ pending(t), b → persisted(l1), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

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 17 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ l ≠ l0 → persistDependentReads(l, (W(t, l0, v), b) ' + h) = (W(t, l0, v), b) ' + persistDependentReads(l, h)

• Proof step 19:

  l ≠ l1, allWritesOKInd(pending(t := ¬ b), persisted(l1 := b), h), ¬ allWritesOKInd(pending, persisted, (W(t, l1, v), b) ' + persistDependentReads(l, h)), ¬ pending(t), b → persisted(l1), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Used simplifier rules: persistDependentReads-nextwrite: ⊦ persistDependentReads(l, (W(t, l, v), b) ' + h) = (W(t, l, v), b) ' + h; 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 Used terms: v, b, l, l1, t, h

Proof step 18 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Lemma persistDependentReads-otherwrite

Proof step 19 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  l ≠ l1, allWritesOKInd(pending(t := ¬ b), persisted(l1 := b), h), ¬ allWritesOKInd(pending(t := ¬ b), persisted(l1 := b), persistDependentReads(l, h)), ¬ pending(t), b → persisted(l1), ∀ pending0, persisted0, l0. ¬ allWritesOKInd(pending0, persisted0, h) ∨ allWritesOKInd(pending0, persisted0, persistDependentReads(l0, h)) ⊦

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 20 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 21 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  allWritesOKInd(pending, persisted, (vpe ' + h) + h2), ¬ allWritesOKInd(pending, persisted, (vpe ' + h) + persistDependentReads(l, h2)), ∀ pending0, persisted0, h0, l0. ¬ allWritesOKInd(pending0, persisted0, h + h0) ∨ allWritesOKInd(pending0, persisted0, h + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

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

Proof step 22 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 23:

  vpe = (e, b), allWritesOKInd(pending, persisted, (vpe ' + h) + h2), ¬ allWritesOKInd(pending, persisted, (vpe ' + h) + persistDependentReads(l, h2)), ∀ pending0, persisted0, h0, l0. ¬ allWritesOKInd(pending0, persisted0, h + h0) ∨ allWritesOKInd(pending0, persisted0, h + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

Proof step 23 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  allWritesOKInd(pending, persisted, ((e, b) ' + h) + h2), ¬ allWritesOKInd(pending, persisted, ((e, b) ' + h) + persistDependentReads(l, h2)), ∀ pending0, persisted0, h0, l0. ¬ allWritesOKInd(pending0, persisted0, h + h0) ∨ allWritesOKInd(pending0, persisted0, h + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

Proof step 24 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 25:

  e = R(t, l1, v), allWritesOKInd(pending, persisted, ((e, b) ' + h) + h2), ¬ allWritesOKInd(pending, persisted, ((e, b) ' + h) + persistDependentReads(l, h2)), ∀ pending0, persisted0, h0, l0. ¬ allWritesOKInd(pending0, persisted0, h + h0) ∨ allWritesOKInd(pending0, persisted0, h + persistDependentReads(l0, h0)) ⊦

• Proof step 27:

  e = W(t, l1, v), allWritesOKInd(pending, persisted, ((e, b) ' + h) + h2), ¬ allWritesOKInd(pending, persisted, ((e, b) ' + h) + persistDependentReads(l, h2)), ∀ pending0, persisted0, h0, l0. ¬ allWritesOKInd(pending0, persisted0, h + h0) ∨ allWritesOKInd(pending0, persisted0, h + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

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

Proof step 25 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  allWritesOKInd(pending, persisted, h + h2), ¬ allWritesOKInd(pending, persisted, h + persistDependentReads(l, h2)), ∀ pending0, persisted0, h0, l0. ¬ allWritesOKInd(pending0, persisted0, h + h0) ∨ allWritesOKInd(pending0, persisted0, h + persistDependentReads(l0, h0)) ⊦

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 26 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pending, persisted, h2, l

Proof step 27 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  allWritesOKInd(pending(t := ¬ b), persisted(l1 := b), h + h2), ¬ allWritesOKInd(pending(t := ¬ b), persisted(l1 := b), h + persistDependentReads(l, h2)), ¬ pending(t), b → persisted(l1), ∀ pending0, persisted0, h0, l0. ¬ allWritesOKInd(pending0, persisted0, h + h0) ∨ allWritesOKInd(pending0, persisted0, h + persistDependentReads(l0, h0)) ⊦

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 28 from proof allwritesOK-ind-persist-dependent-reads (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pending(t := ¬ b), persisted(l1 := b), h2, l