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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h ++ r)[r, o] \ rs ≠ ((h \ rs) ++ r)[r, o], r ≠ null, ¬ r ∈ rs, ¬ r ∈ h ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (h ++ r)[r, o] \ rs ≠ ((h \ rs) ++ r)[r, o], r ≠ null, ¬ r ∈ rs, ¬ r ∈ h ⊦

Rule argument

Additional information

Proof step 3 from proof sw-del-add-new (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, ¬ r ∈ rs, ¬ r ∈ h, ∃ r0. ¬((r0 ∈ (h ++ r)[r, o] \ rs ↔ r0 ∈ ((h \ rs) ++ r)[r, o]) ∧ (r0 ∈ (h ++ r)[r, o] \ rs → ((h ++ r)[r, o] \ rs)[r0] = ((h \ rs) ++ r)[r, o][r0])) ⊦

Rule argument

Additional information

Used terms: ((h \ rs) ++ r)[r, o], (h ++ r)[r, o] \ rs

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

Lemma ext

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  r ≠ null, ¬ r ∈ rs, ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h ∧ ¬ r0 ∈ rs → (r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs) ∧ ((r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs → ((h ++ r)[r, o] \ rs)[r0] = (r0 = r ⊃ o;((h \ rs) ++ r)[r0]))

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-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h;

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  r0 = r, r ≠ null, ¬ r ∈ rs, ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h ∧ ¬ r0 ∈ rs → (r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs) ∧ ((r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs → ((h ++ r)[r, o] \ rs)[r0] = (r0 = r ⊃ o;((h \ rs) ++ r)[r0]))

• Proof step 10:

  r ≠ null, r0 ≠ r, ¬ r ∈ rs, ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h ∧ ¬ r0 ∈ rs → (r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs) ∧ ((r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs → ((h ++ r)[r, o] \ rs)[r0] = (r0 = r ⊃ o;((h \ rs) ++ r)[r0]))

Rule argument

Additional information

Used formulas: r0 = r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ((h ++ r)[r, o] \ rs)[r] ≠ o, r ≠ null, ¬ r ∈ rs, ¬ r ∈ h ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ r ∈ h ∧ ¬ r ∈ rs → (h \ rs)[r] = h[r]

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-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; Used terms: r, rs, (h ++ r)[r, o]

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

Lemma at-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ((h ++ r)[r, o] \ rs)[r0] ≠ h[r0], r ≠ null, r0 ≠ r, r0 ∈ h, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; at-alloc: r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]; at-diffs: ⊦ r ∈ h ∧ ¬ r ∈ rs → (h \ rs)[r] = h[r];

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ r ∈ h ∧ ¬ r ∈ rs → (h \ rs)[r] = h[r]

• Proof step 13:

  (h ++ r)[r, o][r0] ≠ h[r0], r ≠ null, r0 ≠ r, r0 ∈ h, r0 ∈ (h ++ r)[r, o], ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs ⊦

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; Used terms: r0, rs, (h ++ r)[r, o]

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

Lemma at-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

Proof step 14 from proof sw-del-add-new (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]

Rule argument

Additional information

Used terms: r0, r, h

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

Lemma at-alloc