Proof step 1 from proof at-overwrite-no-write (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], ((mem ⊕ h))(l) ≠ mem(l) ⊦

Rule argument

Additional information

Used simplifier rules: restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?);

Proof step 3 from proof at-overwrite-no-write (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

Proof step 4 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

Proof step 5 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used terms: e, boolvar

Proof step 6 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Proof step 7 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], (e, boolvar) '.filter(λ vpe. vpe._1.W?) = [], e.l = l, ((mem ⊕ ((e, boolvar) ' + h0)))(l) ≠ mem(l), ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

• Proof step 12:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], [].filter(λ vpe. vpe._1.W?) = [], e.l ≠ l, ((mem ⊕ ((e, boolvar) ' + h0)))(l) ≠ mem(l), ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

Rule argument

Additional information

Proof step 8 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h0.filter(λ vpe. vpe._1.l = e.l).filter(λ vpe. vpe._1.W?) = [], ((mem ⊕ ((e, boolvar) ' + h0)))(e.l) ≠ mem(e.l), ¬ e.W?, ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

Rule argument

Additional information

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

Proof step 9 from proof at-overwrite-no-write (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  h0.filter(λ vpe. vpe._1.l = e.l).filter(λ vpe. vpe._1.W?) = [], e = R(t, l, v), ((mem ⊕ ((e, boolvar) ' + h0)))(e.l) ≠ mem(e.l), ¬ e.W?, ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; RWevent freely generated by R, W;; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).W?; (s)

Proof step 10 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], ((mem ⊕ h0))(l) ≠ mem(l), ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

Rule argument

Additional information

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

Proof step 11 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem

Proof step 12 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], e.l ≠ l, ((mem ⊕ ((e, boolvar) ' + h0)))(l) ≠ mem(l), ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

Rule argument

Additional information

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

Proof step 13 from proof at-overwrite-no-write (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 14:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], e = R(t, l1, v), e.l ≠ l, ((mem ⊕ ((e, boolvar) ' + h0)))(l) ≠ mem(l), ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

• Proof step 16:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], e = W(t, l1, v), e.l ≠ l, ((mem ⊕ ((e, boolvar) ' + h0)))(l) ≠ mem(l), ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

Rule argument

Additional information

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

Proof step 14 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.W?) = [], l1 ≠ l, ((mem ⊕ h0))(l) ≠ mem(l), ∀ l0, mem0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. vpe._1.W?) ≠ [] ∨ ((mem0 ⊕ h0))(l0) = mem0(l0) ⊦

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 ⊦ R(t, l, v).l = l; (s)

Proof step 15 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem

Proof step 16 from proof at-overwrite-no-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

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 ⊦ W(t, l, v).l = l; (s)

Proof step 17 from proof at-overwrite-no-write (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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