Proof step 1 from proof abs-loc-no-w-last-firstfo-then-no-pending (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fowl |W | t = [], ((h | l) | t) | false ≠ [], absloc(events((h | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, h), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl ⊦

Rule argument

Additional information

Proof step 2 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  fowl |W | t = [], ((vpe + h0 | l) | t) | false ≠ [], absloc(events((vpe + h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, vpe + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl, t, l, rset, mem, persisted. ¬ ( fowl |W | t = [] ∧ ((h0 | l) | t) | false ≠ [] ∧ absloc(events((h0 | l) | false), rset, FO(t) ' + fowl) ∧ allReadsOKInd(mem, persisted, h0) ∧ persisted(l) ∧ ¬ t ∈ rset ∧ ¬ FO(t) ∈ fowl) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ [] | l = []; (s) ⊦ [] | t = []; (s) ⊦ [] | b = []; (s)

Proof step 3 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  fowl |W | t = [], absloc(events((vpe._1.l = l ⊃ vpe ';[]) | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, vpe ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦ ((vpe._1.l = l ⊃ vpe ';[]) | t) | false = [] ∧ ((h0 | l) | t) | false = []

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) ⊦ h + h0 | t = (h | t) + (h0 | t); (s)

Proof step 4 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 5:

  vpe = (e, boolvar), fowl |W | t = [], absloc(events((e.l = l ⊃ vpe ';[]) | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, vpe ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦ ((e.l = l ⊃ vpe ';[]) | t) | false = [] ∧ ((h0 | l) | t) | false = []

Rule argument

Additional information

Used terms: e, boolvar

Proof step 5 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  fowl |W | t = [], absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦ ((e.l = l ⊃ (e, boolvar) ';[]) | t) | false = [] ∧ ((h0 | l) | t) | false = []

Rule argument

Additional information

Proof step 6 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 7:

  fowl |W | t = [], ((e.l = l ⊃ (e, boolvar) ';[]) | t) | false ≠ [], absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

• Proof step 12:

  fowl |W | t = [], ((h0 | l) | t) | false ≠ [], absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Proof step 7 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  e.l = l, fowl |W | t = [], ((e.l = l ⊃ (e, boolvar) ';[]) | t) | false ≠ [], absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) ⊦ [] | b = []; (s) Used formulas: e.l = l

Proof step 8 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  fowl |W | t = [], (t = e.t ⊃ (e, boolvar) ';[]) | false ≠ [], absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) ⊦ (e, b) ' | t = (t = e.t ⊃ (e, b) ';[]); (s)

Proof step 9 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  t = e.t, fowl |W | t = [], (t = e.t ⊃ (e, boolvar) ';[]) | false ≠ [], absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] | b = []; (s) Used formulas: t = e.t

Proof step 10 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  fowl |W | e.t = [], absloc(e ' + events((h0 | e.l) | false), rset, FO(e.t) ' + fowl), allReadsOKInd(mem, persisted, (e, false) ' + h0), persisted(e.l), ¬ FO(e.t) ∈ fowl, ¬ e.t ∈ rset, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

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

Proof step 11 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: absloc-recW-FO: ⊦ absloc(W(t, l, v) ' + el, rset, FO(t0) ' + fowl) ↔ absloc(W(t, l, v) ' + el, rset, fowl); absloc-no-W-leading-W: ⊦ fowl |W | t = [] → ¬ absloc(W(t, l, v) ' + el, rset, fowl); RWevent freely generated by R, W;; ⊦ allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h); (s) ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).t = t; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ R(t, l, v).t = t; (s) ⊦ R(t, l, v).l = l; (s) ⊦ allReadsOKInd(mem, persisted, (R(t, l, v), b) ' + h) ↔ v = mem(l) ∧ (b ↔ persisted(l)) ∧ allReadsOKInd(mem, persisted, h); (s)

Proof step 12 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 13:

  e.l = l, fowl |W | t = [], ((h0 | l) | t) | false ≠ [], absloc(events((e, boolvar) ' | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

• Proof step 29:

  fowl |W | t = [], e.l ≠ l, ((h0 | l) | t) | false ≠ [], absloc(events([] | false) + events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Proof step 13 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s)

Proof step 14 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 15:

  ¬ boolvar, fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(events((e, false) ') + events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

• Proof step 23:

  boolvar, fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(events([]) + events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Proof step 15 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(e ' + events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, false) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ events(vpe ') = vpe._1 '; (s)

Proof step 16 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 17:

  e = W(t1, l, v), fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(e ' + events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, false) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: RWevent freely generated by R, W;; ⊦ R(t, l, v).l = l; (s) ⊦ allReadsOKInd(mem, persisted, (R(t, l, v), b) ' + h) ↔ v = mem(l) ∧ (b ↔ persisted(l)) ∧ allReadsOKInd(mem, persisted, h); (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 17 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  fowl |W | t = [], ((h0 | l) | t) | false ≠ [], absloc(W(t1, l, v) ' + events((h0 | l) | false), rset, fowl), allReadsOKInd(mem(l := v), persisted(l := false), h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recW-FO: ⊦ absloc(W(t, l, v) ' + el, rset, FO(t0) ' + fowl) ↔ absloc(W(t, l, v) ' + el, rset, fowl); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(t, l, v).l = l; (s) ⊦ allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h); (s)

Proof step 18 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 19:

  (fow + fowl0)|W | t = [], ((h0 | l) | t) | false ≠ [], absloc(W(t1, l, v) ' + events((h0 | l) | false), rset, fow + fowl0), allReadsOKInd(mem(l := v), persisted(l := false), h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fow + fowl0, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0, ∀ t, h0, l, t1, v, rset, mem, persisted. ¬ ( fowl0 |W | t = [] ∧ ((h0 | l) | t) | false ≠ [] ∧ absloc(W(t1, l, v) ' + events((h0 | l) | false), rset, fowl0) ∧ allReadsOKInd(mem(l := v), persisted(l := false), h0) ∧ persisted(l) ∧ ¬ t ∈ rset ∧ ¬ FO(t) ∈ fowl0 ∧ (∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recW-empty: ⊦ ¬ absloc(W(t, l, v) ' + el, rset, []); List('a) freely generated by [], +;; ⊦ [] |W = []; (s) ⊦ [] | t = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 19 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  fow ' |W | t = [], fowl0 |W | t = [], FO(t) ≠ fow, ((h0 | l) | t) | false ≠ [], absloc(W(t1, l, v) ' + events((h0 | l) | false), rset, fow ' + fowl0), allReadsOKInd(mem(l := v), persisted(l := false), h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl0, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0, ∀ t0, h, l0, t2, v0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h | l0) | t0) | false = [] ∨ ¬ absloc(W(t2, l0, v0) ' + events((h | l0) | false), rset0, fowl0) ∨ ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ∨ ¬ (∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h | l0) | t0) | false = [] ∨ ¬ absloc(events((h | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s)

Proof step 20 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 21:

  fow = FO(t3), fowl0 |W | t = [], fow ' |W | t = [], FO(t) ≠ fow, ((h0 | l) | t) | false ≠ [], absloc(W(t1, l, v) ' + events((h0 | l) | false), rset, fow ' + fowl0), allReadsOKInd(mem(l := v), persisted(l := false), h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl0, ∀ t0, h, l0, t2, v0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h | l0) | t0) | false = [] ∨ ¬ absloc(W(t2, l0, v0) ' + events((h | l0) | false), rset0, fowl0) ∨ ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ∨ ¬ (∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h | l0) | t0) | false = [] ∨ ¬ absloc(events((h | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0), ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ 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); abs-loc-no-w-no-fo-then-no-pending: ⊦ absloc(events((h | l) | false), rset, fowl) ∧ fowl |W | t = [] ∧ ¬ FO(t) ∈ fowl ∧ ¬ t ∈ rset → ((h | l) | t) | false = []; FOW freely generated by FO, W;; ⊦ W(v, t) ' |W = W(v, t) '; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ W(v, tid).tid = tid; (s) ⊦ a ' ≠ []; (s) ⊦ FO(tid) ≠ W(v, tid0); (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 21 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  fowl0 |W | t = [], t ≠ t3, ((h0 | l) | t) | false ≠ [], absloc(W(t1, l, v) ' + events((h0 | l) | false), rset, fowl0), allReadsOKInd(mem(l := v), persisted(l := false), h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl0, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0, ∀ t0, h, l0, t2, v0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h | l0) | t0) | false = [] ∨ ¬ absloc(W(t2, l0, v0) ' + events((h | l0) | false), rset0, fowl0) ∨ ¬ allReadsOKInd(mem0(l0 := v0), persisted0(l0 := false), h) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ∨ ¬ (∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h | l0) | t0) | false = [] ∨ ¬ absloc(events((h | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0) ⊦

Rule argument

Additional information

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

Proof step 22 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, h0, l, t1, v, rset, mem, persisted

Proof step 23 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, true) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ 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 24 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 25:

  e = R(t1, l, v), fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, true) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

• Proof step 27:

  e = W(t1, l, v), fowl |W | t = [], ((h0 | e.l) | t) | false ≠ [], absloc(events((h0 | e.l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, true) ' + h0), persisted(e.l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

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

Proof step 25 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  fowl |W | t = [], ((h0 | l) | t) | false ≠ [], absloc(events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, h0), persisted(l), ¬ FO(t) ∈ fowl, ¬ t ∈ rset, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ R(t, l, v).l = l; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ allReadsOKInd(mem, persisted, (R(t, l, v), b) ' + h) ↔ v = mem(l) ∧ (b ↔ persisted(l)) ∧ allReadsOKInd(mem, persisted, h); (s)

Proof step 26 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fowl, t, l, rset, mem, persisted

Proof step 27 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  fowl |W | t = [], ((h0 | l) | t) | false ≠ [], absloc(events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem(l := v), persisted(l := true), h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h); (s)

Proof step 28 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fowl, t, l, rset, mem(l := v), persisted(l := true)

Proof step 29 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  fowl |W | t = [], e.l ≠ l, ((h0 | l) | t) | false ≠ [], absloc(events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ 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 30 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 31:

  e = R(t1, l1, v), fowl |W | t = [], e.l ≠ l, ((h0 | l) | t) | false ≠ [], absloc(events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

• Proof step 33:

  e = W(t1, l1, v), fowl |W | t = [], e.l ≠ l, ((h0 | l) | t) | false ≠ [], absloc(events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

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

Proof step 31 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  fowl |W | t = [], l1 ≠ l, ((h0 | l) | t) | false ≠ [], absloc(events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem, persisted, h0), persisted(l), ¬ FO(t) ∈ fowl, ¬ t ∈ rset, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ allReadsOKInd(mem, persisted, (R(t, l, v), b) ' + h) ↔ v = mem(l) ∧ (b ↔ persisted(l)) ∧ allReadsOKInd(mem, persisted, h); (s) ⊦ R(t, l, v).l = l; (s)

Proof step 32 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fowl, t, l, rset, mem, persisted

Proof step 33 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  fowl |W | t = [], l1 ≠ l, ((h0 | l) | t) | false ≠ [], absloc(events((h0 | l) | false), rset, FO(t) ' + fowl), allReadsOKInd(mem(l1 := v), persisted(l1 := boolvar), h0), persisted(l), ¬ t ∈ rset, ¬ FO(t) ∈ fowl, ∀ fowl0, t0, l0, rset0, mem0, persisted0. fowl0 |W | t0 ≠ [] ∨ ((h0 | l0) | t0) | false = [] ∨ ¬ absloc(events((h0 | l0) | false), rset0, FO(t0) ' + fowl0) ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ∨ t0 ∈ rset0 ∨ FO(t0) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h); (s) ⊦ W(t, l, v).l = l; (s)

Proof step 34 from proof abs-loc-no-w-last-firstfo-then-no-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fowl, t, l, rset, mem(l1 := v), persisted(l1 := boolvar)