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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  mem ⊕ (h + (W(t, l, v), b) ') ≠ (mem ⊕ h)(l := v) ⊦

Rule argument

Additional information

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

User applied rule induction

And obtained the following new goals

• Proof step 3:

  hPred([]), ∀ t, l, v, h. hPred(h) → hPred((W(t, l, v), true) ' + h), ∀ t, l, v, h. hPred(h) → hPred((W(t, l, v), false) ' + h), ∀ t, l, v, h. hPred(h) → hPred((R(t, l, v), true) ' + h), ∀ t, l, v, h. hPred(h) → hPred((R(t, l, v), false) ' + h) ⊦ hPred(h)

• Proof step 4:

  [] = h, mem ⊕ (h + (W(t, l, v), b) ') ≠ (mem ⊕ h)(l := v) ⊦

• Proof step 5:

  ∀ mem, h1, t, l, v, b. ¬(h = h1 ∧ mem ⊕ (h1 + (W(t, l, v), b) ') ≠ (mem ⊕ h1)(l := v)) ⊦ ∀ mem, h1, t0, l0, v0, b. ¬((W(t, l, v), true) ' + h = h1 ∧ mem ⊕ (h1 + (W(t0, l0, v0), b) ') ≠ (mem ⊕ h1)(l0 := v0))

• Proof step 7:

  ∀ mem, h1, t, l, v, b. ¬(h = h1 ∧ mem ⊕ (h1 + (W(t, l, v), b) ') ≠ (mem ⊕ h1)(l := v)) ⊦ ∀ mem, h1, t0, l0, v0, b. ¬((W(t, l, v), false) ' + h = h1 ∧ mem ⊕ (h1 + (W(t0, l0, v0), b) ') ≠ (mem ⊕ h1)(l0 := v0))

• Proof step 9:

  ∀ mem, h1, t, l, v, b. ¬(h = h1 ∧ mem ⊕ (h1 + (W(t, l, v), b) ') ≠ (mem ⊕ h1)(l := v)) ⊦ ∀ mem, h1, t0, l0, v0, b. ¬((R(t, l, v), true) ' + h = h1 ∧ mem ⊕ (h1 + (W(t0, l0, v0), b) ') ≠ (mem ⊕ h1)(l0 := v0))

• Proof step 11:

  ∀ mem, h1, t, l, v, b. ¬(h = h1 ∧ mem ⊕ (h1 + (W(t, l, v), b) ') ≠ (mem ⊕ h1)(l := v)) ⊦ ∀ mem, h1, t0, l0, v0, b. ¬((R(t, l, v), false) ' + h = h1 ∧ mem ⊕ (h1 + (W(t0, l0, v0), b) ') ≠ (mem ⊕ h1)(l0 := v0))

Rule argument

Additional information

Used terms: h, λ h0. ∀ mem, h, t, l, v, b. ¬(h0 = h ∧ mem ⊕ (h + (W(t, l, v), b) ') ≠ (mem ⊕ h)(l := v))

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

Lemma hist-ind

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  mem(l := v) ⊕ (h + (W(t0, l0, v0), b) ') ≠ (mem(l := v) ⊕ h)(l0 := v0), ∀ mem0, t, l1, v1, b0. mem0 ⊕ (h + (W(t, l1, v1), b0) ') = (mem0 ⊕ h)(l1 := v1) ⊦

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 6 from proof overwrite-attach-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem(l := v), t0, l0, v0, b

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  mem(l := v) ⊕ (h + (W(t0, l0, v0), b) ') ≠ (mem(l := v) ⊕ h)(l0 := v0), ∀ mem0, t, l1, v1, b0. mem0 ⊕ (h + (W(t, l1, v1), b0) ') = (mem0 ⊕ h)(l1 := v1) ⊦

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 8 from proof overwrite-attach-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem(l := v), t0, l0, v0, b

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  mem ⊕ (h + (W(t0, l0, v0), b) ') ≠ (mem ⊕ h)(l0 := v0), ∀ mem0, t, l, v, b0. mem0 ⊕ (h + (W(t, l, v), b0) ') = (mem0 ⊕ h)(l := v) ⊦

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 10 from proof overwrite-attach-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, t0, l0, v0, b

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  mem ⊕ (h + (W(t0, l0, v0), b) ') ≠ (mem ⊕ h)(l0 := v0), ∀ mem0, t, l, v, b0. mem0 ⊕ (h + (W(t, l, v), b0) ') = (mem0 ⊕ h)(l := v) ⊦

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 12 from proof overwrite-attach-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, t0, l0, v0, b