Proof step 1 from proof abs-firstPersistW-firstVolWrite-correct-loc (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  h[firstVolWrite(l, h)] = (e, bv), e.l ≠ l, firstPersistW(p(l)) < # p(l), abs(h, rs, p) ⊦

Rule argument

Additional information

Proof step 2 from proof abs-firstPersistW-firstVolWrite-correct-loc (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), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), abs(h, rs, p) ⊦

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-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  h[firstVolWrite(l, h)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), ∀ l. absloc(events((h | l) | false), rs(l), p(l)) ⊦

Rule argument

Additional information

Used terms: h, rs, p

Proof step 4 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Lemma abs-def

Proof step 5 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  h[firstVolWrite(l, h)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h | l) | false), rs(l), p(l)) ⊦

Rule argument

Additional information

Used terms: l

Proof step 6 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 7:

  (vpe + h0)[firstVolWrite(l, vpe + h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((vpe + h0 | l) | false), rs(l), p(l)), ∀ l, e, bv, p, rs. ¬(h0[firstVolWrite(l, h0)] = (e, bv) ∧ e.l ≠ l ∧ p(l) ≠ [] ∧ firstPersistW(p(l)) < # p(l) ∧ absloc(events((h0 | l) | false), rs(l), p(l))) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-base: ⊦ absloc([], rset, fowl) ↔ fowl |W = []; List('a) freely generated by [], +;; ⊦ [] | l = []; (s) ⊦ [] | b = []; (s) ⊦ events([]) = []; (s) ⊦ fowl |W = [] → firstPersistW(fowl) = # fowl; (s) ⊦ ¬ n < n; (s)

Proof step 7 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (vpe ' + h0)[firstVolWrite(l, vpe ' + h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((vpe._1.l = l ⊃ vpe ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(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) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ a + x = a ' + x; (s)

Proof step 8 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  (vpe ' + h0)[firstVolWrite(l, vpe ' + h0)] = (e, bv), vpe = (e0, bv0), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((e0.l = l ⊃ vpe ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Used terms: e0, bv0

Proof step 9 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ((e0, bv0) ' + h0)[firstVolWrite(l, (e0, bv0) ' + h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((e0.l = l ⊃ (e0, bv0) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Proof step 10 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 11:

  ((e0, bv0) ' + h0)[firstVolWrite(l, (e0, bv0) ' + h0)] = (e, bv), e0 = R(t, l1, v), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((e0.l = l ⊃ (e0, bv0) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

• Proof step 21:

  ((e0, bv0) ' + h0)[firstVolWrite(l, (e0, bv0) ' + h0)] = (e, bv), e0 = W(t, l1, v), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((e0.l = l ⊃ (e0, bv0) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

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

Proof step 11 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((l1 = l ⊃ (R(t, l, v), bv0) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ R(t, l, v).l = l; (s) 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)[n + 1] = x[n]; (s) ⊦ firstVolWrite(l, (R(t, l0, v), b) ' + h) = firstVolWrite(l, h) + 1; (s)

Proof step 12 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  h0[firstVolWrite(l, h0)] = (e, bv), l1 = l, e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((R(t, l, v), bv0) ' | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

• Proof step 19:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, l1 ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events([] | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Proof step 13 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((¬ bv0 ⊃ (R(t, l, v), false) ';[])) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

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

Proof step 14 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  h0[firstVolWrite(l, h0)] = (e, bv), ¬ bv0, e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((R(t, l, v), false) ') + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

• Proof step 17:

  h0[firstVolWrite(l, h0)] = (e, bv), bv0, e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events([]) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Proof step 15 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h0 | l) | false), rs(l), p(l)), ¬ t ∈ rs(l) → FO(t) ∈ p(l), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

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 ⊦ events(vpe ') = vpe._1 '; (s)

Proof step 16 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, e, bv, p, rs

Proof step 17 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ events([]) = []; (s)

Proof step 18 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, e, bv, p, rs

Proof step 19 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, l1 ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

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 20 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, e, bv, p, rs

Proof step 21 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ((W(t, l1, v), bv0) ' + h0)[firstVolWrite(l, (W(t, l1, v), bv0) ' + h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((l1 = l ⊃ (W(t, l, v), bv0) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s)

Proof step 22 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 23:

  ((W(t, l1, v), bv0) ' + h0)[firstVolWrite(l, (W(t, l1, v), bv0) ' + h0)] = (e, bv), l1 = l, e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((W(t, l, v), bv0) ' | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

• Proof step 27:

  ((W(t, l1, v), bv0) ' + h0)[firstVolWrite(l, (W(t, l1, v), bv0) ' + h0)] = (e, bv), e.l ≠ l, l1 ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events([] | false) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Proof step 23 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  ((W(t, l, v), bv0) ' + h0)[firstVolWrite(l, (W(t, l, v), bv0) ' + h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((¬ bv0 ⊃ (W(t, l, v), false) ';[])) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

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

Proof step 24 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 25:

  ((W(t, l, v), bv0) ' + h0)[firstVolWrite(l, (W(t, l, v), bv0) ' + h0)] = (e, bv), bv0, e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events([]) + events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ firstVolWrite(l, (W(t, l, v), false) ' + h) = 0; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ events(vpe ') = vpe._1 '; (s) ⊦ W(t, l, v).l = l; (s)

Proof step 25 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

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

Proof step 26 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, e, bv, p, rs

Proof step 27 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  h0[firstVolWrite(l, h0)] = (e, bv), e.l ≠ l, l1 ≠ l, p(l) ≠ [], firstPersistW(p(l)) < # p(l), absloc(events((h0 | l) | false), rs(l), p(l)), ∀ l0, e0, bv0, p0, rs0. h0[firstVolWrite(l0, h0)] ≠ (e0, bv0) ∨ e0.l = l0 ∨ p0(l0) = [] ∨ ¬ firstPersistW(p0(l0)) < # p0(l0) ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ events([]) = []; (s) ⊦ [] | b = []; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ l0 ≠ l → firstVolWrite(l, (W(t, l0, v), b) ' + h) = firstVolWrite(l, h) + 1; (s)

Proof step 28 from proof abs-firstPersistW-firstVolWrite-correct-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, e, bv, p, rs