Proof step 1 from proof persist-dependent-reads-unchanged-writes (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  persistDependentReads(l0, h) |W ≠ h |W ⊦

Rule argument

Additional information

Proof step 2 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  persistDependentReads(l0, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used simplifier rules: restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?);

Proof step 3 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 4:

  hPred([]), ∀ t, l, v, h. hPred(h) → hPred((W(t, l, v), true) ' + h), ∀ t, l, v, h. hPred(h) → hPred((W(t, l, v), false) ' + h), ∀ t, l, v, h. hPred(h) → hPred((R(t, l, v), true) ' + h), ∀ t, l, v, h. hPred(h) → hPred((R(t, l, v), false) ' + h) ⊦ hPred(h)

• Proof step 5:

  [] = h, persistDependentReads(l0, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?) ⊦

• Proof step 6:

  ∀ l0, h1. ¬(h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?)) ⊦ ∀ l0, h1. ¬((W(t, l, v), true) ' + h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?))

• Proof step 11:

  ∀ l0, h1. ¬(h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?)) ⊦ ∀ l0, h1. ¬((W(t, l, v), false) ' + h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?))

• Proof step 16:

  ∀ l0, h1. ¬(h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?)) ⊦ ∀ l0, h1. ¬((R(t, l, v), true) ' + h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?))

• Proof step 23:

  ∀ l0, h1. ¬(h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?)) ⊦ ∀ l0, h1. ¬((R(t, l, v), false) ' + h = h1 ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.W?) ≠ h1.filter(λ vpe. vpe._1.W?))

Rule argument

Additional information

Used terms: h, λ h0. ∀ l0, h. ¬ ( h0 = h ∧ persistDependentReads(l0, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?))

Proof step 4 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Lemma hist-ind

Proof step 5 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: persistDependentReads-base: ⊦ persistDependentReads(l, []) = []; ⊦ [].filter(p) = []; (s)

Proof step 6 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  persistDependentReads(l0, (W(t, l, v), true) ' + h).filter(λ vpe. vpe._1.W?) ≠ (W(t, l, v), true) ' + h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

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

Proof step 7 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  ((W(t, l, v), true) ' + persistDependentReads(l0, h)).filter(λ vpe. vpe._1.W?) ≠ (W(t, l, v), true) ' + h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

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) ⊦ W(t, l, v).W?; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v, true, l0, l, t, h

Proof step 8 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Lemma persistDependentReads-otherwrite

Proof step 9 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  persistDependentReads(l0, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ W(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 10 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 11 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  persistDependentReads(l0, (W(t, l, v), false) ' + h).filter(λ vpe. vpe._1.W?) ≠ (W(t, l, v), false) ' + h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

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

Proof step 12 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  ((W(t, l, v), false) ' + persistDependentReads(l0, h)).filter(λ vpe. vpe._1.W?) ≠ (W(t, l, v), false) ' + h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

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) ⊦ W(t, l, v).W?; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v, false, l0, l, t, h

Proof step 13 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Lemma persistDependentReads-otherwrite

Proof step 14 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  persistDependentReads(l0, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ W(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 15 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 16 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  persistDependentReads(l0, (R(t, l, v), true) ' + h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ ¬ R(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 17 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  l0 = l, persistDependentReads(l0, (R(t, l, v), true) ' + h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

• Proof step 21:

  ((R(t, l, v), true) + persistDependentReads(l0, h)).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

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

Proof step 18 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Lemma persistDependentReads-otherread

Proof step 19 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  persistDependentReads(l, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

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); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ ¬ R(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 20 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l

Proof step 21 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  persistDependentReads(l0, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ ¬ R(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s)

Proof step 22 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 23 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  persistDependentReads(l0, (R(t, l, v), false) ' + h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ ¬ R(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 24 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  l0 = l, persistDependentReads(l0, (R(t, l, v), false) ' + h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

• Proof step 28:

  ((R(t, l, v), false) + persistDependentReads(l0, h)).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

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

Proof step 25 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Lemma persistDependentReads-otherread

Proof step 26 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  persistDependentReads(l, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

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); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ ¬ R(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 27 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l

Proof step 28 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  persistDependentReads(l0, h).filter(λ vpe. vpe._1.W?) ≠ h.filter(λ vpe. vpe._1.W?), l0 ≠ l, ∀ l1. persistDependentReads(l1, h).filter(λ vpe. vpe._1.W?) = h.filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ ¬ R(t, l, v).W?; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s)

Proof step 29 from proof persist-dependent-reads-unchanged-writes (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0