Proof step 1 from proof persistDependentReads-restrict-same-loc (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  persistDependentReads(l, h) | l ≠ persistDependentReads(l, h | l) ⊦

Rule argument

Additional information

Proof step 2 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  persistDependentReads(l, h).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, h.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

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

Proof step 3 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  persistDependentReads(l, vpe + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, (vpe + h0).filter(λ vpe. vpe._1.l = l)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  persistDependentReads(l, vpe ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, (vpe._1.l = l ⊃ vpe ';[]) + h0.filter(λ vpe. vpe._1.l = l)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

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 5 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  vpe = (e, boolvar), persistDependentReads(l, vpe ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, (e.l = l ⊃ vpe ';[]) + h0.filter(λ vpe. vpe._1.l = l)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 6 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  persistDependentReads(l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, (e.l = l ⊃ (e, boolvar) ';[]) + h0.filter(λ vpe. vpe._1.l = l)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

Proof step 7 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  e.l = l, persistDependentReads(l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, (e, boolvar) ' + h0.filter(λ vpe. vpe._1.l = l)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

• Proof step 12:

  persistDependentReads(l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, [] + h0.filter(λ vpe. vpe._1.l = l)), e.l ≠ l, ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

Proof step 8 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  persistDependentReads(e.l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = e.l) ≠ persistDependentReads(e.l, (e, boolvar) ' + h0.filter(λ vpe. vpe._1.l = e.l)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

Proof step 9 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  e = R(t, l0, v), persistDependentReads(e.l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = e.l) ≠ persistDependentReads(e.l, (e, boolvar) ' + h0.filter(λ vpe. vpe._1.l = e.l)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

Used simplifier rules: persistDependentReads-nextwrite: ⊦ persistDependentReads(l, (W(t, l, v), b) ' + h) = (W(t, l, v), b) ' + h; RWevent freely generated by R, W;; ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ W(t, l, v).l = l; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 10 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  persistDependentReads(l0, h0).filter(λ vpe. vpe._1.l = l0) ≠ persistDependentReads(l0, h0.filter(λ vpe. vpe._1.l = l0)), ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

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 = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ R(t, l, v).l = l; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 11 from proof persistDependentReads-restrict-same-loc (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 12 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  persistDependentReads(l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)), e.l ≠ l, ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

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

Proof step 13 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 14:

  e = R(t, l0, v), persistDependentReads(l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)), e.l ≠ l, ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

• Proof step 16:

  e = W(t, l0, v), persistDependentReads(l, (e, boolvar) ' + h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)), e.l ≠ l, ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

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

Proof step 14 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)), l0 ≠ l, ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

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

Proof step 15 from proof persistDependentReads-restrict-same-loc (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 16 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) ≠ persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)), l0 ≠ l, ∀ l. persistDependentReads(l, h0).filter(λ vpe. vpe._1.l = l) = persistDependentReads(l, h0.filter(λ vpe. vpe._1.l = l)) ⊦

Rule argument

Additional information

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

Proof step 17 from proof persistDependentReads-restrict-same-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l