Proof step 1 from proof overwrite-persist-one-write-restrict-true (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h2 |W | l) | true = [], mem ⊕ (h1 + (W(t, l, v), true) ' + h2 | true) ≠ (mem ⊕ (h1 + (W(t, l, v), false) ' + h2 | true))(l := v) ⊦

Rule argument

Additional information

Proof step 2 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ (h1.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ (h1.filter(._2) + h2.filter(._2)))(l := v) ⊦

Rule argument

Additional information

Used simplifier rules: restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-true-true: ⊦ (e, true) ' + h | true = (e, true) ' + (h | true); overwrite-persist-one-write: ⊦ mem ⊕ (h1 + (W(t, l, v), true) ' + h2) = mem ⊕ (h1 + (W(t, l, v), false) ' + h2); restrict-b-append: ⊦ h + h0 | b = (h | b) + (h0 | b); restrict-true-false: ⊦ (e, false) ' + h | true = h | true; restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 3 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ ([].filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ([].filter(._2) + h2.filter(._2)))(l := v) ⊦

• Proof step 49:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ ((vpe + h).filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ((vpe + h).filter(._2) + h2.filter(._2)))(l := v), ∀ h2, l, mem, t, v. ¬ ( h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [] ∧ mem ⊕ (h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ (h.filter(._2) + h2.filter(._2)))(l := v)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ h2.filter(._2) ≠ (mem ⊕ h2.filter(._2))(l := v) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ [].filter(p) = []; (s)

Proof step 5 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  (vpe + h).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ (vpe + h).filter(._2) ≠ (mem ⊕ (vpe + h).filter(._2))(l := v), ∀ l, mem, v. ¬(h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [] ∧ mem(l := v) ⊕ h.filter(._2) ≠ (mem ⊕ h.filter(._2))(l := v)) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-base: ⊦ mem ⊕ [] = mem; List('a) freely generated by [], +;; ⊦ [].filter(p) = []; (s)

Proof step 6 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (vpe._1.W? ⊃ vpe ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) = [], h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ ((vpe._2 ⊃ vpe ';[]) + h.filter(._2)) ≠ (mem ⊕ ((vpe._2 ⊃ vpe ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

Proof step 7 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], (e.W? ⊃ vpe ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) = [], vpe = (e, boolvar), mem(l := v) ⊕ ((boolvar ⊃ vpe ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ vpe ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 8 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (e.W? ⊃ (e, boolvar) ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) = [], h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 9 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], (e, boolvar) '.filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

• Proof step 24:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], [].filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 10 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], (e.l = l ⊃ (e, boolvar) ';[]).filter(._2) = [], mem(l := v) ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s)

Proof step 11 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  (l1 = l ⊃ (e, boolvar) ';[]).filter(._2) = [], h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], e = W(t, l1, v1), mem(l := v) ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ e.W? → ((t = e.t ∧ l = e.l) ∧ v = e.v ↔ e = W(t, l, v)); (elim) Used terms: e, t, l1, v1

Proof step 12 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], (l1 = l ⊃ (W(t, l, v1), boolvar) ';[]).filter(._2) = [], mem(l := v) ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 13 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 14:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], (W(t, l, v1), boolvar) '.filter(._2) = [], l1 = l, mem(l := v) ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

• Proof step 16:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], [].filter(._2) = [], l1 ≠ l, mem(l := v) ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 14 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ h.filter(._2) ≠ (mem ⊕ h.filter(._2))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ a ' ≠ []; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s)

Proof step 15 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem, v

Proof step 16 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], l1 ≠ l, mem(l := v) ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [].filter(p) = []; (s)

Proof step 17 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 18:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], boolvar, l1 ≠ l, mem(l := v) ⊕ ((W(t, l1, v1), true) ' + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

• Proof step 22:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], ¬ boolvar, l1 ≠ l, mem(l := v) ⊕ ([] + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (W(t, l1, v1), true) ';[]) + h.filter(._2)))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 18 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], l1 ≠ l, mem(l := v)(l1 := v1) ⊕ h.filter(._2) ≠ (mem(l1 := v1) ⊕ h.filter(._2))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 19 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ l0 ≠ l1 → mem(l0 := v0)(l1 := v1) = mem(l1 := v1)(l0 := v0)

• Proof step 21:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], l1 ≠ l, mem(l1 := v1)(l := v) ⊕ h.filter(._2) ≠ (mem(l1 := v1) ⊕ h.filter(._2))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used terms: l1, mem, v1, l, v

Proof step 20 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Lemma mem-update-swap

Proof step 21 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem(l1 := v1), v

Proof step 22 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], l1 ≠ l, mem(l := v) ⊕ h.filter(._2) ≠ (mem ⊕ h.filter(._2))(l := v), ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 23 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem, v

Proof step 24 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [].filter(p) = []; (s)

