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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  h[firstVolWrite(l, h)] = (e, bv), firstPersistW(p(l)) < # p(l), abs(h, rs, p), ¬ abs(h.take(firstVolWrite(l, h)) + (e, true) ' + persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)), rs, p(l := p(l) -p firstPersistW(p(l)))) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h[firstVolWrite(l, h)] = (e, bv), p(l) ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p), ¬ abs(h.take(firstVolWrite(l, h)) + (e, true) ' + persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)), rs, p(l := p(l) -p firstPersistW(p(l)))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 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))))

• Proof step 5:

  h[firstVolWrite(l, h)] = (e, bv), p(l) ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p), ∃ l0. ¬ ( absloc(events((h | l0) | false), rs(l0), p(l0)) → absloc (events((h.take(firstVolWrite(l, h)) + (e, true) ' + persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), p(l := p(l) -p firstPersistW(p(l)))(l0))) ⊦

Rule argument

Additional information

Used terms: p(l := p(l) -p firstPersistW(p(l))), rs, h.take(firstVolWrite(l, h)) + (e, true) ' + persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)), rs, p, h

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

Lemma abs-def-reduce

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  h[firstVolWrite(l, h)] = (e, bv), p(l) ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))) ⊦

Rule argument

Additional information

Used simplifier rules: abs-firstPersistW-firstVolWrite-correct-loc: ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) ∧ h[firstVolWrite(l, h)] = (e, bv) → e.l = l; 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 abs-persist-firstPersistW (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  ⊦ 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 8:

  h[firstVolWrite(l, h)] = (e, bv), p(l) ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));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 7 from proof abs-persist-firstPersistW (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h[firstVolWrite(l, h)] = (e, bv), h = h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))) ⊦

Rule argument

Additional information

Used simplifier rules: abs-firstPersistW-is-in-hist: ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) → (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 9 from proof abs-persist-firstPersistW (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  h[firstVolWrite(l, h)] = (e, bv), h = h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) ≠ [], (h |W | l) | false ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))) ⊦

Rule argument

Additional information

Used simplifier rules: abs-firstPersistW-is-in-hist: ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) → (h |W | l) | false ≠ []; Used formulas: (h |W | l) | false ≠ []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h[firstVolWrite(l, h)] = (e, bv), h = h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) ≠ [], (h |W | l) | false ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p), absloc(events((h | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ abs(h, rs, p) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)))

• Proof step 13:

  h[firstVolWrite(l, h)] = (e, bv), h = h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) ≠ [], (h |W | l) | false ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))), ∀ l. absloc(events((h | l) | false), rs(l), p(l)) ⊦

Rule argument

Additional information

Used terms: h, rs, p

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

Lemma abs-def

Proof step 13 from proof abs-persist-firstPersistW (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  h[firstVolWrite(l, h)] = (e, bv), h = h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) ≠ [], (h |W | l) | false ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))) ⊦

Rule argument

Additional information

Used terms: l0

Proof step 14 from proof abs-persist-firstPersistW (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 15:

  h[firstVolWrite(l, h)] = (e, bv), h = h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) ≠ [], (h |W | l) | false ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1) | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))) ⊦

Rule argument

Additional information

Proof step 15 from proof abs-persist-firstPersistW (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  h[firstVolWrite(l, h)] = (e, bv), h = h.take(firstVolWrite(l, h)) + (W(t, l, v), false) ' + h.drop(firstVolWrite(l, h) + 1), p(l) ≠ [], (h |W | l) | false ≠ [], firstPersistW(p(l)) < # p(l), absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (W(t, l0, v), false) ';[]) | false) + events((h.drop(firstVolWrite(l, h) + 1) | l0) | false), rs(l0), p(l0)), ¬ absloc ( events((h.take(firstVolWrite(l, h)) | l0) | false) + events((l = l0 ⊃ (e, true) ';[]) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l0) | false), rs(l0), (l = l0 ⊃ p(l0) -p firstPersistW(p(l0));p(l0))) ⊦

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) ⊦ 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 16 from proof abs-persist-firstPersistW (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: absloc-persist-firstPersistW: ⊦ absloc ( events((h.take(firstVolWrite(l, h)) | l) | false) + W(t, l, v) ' + events((h.drop(firstVolWrite(l, h) + 1) | l) | false), rset, fowl) ∧ firstPersistW(fowl) < # fowl → absloc ( events((h.take(firstVolWrite(l, h)) | l) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)); ⊦ [] | 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 ⊦ events(vpe ') = vpe._1 '; (s) ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic