Proof step 1 from proof persistDependentReads-restrict-single-W (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ((h | l) | t) | false = (W(t0, l0, v0), b) ', ((persistDependentReads(l, h) | l) | t) | false ≠ (W(t0, l0, v0), b) ' ⊦

Rule argument

Additional information

Proof step 2 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b) ', persistDependentReads(l, h).filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b) ' ⊦

Rule argument

Additional information

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

Proof step 3 from proof persistDependentReads-restrict-single-W (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.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b) ', [] = h, persistDependentReads(l, h).filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b) ' ⊦

• Proof step 6:

  ∀ h1, l, t, t0, l0, v0, b. ¬ ( h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b) ' ∧ persistDependentReads(l, h1).filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b) ') ⊦ ∀ h1, l0, t0, t1, l1, v0, b. ¬ ( (W(t, l, v), true) ' + h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ' ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ')

• Proof step 10:

  ∀ h1, l, t, t0, l0, v0, b. ¬ ( h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b) ' ∧ persistDependentReads(l, h1).filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b) ') ⊦ ∀ h1, l0, t0, t1, l1, v0, b. ¬ ( (W(t, l, v), false) ' + h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ' ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ')

• Proof step 14:

  ∀ h1, l, t, t0, l0, v0, b. ¬ ( h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b) ' ∧ persistDependentReads(l, h1).filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b) ') ⊦ ∀ h1, l0, t0, t1, l1, v0, b. ¬ ( (R(t, l, v), true) ' + h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ' ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ')

• Proof step 24:

  ∀ h1, l, t, t0, l0, v0, b. ¬ ( h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b) ' ∧ persistDependentReads(l, h1).filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b) ') ⊦ ∀ h1, l0, t0, t1, l1, v0, b. ¬ ( (R(t, l, v), false) ' + h = h1 ∧ h1.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ' ∧ persistDependentReads(l0, h1).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ')

Rule argument

Additional information

Used terms: h, λ h0. ∀ h, l, t, t0, l0, v0, b. ¬ ( h0 = h ∧ h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b) ' ∧ persistDependentReads(l, h).filter(λ vpe. vpe._1.l = l) .filter (λ vpe. vpe._1.t = t ) .filter (λ vpe. ¬ vpe._2 ) ≠ (W(t0, l0, v0), b) ')

Proof step 4 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Lemma hist-ind

Proof step 5 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ [].filter(p) = []; (s)

Proof step 6 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (l = l0 ⊃ (W(t, l0, v), true) ';[]).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (W(t, l, v), true) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 7 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  [].filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (W(t, l, v), true) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 8 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

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) ⊦ [].filter(p) = []; (s)

Proof step 9 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0, t1, l1, v0, b

Proof step 10 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (l = l0 ⊃ (W(t, l0, v), false) ';[]).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (W(t, l, v), false) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 11 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 12:

  [].filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (W(t, l, v), false) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 12 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

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) ⊦ [].filter(p) = []; (s)

Proof step 13 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0, t1, l1, v0, b

Proof step 14 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (l = l0 ⊃ (R(t, l0, v), true) ';[]).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (R(t, l, v), true) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 15 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 16:

  (R(t, l0, v), true) '.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', l = l0, persistDependentReads(l0, (R(t, l, v), true) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

• Proof step 22:

  [].filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (R(t, l, v), true) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

Proof step 16 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  (t = t0 ⊃ (R(t0, l0, v), true) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', (t = t0 ⊃ (R(t0, l0, v), true) ';[]).filter(λ vpe. ¬ vpe._2) + persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

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

Proof step 17 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 18:

  (R(t0, l0, v), true) '.filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', t = t0, (t = t0 ⊃ (R(t0, l0, v), true) ';[]).filter(λ vpe. ¬ vpe._2) + persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

• Proof step 20:

  [].filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', (t = t0 ⊃ (R(t0, l0, v), true) ';[]).filter(λ vpe. ¬ vpe._2) + persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', t ≠ t0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

Proof step 18 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 19 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0, t1, l1, v0, b

Proof step 20 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', t ≠ t0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 21 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0, t1, l1, v0, b

Proof step 22 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

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) ⊦ [].filter(p) = []; (s)

Proof step 23 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0, t1, l1, v0, b

Proof step 24 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  (l = l0 ⊃ (R(t, l0, v), false) ';[]).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (R(t, l, v), false) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 25 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 26:

  (R(t, l0, v), false) '.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', l = l0, persistDependentReads(l0, (R(t, l, v), false) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

• Proof step 30:

  [].filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, (R(t, l, v), false) ' + h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

Proof step 26 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  (t = t0 ⊃ (R(t0, l0, v), false) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', (t = t0 ⊃ (R(t0, l0, v), true) ';[]).filter(λ vpe. ¬ vpe._2) + persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

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

Proof step 27 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 28:

  (t = t0 ⊃ (R(t0, l0, v), false) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', (t = t0 ⊃ (R(t0, l0, v), true) ';[]).filter(λ vpe. ¬ vpe._2) + persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', t ≠ t0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ R(t, l, v) ≠ W(t0, l0, v0); (s) Used formulas: t = t0

Proof step 28 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', t ≠ t0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

Rule argument

Additional information

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

Proof step 29 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0, t1, l1, v0, b

Proof step 30 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  h.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t1, l1, v0), b) ', persistDependentReads(l0, h).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t1, l1, v0), b) ', l ≠ l0, ∀ l2, t2, t3, l3, v1, b0. h.filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) ≠ (W(t3, l3, v1), b0) ' ∨ persistDependentReads(l2, h).filter(λ vpe. vpe._1.l = l2).filter(λ vpe. vpe._1.t = t2).filter(λ vpe. ¬ vpe._2) = (W(t3, l3, v1), b0) ' ⊦

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) ⊦ [].filter(p) = []; (s)

Proof step 31 from proof persistDependentReads-restrict-single-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0, t1, l1, v0, b