Proof step 1 from proof allreadsok-ind-persist (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  allReadsOKInd(mem, persisted, h1 + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, h1 + (W(t, l, v), true) ' + persistDependentReads(l, h2)) ⊦

Rule argument

Additional information

Proof step 2 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  allReadsOKInd(mem, persisted, [] + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, [] + (W(t, l, v), true) ' + persistDependentReads(l, h2)) ⊦

• Proof step 30:

  allReadsOKInd(mem, persisted, (vpe + h) + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, (vpe + h) + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem, persisted, t, l, v, h2. ¬ ( allReadsOKInd(mem, persisted, h + (W(t, l, v), false) ' + h2) ∧ ¬ allReadsOKInd(mem, persisted, h + (W(t, l, v), true) ' + persistDependentReads(l, h2))) ⊦

Rule argument

Additional information

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

Proof step 3 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  allReadsOKInd(mem(l := v), persisted(l := false), h2), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, h2)) ⊦

Rule argument

Additional information

Used simplifier rules: allReadsOKInd-recW: ⊦ allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

Proof step 4 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  allReadsOKInd(mem(l := v), persisted(l := false), vpe + h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, vpe + h)), ∀ mem, l, v, persisted. ¬(allReadsOKInd(mem(l := v), persisted(l := false), h) ∧ ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, h))) ⊦

Rule argument

Additional information

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

Proof step 5 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  allReadsOKInd(mem(l := v), persisted(l := false), vpe ' + h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, vpe ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

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

Proof step 6 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

  vpe = (e, b), allReadsOKInd(mem(l := v), persisted(l := false), vpe ' + h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, vpe ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Proof step 7 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  allReadsOKInd(mem(l := v), persisted(l := false), (e, b) ' + h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, (e, b) ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Proof step 8 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  e = R(t, l1, v1), allReadsOKInd(mem(l := v), persisted(l := false), (e, b) ' + h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, (e, b) ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

• Proof step 16:

  e = W(t, l1, v1), allReadsOKInd(mem(l := v), persisted(l := false), (e, b) ' + h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, (e, b) ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

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

Proof step 9 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  allReadsOKInd(mem(l := v), persisted(l := false), h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, (R(t, l1, (l = l1 ⊃ v;mem(l1))), l ≠ l1 ∧ persisted(l1)) ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

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

Proof step 10 from proof allreadsok-ind-persist (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, allReadsOKInd(mem(l := v), persisted(l := false), h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, (R(t, l1, (l = l1 ⊃ v;mem(l1))), l ≠ l1 ∧ persisted(l1)) ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

• Proof step 14:

  l ≠ l1, allReadsOKInd(mem(l := v), persisted(l := false), h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), (R(t, l1, (l = l1 ⊃ v;mem(l1))), l ≠ l1 ∧ persisted(l1)) + persistDependentReads(l, h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

Used terms: (l = l1 ⊃ v;mem(l1)), l ≠ l1 ∧ persisted(l1), l, l1, t, h

Proof step 11 from proof allreadsok-ind-persist (previous step) (back to tree)

Lemma persistDependentReads-otherread

Proof step 12 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  allReadsOKInd(mem(l1 := v), persisted(l1 := false), h), ¬ allReadsOKInd(mem(l1 := v), persisted(l1 := true), persistDependentReads(l1, h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), 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); allReadsOKInd-recR: ⊦ allReadsOKInd(mem, persisted, (R(t, l, v), b) ' + h) ↔ v = mem(l) ∧ (b ↔ persisted(l)) ∧ allReadsOKInd(mem, persisted, h); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 13 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l1, v, persisted

Proof step 14 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  l ≠ l1, allReadsOKInd(mem(l := v), persisted(l := false), h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

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

Proof step 15 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l, v, persisted

Proof step 16 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), persistDependentReads(l, (W(t, l1, v1), b) ' + h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

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

Proof step 17 from proof allreadsok-ind-persist (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, allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), (W(t, l1, v1), b) ' + persistDependentReads(l, h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), 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; allReadsOKInd-recW: ⊦ allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h); mem-update-same: ⊦ mem(l := v0)(l := v) = mem(l := v); persisted-update-same: ⊦ persisted(l := b0)(l := b) = persisted(l := b); a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v1, b, l, l1, t, h

Proof step 18 from proof allreadsok-ind-persist (previous step) (back to tree)

Lemma persistDependentReads-otherwrite

Proof step 19 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  l ≠ l1, allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := true)(l1 := b), persistDependentReads(l, h)), ∀ mem0, l0, v0, persisted0. ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := true), persistDependentReads(l0, h)) ⊦

Rule argument

Additional information

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

Proof step 20 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 21:

  l ≠ l1, allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := true)(l1 := b), persistDependentReads(l, h)), ¬ allReadsOKInd(mem(l1 := v1)(l := v), persisted(l1 := b)(l := false), h) ∨ allReadsOKInd(mem(l1 := v1)(l := v), persisted(l1 := b)(l := true), persistDependentReads(l, h)) ⊦

Rule argument

Additional information

Used terms: mem(l1 := v1), l, v, persisted(l1 := b)

Proof step 21 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 22:

  l ≠ l1, allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l1 := v1)(l := v), persisted(l1 := b)(l := false), h), ¬ allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := true)(l1 := b), persistDependentReads(l, h)) ⊦

