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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  firstPersistW(fowl) < # fowl, absloc(events((h.take(firstVolWrite(l, h)) | l) | false) + W(t, l, v) ' + events((h.drop(firstVolWrite(l, h) + 1) | l) | false), rset, 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)) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  firstPersistW(fowl) < # fowl, absloc(events(([].take(firstVolWrite(l, [])) | l) | false) + W(t, l, v) ' + events(([].drop(firstVolWrite(l, []) + 1) | l) | false), rset, fowl), ¬ absloc (events(([].take(firstVolWrite(l, [])) | l) | false) + events((persistDependentReads(l, [].drop(firstVolWrite(l, []) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)) ⊦

• Proof step 6:

  firstPersistW(fowl) < # fowl, absloc ( events(((vpe + h0).take(firstVolWrite(l, vpe + h0)) | l) | false) + W(t, l, v) ' + events(((vpe + h0).drop(firstVolWrite(l, vpe + h0) + 1) | l) | false), rset, fowl), ¬ absloc ( events(((vpe + h0).take(firstVolWrite(l, vpe + h0)) | l) | false) + events((persistDependentReads(l, (vpe + h0).drop(firstVolWrite(l, vpe + h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl, l, t, v, rset. ¬ ( firstPersistW(fowl) < # fowl ∧ absloc(events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl) ∧ ¬ absloc (events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl))) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc(events(([].take(firstVolWrite(l, [])) | l) | false) + W(t, l, v) ' + events(([].drop(firstVolWrite(l, []) + 1) | l) | false), rset, fowl), ¬ absloc (events(([].take(firstVolWrite(l, [])) | l) | false) + events((persistDependentReads(l, [].drop(firstVolWrite(l, []) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ firstVolWrite(l, h) = h.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)

Rule argument

Additional information

