Proof step 1 from proof overwrite-persist-dependent-reads-restrict-true (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  mem ⊕ (h1 + (persistDependentReads(l, h2) | true)) ≠ mem ⊕ (h1 + (h2 | true)) ⊦

Rule argument

Additional information

Proof step 2 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  mem ⊕ (h1 + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ (h1 + h2.filter(._2)) ⊦

Rule argument

Additional information

Used simplifier rules: restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b);

Proof step 3 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  mem ⊕ ([] + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ ([] + h2.filter(._2)) ⊦

• Proof step 38:

  mem ⊕ ((vpe + h) + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ ((vpe + h) + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  mem ⊕ persistDependentReads(l, h2).filter(._2) ≠ mem ⊕ h2.filter(._2) ⊦

Rule argument

Additional information

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

Proof step 5 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  mem ⊕ persistDependentReads(l, vpe + h).filter(._2) ≠ mem ⊕ (vpe + h).filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: persistDependentReads-base: ⊦ persistDependentReads(l, []) = []; overwrite-base: ⊦ mem ⊕ [] = mem; List('a) freely generated by [], +;; ⊦ [].filter(p) = []; (s)

Proof step 6 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  mem ⊕ persistDependentReads(l, vpe ' + h).filter(._2) ≠ mem ⊕ ((vpe._2 ⊃ vpe ';[]) + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

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

Proof step 7 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  vpe = (e, boolvar), mem ⊕ persistDependentReads(l, vpe ' + h).filter(._2) ≠ mem ⊕ ((boolvar ⊃ vpe ';[]) + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 8 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  mem ⊕ persistDependentReads(l, (e, boolvar) ' + h).filter(._2) ≠ mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Proof step 9 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

  boolvar, mem ⊕ persistDependentReads(l, (e, boolvar) ' + h).filter(._2) ≠ mem ⊕ ((e, true) ' + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

• Proof step 24:

  ¬ boolvar, mem ⊕ persistDependentReads(l, (e, boolvar) ' + h).filter(._2) ≠ mem ⊕ ([] + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Proof step 10 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  mem ⊕ persistDependentReads(l, (e, true) ' + h).filter(._2) ≠ mem ⊕ ((e, true) ' + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Proof step 11 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  e = R(t, l0, v), mem ⊕ persistDependentReads(l, (e, true) ' + h).filter(._2) ≠ mem ⊕ ((e, true) ' + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

• Proof step 19:

  e = W(t, l0, v), mem ⊕ persistDependentReads(l, (e, true) ' + h).filter(._2) ≠ mem ⊕ ((e, true) ' + h.filter(._2)), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

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

Proof step 12 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  mem ⊕ persistDependentReads(l, (R(t, l0, v), true) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 13 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  l = l0, mem ⊕ persistDependentReads(l, (R(t, l0, v), true) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

• Proof step 17:

  l ≠ l0, mem ⊕ ((R(t, l0, v), true) + persistDependentReads(l, h)).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v, true, l, l0, t, h

Proof step 14 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Lemma persistDependentReads-otherread

Proof step 15 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  mem ⊕ persistDependentReads(l0, h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

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); overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 16 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l0

Proof step 17 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  l ≠ l0, mem ⊕ persistDependentReads(l, h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s)

Proof step 18 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l

Proof step 19 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  mem ⊕ persistDependentReads(l, (W(t, l0, v), true) ' + h).filter(._2) ≠ mem(l0 := v) ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 20 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  l ≠ l0, mem ⊕ ((W(t, l0, v), true) ' + persistDependentReads(l, h)).filter(._2) ≠ mem(l0 := v) ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: persistDependentReads-nextwrite: ⊦ persistDependentReads(l, (W(t, l, v), b) ' + h) = (W(t, l, v), b) ' + h; overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v, true, l, l0, t, h

Proof step 21 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Lemma persistDependentReads-otherwrite

Proof step 22 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  l ≠ l0, mem(l0 := v) ⊕ persistDependentReads(l, h).filter(._2) ≠ mem(l0 := v) ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 23 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem(l0 := v), l

Proof step 24 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  mem ⊕ persistDependentReads(l, (e, false) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

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

Proof step 25 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 26:

  e = R(t, l0, v), mem ⊕ persistDependentReads(l, (e, false) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

• Proof step 33:

  e = W(t, l0, v), mem ⊕ persistDependentReads(l, (e, false) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

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

Proof step 26 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  mem ⊕ persistDependentReads(l, (R(t, l0, v), false) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Proof step 27 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  l = l0, mem ⊕ persistDependentReads(l, (R(t, l0, v), false) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

• Proof step 31:

  l ≠ l0, mem ⊕ ((R(t, l0, v), false) + persistDependentReads(l, h)).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v, false, l, l0, t, h

Proof step 28 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Lemma persistDependentReads-otherread

Proof step 29 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  mem ⊕ persistDependentReads(l0, h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

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); overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 30 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l0

Proof step 31 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  l ≠ l0, mem ⊕ persistDependentReads(l, h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

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

Proof step 32 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l

Proof step 33 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  mem ⊕ persistDependentReads(l, (W(t, l0, v), false) ' + h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Proof step 34 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

• Proof step 36:

  l ≠ l0, mem ⊕ ((W(t, l0, v), false) ' + persistDependentReads(l, h)).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

Used simplifier rules: persistDependentReads-nextwrite: ⊦ persistDependentReads(l, (W(t, l, v), b) ' + h) = (W(t, l, v), b) ' + h; ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v, false, l, l0, t, h

Proof step 35 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Lemma persistDependentReads-otherwrite

Proof step 36 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  l ≠ l0, mem ⊕ persistDependentReads(l, h).filter(._2) ≠ mem ⊕ h.filter(._2), ∀ mem, l. mem ⊕ persistDependentReads(l, h).filter(._2) = mem ⊕ h.filter(._2) ⊦

Rule argument

Additional information

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

Proof step 37 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l

Proof step 38 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  mem ⊕ ((vpe ' + h) + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ ((vpe ' + h) + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

Rule argument

Additional information

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

Proof step 39 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 40:

  vpe = (e, b), mem ⊕ ((vpe ' + h) + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ ((vpe ' + h) + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

Rule argument

Additional information

Proof step 40 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  mem ⊕ (((e, b) ' + h) + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ (((e, b) ' + h) + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

Rule argument

Additional information

Proof step 41 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 42:

  e = R(t, l0, v), mem ⊕ (((e, b) ' + h) + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ (((e, b) ' + h) + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

• Proof step 44:

  e = W(t, l0, v), mem ⊕ (((e, b) ' + h) + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ (((e, b) ' + h) + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

Rule argument

Additional information

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

Proof step 42 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) ≠ mem ⊕ (h + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 43 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, l, h2

Proof step 44 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  mem(l0 := v) ⊕ (h + persistDependentReads(l, h2).filter(._2)) ≠ mem(l0 := v) ⊕ (h + h2.filter(._2)), ∀ mem, l, h2. mem ⊕ (h + persistDependentReads(l, h2).filter(._2)) = mem ⊕ (h + h2.filter(._2)) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 45 from proof overwrite-persist-dependent-reads-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem(l0 := v), l, h2