• Proof step 26:

  l ≠ l1, allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), allReadsOKInd(mem(l1 := v1)(l := v), persisted(l1 := b)(l := true), persistDependentReads(l, h)), ¬ allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := true)(l1 := b), persistDependentReads(l, h)) ⊦

Rule argument

Additional information

Proof step 22 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ l0 ≠ l1 → persisted(l0 := b0)(l1 := b1) = persisted(l1 := b1)(l0 := b0)

• Proof step 24:

  l ≠ l1, allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l1 := v1)(l := v), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := true)(l1 := b), persistDependentReads(l, h)) ⊦

Rule argument

Additional information

Used terms: persisted, false, l, b, l1

Proof step 23 from proof allreadsok-ind-persist (previous step) (back to tree)

Lemma persisted-update-swap

Proof step 24 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ l0 ≠ l1 → mem(l0 := v0)(l1 := v1) = mem(l1 := v1)(l0 := v0)

Rule argument

Additional information

Used terms: l, mem, v, l1, v1

Proof step 25 from proof allreadsok-ind-persist (previous step) (back to tree)

Lemma mem-update-swap

Proof step 26 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ l0 ≠ l1 → persisted(l0 := b0)(l1 := b1) = persisted(l1 := b1)(l0 := b0)

• Proof step 28:

  l ≠ l1, allReadsOKInd(mem(l1 := v1)(l := v), persisted(l := true)(l1 := b), persistDependentReads(l, h)), allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := false)(l1 := b), h), ¬ allReadsOKInd(mem(l := v)(l1 := v1), persisted(l := true)(l1 := b), persistDependentReads(l, h)) ⊦

Rule argument

Additional information

Used terms: persisted, true, l, b, l1

Proof step 27 from proof allreadsok-ind-persist (previous step) (back to tree)

Lemma persisted-update-swap

Proof step 28 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ l0 ≠ l1 → mem(l0 := v0)(l1 := v1) = mem(l1 := v1)(l0 := v0)

Rule argument

Additional information

Used terms: l, mem, v, l1, v1

Proof step 29 from proof allreadsok-ind-persist (previous step) (back to tree)

Lemma mem-update-swap

Proof step 30 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  allReadsOKInd(mem, persisted, (vpe ' + h) + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, (vpe ' + h) + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem0, persisted0, t0, l0, v0, h0. ¬ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ∨ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), true) ' + 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 31 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 32:

  vpe = (e, b), allReadsOKInd(mem, persisted, (vpe ' + h) + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, (vpe ' + h) + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem0, persisted0, t0, l0, v0, h0. ¬ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ∨ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), true) ' + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

Proof step 32 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  allReadsOKInd(mem, persisted, ((e, b) ' + h) + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, ((e, b) ' + h) + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem0, persisted0, t0, l0, v0, h0. ¬ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ∨ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), true) ' + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

Proof step 33 from proof allreadsok-ind-persist (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 34:

  e = R(t1, l1, v1), allReadsOKInd(mem, persisted, ((e, b) ' + h) + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, ((e, b) ' + h) + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem0, persisted0, t0, l0, v0, h0. ¬ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ∨ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), true) ' + persistDependentReads(l0, h0)) ⊦

• Proof step 36:

  e = W(t1, l1, v1), allReadsOKInd(mem, persisted, ((e, b) ' + h) + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, ((e, b) ' + h) + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem0, persisted0, t0, l0, v0, h0. ¬ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ∨ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), true) ' + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

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

Proof step 34 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  allReadsOKInd(mem, persisted, h + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem, persisted, h + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem0, persisted0, t0, l0, v0, h0. ¬ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ∨ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), true) ' + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

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

Proof step 35 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: mem, persisted, t, l, v, h2

Proof step 36 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  allReadsOKInd(mem(l1 := v1), persisted(l1 := b), h + (W(t, l, v), false) ' + h2), ¬ allReadsOKInd(mem(l1 := v1), persisted(l1 := b), h + (W(t, l, v), true) ' + persistDependentReads(l, h2)), ∀ mem0, persisted0, t0, l0, v0, h0. ¬ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ∨ allReadsOKInd(mem0, persisted0, h + (W(t0, l0, v0), true) ' + persistDependentReads(l0, h0)) ⊦

Rule argument

Additional information

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

Proof step 37 from proof allreadsok-ind-persist (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: mem(l1 := v1), persisted(l1 := b), t, l, v, h2