Proof step 1 from proof sw-del-add (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ((h -- r0) ++ r)(r := o) ≠ (h ++ r)(r := o) -- r0, r ≠ null, r0 ≠ r, ¬ r ∈ h ⊦

Rule argument

Additional information

Proof step 2 from proof sw-del-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ((h -- r0) ++ r)(r := o) ≠ (h ++ r)(r := o) -- r0, r ≠ null, r0 ≠ r, ¬ r ∈ h ⊦

Rule argument

Additional information

Proof step 3 from proof sw-del-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 5:

  r ≠ null, r0 ≠ r, ¬ r ∈ h, ∃ r1. ¬ ( (r1 ∈ ((h -- r0) ++ r)(r := o) ↔ r1 ∈ (h ++ r)(r := o) -- r0) ∧ (r1 ∈ ((h -- r0) ++ r)(r := o) → ((h -- r0) ++ r)(r := o)(r1) = ((h ++ r)(r := o) -- r0)(r1))) ⊦

Rule argument

Additional information

Used terms: (h ++ r)(r := o) -- r0, ((h -- r0) ++ r)(r := o)

Proof step 4 from proof sw-del-add (previous step) (back to tree)

Lemma ext

Proof step 5 from proof sw-del-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  r ≠ null, r0 ≠ r, ¬ r ∈ h ⊦ (r1 = r ∨ r1 ≠ r0 ∧ r1 ∈ h → r1 ≠ r0 ∧ (r1 = r ∨ r1 ∈ h)) ∧ (r1 = r ∨ r1 ≠ r0 ∧ r1 ∈ h → (r1 = r ⊃ o;((h -- r0) ++ r)(r1)) = ((h ++ r)(r := o) -- r0)(r1))

Rule argument

Additional information

Used simplifier rules: in-write: ⊦ r ∈ h(r0 := o) ↔ r ∈ h; at-write: ⊦ h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ o;h(r)); in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h;

Proof step 6 from proof sw-del-add (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  r ≠ null, r0 ≠ r, ¬ r ∈ h, r1 = r ∨ r1 ≠ r0 ∧ r1 ∈ h ⊦ r1 ≠ r0 ∧ (r1 = r ∨ r1 ∈ h)

• Proof step 9:

  (r1 = r ⊃ o;((h -- r0) ++ r)(r1)) ≠ ((h ++ r)(r := o) -- r0)(r1), r ≠ null, r0 ≠ r, ¬ r ∈ h, r1 = r ∨ r1 ≠ r0 ∧ r1 ∈ h ⊦

Rule argument

Additional information

Proof step 7 from proof sw-del-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  r ≠ null, r0 ≠ r, ¬ r ∈ h, r1 = r ∨ r1 ≠ r0 ∧ r1 ∈ h ⊦ r1 ≠ r0 ∧ (r1 = r ∨ r1 ∈ h)

Rule argument

Additional information

Proof step 8 from proof sw-del-add (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Proof step 9 from proof sw-del-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (r1 = r ⊃ o;((h -- r0) ++ r)(r1)) ≠ ((h ++ r)(r := o) -- r0)(r1), r ≠ null, r0 ≠ r, ¬ r ∈ h, r1 = r ∨ r1 ≠ r0 ∧ r1 ∈ h ⊦

Rule argument

Additional information

Proof step 10 from proof sw-del-add (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-write: ⊦ r ∈ h(r0 := o) ↔ r ∈ h; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; at-del: r ∈ h ⊦ r ≠ r0 → (h -- r0)(r) = h(r); at-write-same-alloc: ⊦ ¬ r ∈ h ∧ r ≠ null → (h ++ r)(r := o)(r) = o; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; in-write: ⊦ r ∈ h(r0 := o) ↔ r ∈ h; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; at-del: r ∈ h ⊦ r ≠ r0 → (h -- r0)(r) = h(r); at-write: ⊦ h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ o;h(r)); at-alloc: r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ (h ++ r0)(r) = h(r);