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 ∈ (h ++ r)(r := o) \ rs ↔ r0 ∈ (h \ rs) ++ r) ∧ (r0 ∈ (h ++ r)(r := o) \ rs → ((h ++ r)(r := o) \ rs)(r0) = (r0 = r ∧ r ∈ (h \ rs) ++ 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));

Proof step 6 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 7:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

• Proof step 8:

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

Rule argument

Additional information

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

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

Lemma in-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

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;

Proof step 9 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 10:

  r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h

• Proof step 11:

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

• Proof step 14:

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

Rule argument

Additional information

Used terms: r, h \ rs, r0

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

Lemma in-alloc

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  r ∈ h \ rs, ¬ r ∈ rs, ¬ r ∈ h ⊦ ((r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs ↔ r0 ∈ (h \ rs) ++ r) ∧ ((r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs → ((h ++ r)(r := o) \ rs)(r0) = (r0 = r ∧ r ∈ (h \ rs) ++ r ⊃ o;((h \ rs) ++ r)(r0)))

Rule argument

Additional information

Used simplifier rules: nonnull: ⊦ r ∈ h → r ≠ null;

Proof step 12 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 13:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r, h, rs

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

Lemma in-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: in-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs;

Proof step 15 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 16:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

• Proof step 17:

  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 ∧ r ∈ (h \ rs) ++ r ⊃ o;((h \ rs) ++ r)(r0)))

Rule argument

Additional information

Used terms: r0, h, rs

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

Lemma in-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  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 ∧ r ∈ (h \ rs) ++ r ⊃ o;((h \ rs) ++ r)(r0)))

Rule argument

Additional information

Proof step 18 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 19:

  r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h

• Proof step 20:

  r ≠ null, ¬ r ∈ rs, ¬ r ∈ h ⊦ r ≠ null ∧ ¬ r ∈ h \ rs, (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 ∧ r ∈ (h \ rs) ++ r ⊃ o;((h \ rs) ++ r)(r0)))

• Proof step 23:

  r ≠ null, ¬ r ∈ h \ rs, ¬ 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 ∧ (r = r ∨ r ∈ h \ rs) ⊃ o;((h \ rs) ++ r)(r0)))

Rule argument

Additional information

Used terms: r, h \ rs, r

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

Lemma in-alloc

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  r ∈ h \ rs, ¬ 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 ∧ r ∈ (h \ rs) ++ r ⊃ o;((h \ rs) ++ r)(r0)))

Rule argument

Additional information

Used simplifier rules: nonnull: ⊦ r ∈ h → r ≠ null;

Proof step 21 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 22:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r, h, rs

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

Lemma in-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  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-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs;

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 25:

  r ≠ null, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs ⊦ (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 ∈ rs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ((h ++ r)(r := o) \ rs)(r0) ≠ (r0 = r ⊃ o;((h \ rs) ++ r)(r0)), r ≠ null, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, r0 = r ∨ r0 ∈ h ⊦

Rule argument

Additional information

Proof step 26 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 27:

  r0 = r, ((h ++ r)(r := o) \ rs)(r0) ≠ (r0 = r ⊃ o;((h \ rs) ++ r)(r0)), r ≠ null, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, r0 = r ∨ r0 ∈ h ⊦

• Proof step 30:

  ((h ++ r)(r := o) \ rs)(r0) ≠ (r0 = r ⊃ o;((h \ rs) ++ r)(r0)), r ≠ null, r0 ≠ r, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, r0 = r ∨ r0 ∈ h ⊦

Rule argument

Additional information

Used formulas: r0 = r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ((h ++ r)(r := o) \ rs)(r) ≠ o, r ≠ null, ¬ r ∈ h, ¬ r ∈ rs ⊦

Rule argument

Additional information

Proof step 28 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 29:

  ⊦ 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, (h ++ r)(r := o), rs

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

Lemma at-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Proof step 31 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 32:

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

• Proof step 33:

  (h ++ r)(r := o)(r0) ≠ ((h \ rs) ++ r)(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, (h ++ r)(r := o), rs

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

Lemma at-diffs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Used simplifier rules: at-write-other: ⊦ r ≠ r0 → h(r0 := o)(r) = h(r); at-alloc: r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)(r) = 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 34 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 35:

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

• Proof step 36:

  h(r0) ≠ ((h \ rs) ++ r)(r0), r ≠ null, r0 ≠ r, r0 ∈ h, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs ⊦ r0 ∈ h \ rs ∧ r ≠ null ∧ ¬ r ∈ h \ rs ∧ r0 ≠ r

Rule argument

Additional information

Used simplifier rules: at-diffs: ⊦ r ∈ h ∧ ¬ r ∈ rs → (h \ rs)(r) = h(r); Used terms: r0, h \ rs, r

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

Lemma at-alloc

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  h(r0) ≠ ((h \ rs) ++ r)(r0), r0 ≠ r, r ∈ h \ rs, r0 ∈ h, r0 ∈ h \ rs, ¬ r ∈ h, ¬ r ∈ rs, ¬ r0 ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; nonnull: ⊦ r ∈ h → r ≠ null;

Proof step 37 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 38:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r, h, rs

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

Lemma in-diffs