Proof step 1 from proof rely-APersist (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))), firstVolWrite(l, gs.h) < # gs.h, allReadsOK(gs.h), allWritesOK(gs.h) ⊦ ∀ t0. rely(t0, gs.h, gs0.h)

Rule argument

Additional information

Proof step 2 from proof rely-APersist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, (gs.h |W | l) | false ≠ [], allReadsOK(gs.h), allWritesOK(gs.h), ¬ rely (t0, gs.h, gs.h.take(firstVolWrite(l, gs.h)) + (gs.h[firstVolWrite(l, gs.h)]._1, true) ' + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.h:= h).h = h; (s) 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 3 from proof rely-APersist (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, gs.h[firstVolWrite(l, gs.h)] = (e, boolvar), (gs.h |W | l) | false ≠ [], allReadsOK(gs.h), allWritesOK(gs.h), ¬ rely(t0, gs.h, gs.h.take(firstVolWrite(l, gs.h)) + (e, true) ' + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1))) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 4 from proof rely-APersist (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 5:

  # h = firstVolWrite(l, gs.h), gs.h = h + h0, gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, gs.h[firstVolWrite(l, gs.h)] = (e, boolvar), (gs.h |W | l) | false ≠ [], allReadsOK(gs.h), allWritesOK(gs.h), firstVolWrite(l, gs.h) ≤ # gs.h, ¬ rely(t0, gs.h, h + (e, true) ' + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ¬ # h < firstVolWrite(l, h); (s) ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n); (elim) Used terms: gs.h, firstVolWrite(l, gs.h), h, h0

Proof step 5 from proof rely-APersist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # h = firstVolWrite(l, h + h0), gs.h = h + h0, gs.pm = ∅ ⊕ ((h | true) + (h0 | true)), gs.vm = ∅ ⊕ (h + h0), (h + h0)[# h] = (e, boolvar), allReadsOK(h + h0), allWritesOK(h + h0), ¬ rely(t0, h + h0, h + (e, true) ' + persistDependentReads(l, h0.drop(1))) ⊦ (h |W | l) | false = [] ∧ (h0 |W | l) | false = []

Rule argument

Additional information

Used simplifier rules: 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 ⊦ (x + y).drop(# x + n) = y.drop(n); (s) ⊦ m ≤ m + n; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ (h + h0)|W = h |W + h0 |W; (s)

Proof step 6 from proof rely-APersist (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  # h = firstVolWrite(l, h + h0), # h1 = 1, gs.h = h + h0, gs.pm = ∅ ⊕ ((h | true) + (h0 | true)), gs.vm = ∅ ⊕ (h + h0), (h + h0)[# h] = (e, boolvar), h0 = h1 + h2, allReadsOK(h + h0), allWritesOK(h + h0), 1 ≤ # h0, ¬ rely(t0, h + h0, h + (e, true) ' + persistDependentReads(l, h2)) ⊦ (h |W | l) | false = [] ∧ (h0 |W | l) | false = []

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ firstVolWrite(l, h) = # h ↔ (h |W | l) | false = []; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] |W = []; (s) ⊦ [] | l = []; (s) ⊦ [] | b = []; (s) ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n); (elim) Used terms: h0, 1, h1, h2

Proof step 7 from proof rely-APersist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # h = firstVolWrite(l, gs.h), gs.h = h + h1 + h2, gs.pm = ∅ ⊕ ((h | true) + (h1 | true) + (h2 | true)), gs.vm = ∅ ⊕ gs.h, gs.h[# h] = (e, boolvar), h1 = h1.head ', # h1 + # h2 ≠ 0, allReadsOK(gs.h), allWritesOK(gs.h), 1 ≤ # h1 + # h2, ¬ rely(t0, gs.h, h + (e, true) ' + persistDependentReads(l, h2)) ⊦ (h |W | l) | false = [] ∧ (h1 |W | l) | false = [] ∧ (h2 |W | l) | false = []

Rule argument

Additional information

Used simplifier rules: not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ (h + h0)|W = h |W + h0 |W; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ x + [] = x; (s) ⊦ a + x = a ' + x; (s) ⊦ # x = 1 ↔ x = x.head + []; (as)

Proof step 8 from proof rely-APersist (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  # h = firstVolWrite(l, gs.h), gs.h = h + h1 + h2, gs.pm = ∅ ⊕ ((h | true) + (h1 | true) + (h2 | true)), gs.vm = ∅ ⊕ gs.h, gs.h[# h] = (e, boolvar), h1 = vpe ', h1 = vpe + h0, # h1 + # h2 ≠ 0, h1 ≠ [], allReadsOK(gs.h), allWritesOK(gs.h), 1 ≤ # h1 + # h2, ¬ rely(t0, gs.h, h + (e, true) ' + persistDependentReads(l, h2)) ⊦ (h |W | l) | false = [] ∧ (h1 |W | l) | false = [] ∧ (h2 |W | l) | false = []

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: h1, vpe, h0

Proof step 9 from proof rely-APersist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # h = firstVolWrite(l, gs.h), gs.h = h + vpe ' + h2, gs.pm = ∅ ⊕ ((h | true) + (vpe ' | true) + (h2 | true)), gs.vm = ∅ ⊕ gs.h, gs.h[# h] = (e, boolvar), allReadsOK(gs.h), allWritesOK(gs.h), ¬ rely(t0, gs.h, h + (e, true) ' + persistDependentReads(l, h2)) ⊦ (h |W | l) | false = [] ∧ ((vpe._1.W? ⊃ vpe ';[]) | l) | false = [] ∧ (h2 |W | l) | false = []

Rule argument

Additional information

Used simplifier rules: ⊦ [] | b = []; (s) ⊦ [] | l = []; (s) ⊦ [] |W = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ vpe ' |W = (vpe._1.W? ⊃ vpe ';[]); (s) ⊦ (h + h0)|W = h |W + h0 |W; (s) ⊦ a + x = a ' + x; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a ' ≠ []; (s) ⊦ m + 1 ≠ 0; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws)

Proof step 10 from proof rely-APersist (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  # h = firstVolWrite(l, gs.h), gs.h = h + vpe ' + h2, gs.pm = ∅ ⊕ ((h | true) + (vpe ' | true) + (h2 | true)), gs.vm = ∅ ⊕ gs.h, gs.h[# h] = (e, boolvar), vpe = (e0, boolvar0), allReadsOK(gs.h), allWritesOK(gs.h), ¬ rely(t0, gs.h, h + (e, true) ' + persistDependentReads(l, h2)) ⊦ (h |W | l) | false = [] ∧ ((e0.W? ⊃ vpe ';[]) | l) | false = [] ∧ (h2 |W | l) | false = []

Rule argument

Additional information

Used terms: e0, boolvar0

Proof step 11 from proof rely-APersist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # h = firstVolWrite(l, gs.h), gs.h = h + (e0, boolvar0) ' + h2, gs.pm = ∅ ⊕ ((h | true) + (boolvar0 ⊃ (e0, true) ';[]) + (h2 | true)), gs.vm = ∅ ⊕ gs.h, gs.h[# h] = (e, boolvar), allReadsOK(gs.h), allWritesOK(gs.h), ¬ rely(t0, gs.h, h + (e, true) ' + persistDependentReads(l, h2)) ⊦ (h |W | l) | false = [] ∧ ((e0.W? ⊃ (e0, boolvar0) ';[]) | l) | false = [] ∧ (h2 |W | l) | false = []

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 12 from proof rely-APersist (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (x + a ' + y)[# x] = a; (s) ⊦ rely(t, h0 + (e, b) ' + h1, h0 + (e, true) ' + persistDependentReads(l, h1)); (ss) a: ⊦ (x + y) + z = x + y + z; from specification list