Proof step 25 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 26:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], boolvar, mem(l := v) ⊕ ((e, true) ' + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

• Proof step 47:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], ¬ boolvar, mem(l := v) ⊕ ([] + h.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2)))(l := v), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 26 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ ((e, true) ' + h.filter(._2)) ≠ (mem ⊕ ((e, true) ' + h.filter(._2)))(l := v), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 27 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 28:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], ((mem(l := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ (mem ⊕ ((e, true) ' + h.filter(._2)))(l := v)(l0), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 28 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], ((mem(l := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ (l = l0 ⊃ v;((mem ⊕ ((e, true) ' + h.filter(._2))))(l0)), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 29 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 30:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], l = l0, ((mem(l := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ v, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: at-overwrite-mem-update-other: ⊦ l ≠ l0 → ((mem(l0 := v) ⊕ h))(l) = ((mem ⊕ h))(l);

Proof step 30 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [], ((mem(l0 := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ v, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 31 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ (h | l)|W = [] → ((mem ⊕ h))(l) = mem(l)

• Proof step 33:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [], ((e, true) ' + h.filter(._2) | l0)|W ≠ [], ((mem(l0 := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ v, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: restrict-l-append: ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); restrict-l-one: ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-W-append: ⊦ (h + h0)|W = h |W + h0 |W; restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: mem(l0 := v), (e, true) ' + h.filter(._2), l0

Proof step 32 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Lemma at-overwrite-no-write

Proof step 33 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [], ((mem(l0 := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ v, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦ (e.l = l0 ⊃ (e, true) ';[]).filter(λ vpe. vpe._1.W?) = [] ∧ h.filter(._2).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) = []

Rule argument

Additional information

Used simplifier rules: restrict-l-append: ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); restrict-l-one: ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-W-append: ⊦ (h + h0)|W = h |W + h0 |W; restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 34 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 35:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [], (e.l = l0 ⊃ (e, true) ';[]).filter(λ vpe. vpe._1.W?) ≠ [], ((mem(l0 := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ v, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

• Proof step 36:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [], h.filter(._2).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [], ((mem(l0 := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ v, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 35 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [].filter(p) = []; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) Used formulas: e.l = l0

Proof step 36 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 38:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [], ((mem(l0 := v) ⊕ ((e, true) ' + h.filter(._2))))(l0) ≠ v, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0), ∃ a. a ∈ h.filter(._2).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ⊦

Rule argument

Additional information

Used terms: h.filter(._2).filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?)

Proof step 37 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = vpe._1.l).filter(._2) = [], ((mem(vpe._1.l := v) ⊕ ((e, true) ' + h.filter(._2))))(vpe._1.l) ≠ v, vpe._1.W?, vpe ∈ h, ¬ e.W?, vpe._2, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 39 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 40:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = e0.l).filter(._2) = [], boolvar, vpe = (e0, boolvar), ((mem(e0.l := v) ⊕ ((e, true) ' + h.filter(._2))))(e0.l) ≠ v, e0.W?, vpe ∈ h, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used terms: e0, boolvar

Proof step 40 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = e0.l).filter(._2) = [], ((mem(e0.l := v) ⊕ ((e, true) ' + h.filter(._2))))(e0.l) ≠ v, e0.W?, (e0, true) ∈ h, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 41 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 42:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l).filter(._2) = [], e0 = W(t, l, v1), ((mem(l := v) ⊕ ((e, true) ' + h.filter(._2))))(l) ≠ v, e0.W?, (e0, true) ∈ h, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ e.W? → ((t = e.t ∧ l = e.l) ∧ v = e.v ↔ e = W(t, l, v)); (elim) Used terms: e0, t, l, v1

Proof step 42 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l).filter(._2) = [], ((mem(l := v) ⊕ ((e, true) ' + h.filter(._2))))(l) ≠ v, (W(t, l, v1), true) ∈ h, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 43 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 45:

  ((mem(l := v) ⊕ ((e, true) ' + h.filter(._2))))(l) ≠ v, (W(t, l, v1), true) ∈ h, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0), ∀ a. ¬ a ∈ h.filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l).filter(._2) ⊦

Rule argument

Additional information

Used terms: h.filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l).filter(._2)

Proof step 44 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  ((mem(l := v) ⊕ ((e, true) ' + h.filter(._2))))(l) ≠ v, (W(t, l, v1), true) ∈ h, ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0), ∀ a. ¬ a ∈ h ∨ ¬ a._1.W? ∨ a._1.l ≠ l ∨ ¬ a._2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 46 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 47 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l := v) ⊕ h.filter(._2) ≠ (mem ⊕ h.filter(._2))(l := v), ¬ e.W?, ∀ l0, mem0, v0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0(l0 := v0) ⊕ h.filter(._2) = (mem0 ⊕ h.filter(._2))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 48 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem, v

Proof step 49 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ (((vpe._2 ⊃ vpe ';[]) + h.filter(._2)) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ (((vpe._2 ⊃ vpe ';[]) + h.filter(._2)) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s)

Proof step 50 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 51:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], vpe = (e, boolvar), mem ⊕ (((boolvar ⊃ vpe ';[]) + h.filter(._2)) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ (((boolvar ⊃ vpe ';[]) + h.filter(._2)) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 51 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 52 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 53:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], boolvar, mem ⊕ ((e, true) ' + h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

• Proof step 59:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], ¬ boolvar, mem ⊕ ([] + h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ((boolvar ⊃ (e, true) ';[]) + h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

Proof step 53 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ ((e, true) ' + h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ((e, true) ' + h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 54 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 55:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], e = R(t1, l1, v1), mem ⊕ ((e, true) ' + h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ((e, true) ' + h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

• Proof step 57:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], e = W(t1, l1, v1), mem ⊕ ((e, true) ' + h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ ((e, true) ' + h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 55 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ (h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ (h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 56 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: h2, l, mem, t, v

Proof step 57 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem(l1 := v1) ⊕ (h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem(l1 := v1) ⊕ (h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 58 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: h2, l, mem(l1 := v1), t, v

Proof step 59 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = [], mem ⊕ (h.filter(._2) + (W(t, l, v), false) ' + h2.filter(._2)) ≠ (mem ⊕ (h.filter(._2) + h2.filter(._2)))(l := v), ∀ h0, l0, mem0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) ≠ [] ∨ mem0 ⊕ (h.filter(._2) + (W(t0, l0, v0), false) ' + h0.filter(._2)) = (mem0 ⊕ (h.filter(._2) + h0.filter(._2)))(l0 := v0) ⊦

Rule argument

Additional information

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

Proof step 60 from proof overwrite-persist-one-write-restrict-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: h2, l, mem, t, v