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 obtained the following new goals

• Proof step 11:

  (r1 = r ⊃ o;((H -- r0) ++ r)[r1]) ≠ ((H ++ r)[r, o] -- r0)[r1], r ≠ null, r0 ≠ r, r1 ≠ r0, r1 ∈ H, ¬ r ∈ H ⊦

Rule argument

Additional information

Used simplifier rules: in-write: ⊦ r ∈ h[r0, o] ↔ 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]); in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ((H -- r0) ++ r)[r1] ≠ (H ++ r)[r1], r ≠ null, r0 ≠ r, r1 ≠ r0, r1 ∈ H, ¬ r ∈ H ⊦

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: ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]);

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 13:

  ((H -- r0) ++ r)[r1] ≠ (H ++ r)[r1], r ≠ null, r0 ≠ r, r1 ≠ r, r1 ≠ r0, r1 ∈ H, ¬ r ∈ H ⊦

Rule argument

Additional information

Used formulas: r1 = r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ((H -- r0) ++ r)[r1] ≠ (H ++ r)[r1], r ≠ null, r0 ≠ r, r1 ≠ r, r1 ≠ r0, r1 ∈ H, ¬ r ∈ H ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]

• Proof step 16:

  (H -- r0)[r1] ≠ (H ++ r)[r1], r ≠ null, r0 ≠ r, r1 ≠ r, r1 ≠ r0, r1 ∈ H, r1 ∈ H -- r0, ¬ r ∈ H -- r0, ¬ r ∈ H ⊦

Rule argument

Additional information

Used simplifier rules: in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; Used terms: r1, r, H -- r0

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

Lemma at-alloc

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  H[r1] ≠ (H ++ r)[r1], r ≠ null, r0 ≠ r, r1 ≠ r, r1 ≠ r0, r1 ∈ H, ¬ r ∈ H ⊦

Rule argument

Additional information

Used simplifier rules: at-del: r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[r]; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]

Rule argument

Additional information

Used terms: r1, r, H

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

Lemma at-alloc