Used simplifier rules: absloc-persist-leading-firstPersistW: ⊦ absloc(W(t, l, v) ' + events((h | l) | false), rset, fowl) → absloc (events((persistDependentReads(l, h) | l) | false), rset, fowl -p firstPersistW(fowl)); ⊦ x.take(0) = []; (s) ⊦ [] | l = []; (s) ⊦ [] | b = []; (s) ⊦ events([]) = []; (s) ⊦ [].indexWhere(p) = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: l, []

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc (events(((vpe ' + h0).take(firstVolWrite(l, vpe ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, vpe ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events(((vpe ' + h0).take(firstVolWrite(l, vpe ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, vpe ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (a ' + x).drop(n + 1) = x.drop(n); (s) ⊦ a + x = a ' + x; (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  vpe = (e, b), fowl ≠ [], firstPersistW(fowl) < # fowl, absloc (events(((vpe ' + h0).take(firstVolWrite(l, vpe ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, vpe ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events(((vpe ' + h0).take(firstVolWrite(l, vpe ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, vpe ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((((e, b) ' + h0).take(firstVolWrite(l, (e, b) ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, (e, b) ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events((((e, b) ' + h0).take(firstVolWrite(l, (e, b) ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, (e, b) ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  e = R(t1, l1, v1), fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((((e, b) ' + h0).take(firstVolWrite(l, (e, b) ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, (e, b) ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events((((e, b) ' + h0).take(firstVolWrite(l, (e, b) ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, (e, b) ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

• Proof step 20:

  e = W(t1, l1, v1), fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((((e, b) ' + h0).take(firstVolWrite(l, (e, b) ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, (e, b) ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events((((e, b) ' + h0).take(firstVolWrite(l, (e, b) ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, (e, b) ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( (events((l1 = l ⊃ (R(t1, l, v1), b) ';[]) | false) + events((h0.take(firstVolWrite(l, h0)) | l) | false)) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc ( (events((l1 = l ⊃ (R(t1, l, v1), b) ';[]) | false) + events((h0.take(firstVolWrite(l, h0)) | l) | false)) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ firstVolWrite(l, (R(t, l0, v), b) ' + h) = firstVolWrite(l, h) + 1; (s) ⊦ events(h1 + h2) = events(h1) + events(h2); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ R(t, l, v).l = l; (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 12:

  l1 = l, fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( (events((R(t1, l, v1), b) ' | false) + events((h0.take(firstVolWrite(l, h0)) | l) | false)) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc ( (events((l1 = l ⊃ (R(t1, l, v1), b) ';[]) | false) + events((h0.take(firstVolWrite(l, h0)) | l) | false)) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

• Proof step 18:

  fowl ≠ [], l1 ≠ l, firstPersistW(fowl) < # fowl, absloc ((events([] | false) + events((h0.take(firstVolWrite(l, h0)) | l) | false)) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc ( (events((l1 = l ⊃ (R(t1, l, v1), b) ';[]) | false) + events((h0.take(firstVolWrite(l, h0)) | l) | false)) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((¬ b ⊃ (R(t1, l, v1), false) ';[])) + events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc ( events((¬ b ⊃ (R(t1, l, v1), false) ';[])) + events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(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 13 from proof absloc-persist-firstPersistW (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 14:

  ¬ b, fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((R(t1, l, v1), false) ') + events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc ( events((¬ b ⊃ (R(t1, l, v1), false) ';[])) + events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

• Proof step 16:

  b, fowl ≠ [], firstPersistW(fowl) < # fowl, absloc (events([]) + events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc ( events((¬ b ⊃ (R(t1, l, v1), false) ';[])) + events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc(events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc (events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ¬ t1 ∈ rset → FO(t1) ∈ fowl, ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(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 ⊦ FO(t) ∈ fowl -p firstPersistW(fowl) ↔ FO(t) ∈ fowl; (s) ⊦ events(vpe ') = vpe._1 '; (s)

Proof step 15 from proof absloc-persist-firstPersistW (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: fowl, l, t, v, rset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc(events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc (events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(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 17 from proof absloc-persist-firstPersistW (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: fowl, l, t, v, rset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  fowl ≠ [], l1 ≠ l, firstPersistW(fowl) < # fowl, absloc(events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc (events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(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 19 from proof absloc-persist-firstPersistW (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: fowl, l, t, v, rset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((((W(t1, l1, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events((((W(t1, l1, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ l0 ≠ l → firstVolWrite(l, (W(t, l0, v), b) ' + h) = firstVolWrite(l, h) + 1

• Proof step 23:

  l1 = l, fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((((W(t1, l1, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events((((W(t1, l1, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, (W(t1, l1, v1), b) ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

• Proof step 27:

  fowl ≠ [], l1 ≠ l, firstPersistW(fowl) < # fowl, absloc ( events((((W(t1, l1, v1), b) ' + h0).take(firstVolWrite(l, h0) + 1) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc ( events((((W(t1, l1, v1), b) ' + h0).take(firstVolWrite(l, h0) + 1) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: v1, b, l, l1, t1, h0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((((W(t1, l, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l, v1), b) ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, (W(t1, l, v1), b) ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events((((W(t1, l, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l, v1), b) ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, (W(t1, l, v1), b) ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 25:

  b, fowl ≠ [], firstPersistW(fowl) < # fowl, absloc ( events((((W(t1, l, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l, v1), b) ' + h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, (W(t1, l, v1), b) ' + h0)) | l) | false), rset, fowl), ¬ absloc ( events((((W(t1, l, v1), b) ' + h0).take(firstVolWrite(l, (W(t1, l, v1), b) ' + h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, (W(t1, l, v1), b) ' + h0))) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-persist-leading-firstPersistW: ⊦ absloc(W(t, l, v) ' + events((h | l) | false), rset, fowl) → absloc (events((persistDependentReads(l, h) | l) | false), rset, fowl -p firstPersistW(fowl)); ⊦ x.take(0) = []; (s) ⊦ [] | l = []; (s) ⊦ [] | b = []; (s) ⊦ events([]) = []; (s) ⊦ firstVolWrite(l, (W(t, l, v), false) ' + h) = 0; (s) ⊦ x.drop(0) = x; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: b

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  fowl ≠ [], firstPersistW(fowl) < # fowl, absloc(events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc (events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ firstVolWrite(l, (W(t, l0, v), true) ' + h) = firstVolWrite(l, h) + 1; (s) ⊦ (e, true) ' + h | false = h | false; (s) ⊦ (W(t, l, v), b) ' + h | l = (W(t, l, v), b) ' + (h | l); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s)

Proof step 26 from proof absloc-persist-firstPersistW (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: fowl, l, t, v, rset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  fowl ≠ [], l1 ≠ l, firstPersistW(fowl) < # fowl, absloc(events((h0.take(firstVolWrite(l, h0)) | l) | false) + W(t, l, v) ' + events((h0.drop(firstVolWrite(l, h0) + 1) | l) | false), rset, fowl), ¬ absloc (events((h0.take(firstVolWrite(l, h0)) | l) | false) + events((persistDependentReads(l, h0.drop(firstVolWrite(l, h0) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)), ∀ fowl0, l0, t0, v0, rset0. ¬ firstPersistW(fowl0) < # fowl0 ∨ ¬ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + W(t0, l0, v0) ' + events((h0.drop(firstVolWrite(l0, h0) + 1) | l0) | false), rset0, fowl0) ∨ absloc (events((h0.take(firstVolWrite(l0, h0)) | l0) | false) + events((persistDependentReads(l0, h0.drop(firstVolWrite(l0, h0) + 1)) | l0) | false), rset0, fowl0 -p firstPersistW(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) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s)

Proof step 28 from proof absloc-persist-firstPersistW (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: fowl, l, t, v, rset