Proof step 1 from proof absloc-persistWrite (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h0 |W | l) | false = [], absloc(events((h0 | l) | false) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((h0 | l) | false) + events((persistDependentReads(l, h1) | l) | false), rset, fowl) ⊦

Rule argument

Additional information

Proof step 2 from proof absloc-persistWrite (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ([] |W | l) | false = [], absloc(events(([] | l) | false) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events(([] | l) | false) + events((persistDependentReads(l, h1) | l) | false), rset, fowl) ⊦

• Proof step 23:

  ((vpe + h)|W | l) | false = [], absloc(events((vpe + h | l) | false) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((vpe + h | l) | false) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ∀ l, t, v, h1, rset, v0, t0, fowl. ¬ ( (h |W | l) | false = [] ∧ absloc(events((h | l) | false) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl) ∧ ¬ absloc(events((h | l) | false) + events((persistDependentReads(l, h1) | l) | false), rset, fowl)) ⊦

Rule argument

Additional information

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

Proof step 3 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  absloc(events((h1 | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h1) | l) | false), rset, fowl) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recW-W: ⊦ absloc(W(t, l, v) ' + el, rset, W(v0, t0) ' + fowl) ↔ t0 = t ∧ v0 = v ∧ absloc(el, rset, fowl); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ events([]) = []; (s) ⊦ [] | b = []; (s) ⊦ [] | l = []; (s) ⊦ [] |W = []; (s)

Proof step 4 from proof absloc-persistWrite (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  absloc(events((vpe + h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, vpe + h) | l) | false), rset, fowl), ∀ l, rset, fowl. ¬(absloc(events((h | l) | false), rset, fowl) ∧ ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl)) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-base: ⊦ absloc([], rset, fowl) ↔ fowl |W = []; List('a) freely generated by [], +;; ⊦ persistDependentReads(l, []) = []; (s) ⊦ [] | l = []; (s) ⊦ [] | b = []; (s) ⊦ events([]) = []; (s)

Proof step 5 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  absloc(events((vpe._1.l = l ⊃ vpe ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, vpe ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ events(h1 + h2) = events(h1) + events(h2); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s)

Proof step 6 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  vpe = (e, boolvar), absloc(events((e.l = l ⊃ vpe ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, vpe ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 7 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (e, boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Proof step 8 from proof absloc-persistWrite (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  e = R(t, l1, v), absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (e, boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

• Proof step 19:

  e = W(t, l1, v), absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (e, boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

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

Proof step 9 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  absloc(events((l1 = l ⊃ (R(t, l, v), boolvar) ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (R(t, l1, v), boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ R(t, l, v).l = l; (s)

Proof step 10 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 11:

  l1 = l, absloc(events((R(t, l, v), boolvar) ' | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (R(t, l1, v), boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

• Proof step 17:

  l1 ≠ l, absloc(events([] | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (R(t, l1, v), boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Proof step 11 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  absloc(events((¬ boolvar ⊃ (R(t, l, v), false) ';[])) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (e, true) ' + h | false = h | false; (s) ⊦ (R(t, l, v), b) ' + h | l = (R(t, l, v), b) ' + (h | l); (s) ⊦ persistDependentReads(l, (R(t, l, v), b) ' + h) = (R(t, l, v), true) ' + persistDependentReads(l, h); (s) ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s)

Proof step 12 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 13:

  ¬ boolvar, absloc(events((R(t, l, v), false) ') + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

• Proof step 15:

  boolvar, absloc(events([]) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Proof step 13 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  absloc(events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl), ¬ t ∈ rset → FO(t) ∈ fowl, ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recR: ⊦ absloc(R(t, l, v) ' + el, rset, fowl) ↔ (¬ t ∈ rset → FO(t) ∈ fowl) ∧ absloc(el, rset, fowl); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ events(vpe ') = vpe._1 '; (s)

Proof step 14 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, rset, fowl

Proof step 15 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  absloc(events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

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

Proof step 16 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, rset, fowl

Proof step 17 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  l1 ≠ l, absloc(events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

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

Proof step 18 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, rset, fowl

Proof step 19 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  absloc(events((l1 = l ⊃ (W(t, l, v), boolvar) ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (W(t, l1, v), boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s)

Proof step 20 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 21:

  l1 ≠ l, absloc(events((l1 = l ⊃ (W(t, l, v), boolvar) ';[]) | false) + events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, (W(t, l1, v), boolvar) ' + h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ persistDependentReads(l, (W(t, l, v), b) ' + h) = (W(t, l, v), b) ' + h; (s) ⊦ (W(t, l, v), b) ' + h | l = (W(t, l, v), b) ' + (h | l); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) ⊦ events(h1 + h2) = events(h1) + events(h2); (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: l1 = l

Proof step 21 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  l1 ≠ l, absloc(events((h | l) | false), rset, fowl), ¬ absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl), ∀ l0, rset0, fowl0. ¬ absloc(events((h | l0) | false), rset0, fowl0) ∨ absloc(events((persistDependentReads(l0, h) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

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

Proof step 22 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, rset, fowl

Proof step 23 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  ((vpe._1.W? ⊃ vpe ';[]) | l) | false = [], (h |W | l) | false = [], absloc((events((vpe._1.l = l ⊃ vpe ';[]) | false) + events((h | l) | false)) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc((events((vpe._1.l = l ⊃ vpe ';[]) | false) + events((h | l) | false)) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ events(h1 + h2) = events(h1) + events(h2); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ a + x = a ' + x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ vpe ' |W = (vpe._1.W? ⊃ vpe ';[]); (s) ⊦ (h + h0)|W = h |W + h0 |W; (s)

Proof step 24 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 25:

  vpe = (e, boolvar), (h |W | l) | false = [], ((e.W? ⊃ vpe ';[]) | l) | false = [], absloc((events((e.l = l ⊃ vpe ';[]) | false) + events((h | l) | false)) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc((events((e.l = l ⊃ vpe ';[]) | false) + events((h | l) | false)) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 25 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ((e.W? ⊃ (e, boolvar) ';[]) | l) | false = [], (h |W | l) | false = [], absloc((events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h | l) | false)) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc((events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h | l) | false)) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Proof step 26 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 27:

  e.l = l, (h |W | l) | false = [], ((e.W? ⊃ (e, boolvar) ';[]) | l) | false = [], absloc((events((e, boolvar) ' | false) + events((h | l) | false)) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc((events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h | l) | false)) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

• Proof step 37:

  (h |W | l) | false = [], ((e.W? ⊃ (e, boolvar) ';[]) | l) | false = [], e.l ≠ l, absloc((events([] | false) + events((h | l) | false)) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc((events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h | l) | false)) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Proof step 27 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ((e.W? ⊃ (e, boolvar) ';[]) | e.l) | false = [], (h |W | e.l) | false = [], absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s)

Proof step 28 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 29:

  ¬ boolvar, (h |W | e.l) | false = [], ((e.W? ⊃ (e, boolvar) ';[]) | e.l) | false = [], absloc(events((e, false) ') + events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

• Proof step 35:

  boolvar, (h |W | e.l) | false = [], ((e.W? ⊃ (e, boolvar) ';[]) | e.l) | false = [], absloc(events([]) + events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Proof step 29 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  ((e.W? ⊃ (e, false) ';[]) | e.l) | false = [], (h |W | e.l) | false = [], absloc(e ' + events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(e ' + events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

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

Proof step 30 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 31:

  (h |W | e.l) | false = [], ((e.W? ⊃ (e, false) ';[]) | e.l) | false = [], absloc(e ' + events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ e.W?, ¬ absloc(e ' + events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) ⊦ a ' ≠ []; (s) Used formulas: e.W?

Proof step 31 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  (h |W | e.l) | false = [], absloc(e ' + events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ e.W?, ¬ absloc(e ' + events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] | b = []; (s) ⊦ [] | l = []; (s)

Proof step 32 from proof absloc-persistWrite (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 33:

  e = R(t3, l, v3), (h |W | e.l) | false = [], absloc(e ' + events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ e.W?, ¬ absloc(e ' + events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recW-W: ⊦ absloc(W(t, l, v) ' + el, rset, W(v0, t0) ' + fowl) ↔ t0 = t ∧ v0 = v ∧ absloc(el, rset, fowl); RWevent freely generated by R, W;; ⊦ W(t, l, v).l = l; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(t, l, v).W?; (s)

Proof step 33 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  (h |W | l) | false = [], absloc(events((h | l) | false) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((h | l) | false) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ¬ t3 ∈ rset → FO(t3) ∈ fowl, ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recR: ⊦ absloc(R(t, l, v) ' + el, rset, fowl) ↔ (¬ t ∈ rset → FO(t) ∈ fowl) ∧ absloc(el, rset, fowl); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ R(t, l, v).l = l; (s) ⊦ ¬ R(t, l, v).W?; (s) ⊦ FO(tid) ≠ W(v, tid0); (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s)

Proof step 34 from proof absloc-persistWrite (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: l, t, v, h1, rset, v0, t0, fowl

Proof step 35 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  ((e.W? ⊃ (e, true) ';[]) | e.l) | false = [], (h |W | e.l) | false = [], absloc(events((h | e.l) | false) + W(t, e.l, v) ' + events((h1 | e.l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((h | e.l) | false) + events((persistDependentReads(e.l, h1) | e.l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

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

Proof step 36 from proof absloc-persistWrite (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: e.l, t, v, h1, rset, v0, t0, fowl

Proof step 37 from proof absloc-persistWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  ((e.W? ⊃ (e, boolvar) ';[]) | l) | false = [], (h |W | l) | false = [], e.l ≠ l, absloc(events((h | l) | false) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl), ¬ absloc(events((h | l) | false) + events((persistDependentReads(l, h1) | l) | false), rset, fowl), ∀ l0, t1, v1, h0, rset0, v2, t2, fowl0. (h |W | l0) | false ≠ [] ∨ ¬ absloc(events((h | l0) | false) + W(t1, l0, v1) ' + events((h0 | l0) | false), rset0, W(v2, t2) ' + fowl0) ∨ absloc(events((h | l0) | false) + events((persistDependentReads(l0, h0) | l0) | false), rset0, fowl0) ⊦

Rule argument

Additional information

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

Proof step 38 from proof absloc-persistWrite (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: l, t, v, h1, rset, v0, t0, fowl