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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), p(l) = W(v, t) ' + fowl, abs(h, rs, p), ¬ abs(h.take(firstVolWrite(l, h)) + (W(t, l, v), true) ' + persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)), rs, p(l := fowl)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), p(l) = W(v, t) ' + fowl, abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ fowl;p(l0))) ⊦

Rule argument

Additional information

Used simplifier rules: abs-def-reduce: ⊦ abs(h, rs, p) → ( abs(h0, rs0, p0) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)) → absloc(events((h0 | l) | false), rs0(l), p0(l)))); a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ events(h1 + h2) = events(h1) + events(h2); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ W(t, l, v).l = l; (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ firstVolWrite(l, h) < # h → (∃ t, v. h = h.take(firstVolWrite(l, h)) + ((W(t, l, v), false) + h.drop(firstVolWrite(l, h) + 1)))

• Proof step 5:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), p(l) = W(v, t) ' + fowl, abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ fowl;p(l0))), firstVolWrite(l, h) < # h → (∃ t, v. h = h.take(firstVolWrite(l, h)) + ((W(t, l, v), false) + h.drop(firstVolWrite(l, h) + 1))) ⊦

Rule argument

Additional information

Used terms: l, h

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), h = h.take(firstVolWrite(l, h)) + (W(t0, l, v0), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) = W(v, t) ' + fowl, abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ fowl;p(l0))) ⊦

Rule argument

Additional information

Used simplifier rules: abs-leading-write-h-restricted-non-empty: ⊦ abs(h, rs, p) ∧ p(l) = W(v, t) ' + fowl → (h |W | l) | false ≠ []; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ firstVolWrite(l, h) < # h ↔ (h |W | l) | false ≠ []; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), h = h.take(firstVolWrite(l, h)) + (W(t0, l, v0), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) = W(v, t) ' + fowl, (h |W | l) | false ≠ [], abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ fowl;p(l0))) ⊦

Rule argument

Additional information

Used simplifier rules: abs-leading-write-h-restricted-non-empty: ⊦ abs(h, rs, p) ∧ p(l) = W(v, t) ' + fowl → (h |W | l) | false ≠ []; a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: (h |W | l) | false ≠ []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), h = h.take(firstVolWrite(l, h)) + (W(t0, l, v0), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) = W(v, t) ' + fowl, (h |W | l) | false ≠ [], abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ fowl;p(l0))) ⊦

Rule argument

Additional information

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

User applied rule subst equation

And obtained the following new goals

• Proof step 9:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), h = h.take(firstVolWrite(l, h)) + (W(t0, l, v0), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) = W(v, t) ' + fowl, (h |W | l) | false ≠ [], abs(h, rs, p), absloc(events((h.take(firstVolWrite(l, h)) + (W(t0, l, v0), false) ' + h.drop(firstVolWrite(l, h) + 1) | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ fowl;p(l0))) ⊦

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  h[firstVolWrite(l, h)] = (W(t, l, v), false), h = h.take(firstVolWrite(l, h)) + (W(t0, l, v0), false) ' + h.drop(firstVolWrite(l, h) + 1), l = l0, p(l) = W(v, t) ' + fowl, (h |W | l) | false ≠ [], abs(h, rs, p), absloc(events((h.take(firstVolWrite(l, h)) + (W(t0, l, v0), false) ' + h.drop(firstVolWrite(l, h) + 1) | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ fowl;p(l0))) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h[firstVolWrite(l0, h)] = (W(t, l0, v), false), h = h.take(firstVolWrite(l0, h)) + (W(t0, l0, v0), false) ' + h.drop(firstVolWrite(l0, h) + 1), p(l0) = W(v, t) ' + fowl, (h |W | l0) | false ≠ [], abs(h, rs, p), absloc(events((h.take(firstVolWrite(l0, h)) | l0) | false) + W(t0, l0, v0) ' + events((h.drop(firstVolWrite(l0, h) + 1) | l0) | false), rs(l0), p(l0)), W(v, t) ∈ p(l0), ¬ absloc (events((h.take(firstVolWrite(l0, h)) | l0) | false) + events((persistDependentReads(l0, h.drop(firstVolWrite(l0, h) + 1)) | l0) | false), rs(l0), fowl) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ [] + x = x; (s) ⊦ events([]) = []; (s) ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) ⊦ events(vpe ') = vpe._1 '; (s) ⊦ events(h1 + h2) = events(h1) + events(h2); (s) ⊦ (e, false) ' + h | false = (e, false) ' + (h | false); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ (W(t, l, v), b) ' + h | l = (W(t, l, v), b) ' + (h | l); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ((h.take(firstVolWrite(l, h)))|W | l) | false = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v0, fowl, l0, t, h.drop(firstVolWrite(l0, h) + 1), h.take(firstVolWrite(l0, h)), t0, rs(l0), v

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

Lemma absloc-persistWrite