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 := o) \ rs ≠ (h \ rs)(r := o), ¬ r ∈ rs, ¬ r ∈ h ⊦

Rule argument

Additional information

Proof step 2 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 3:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 4:

  ¬ r ∈ rs, ¬ r ∈ h, ∃ a. ¬((a ∈ (h \ rs)(r := o) ↔ a ∈ h(r := o) \ rs) ∧ (h \ rs)(r := o)(a) = (h(r := o) \ rs)(a)) ⊦

Rule argument

Additional information

Used terms: h(r := o) \ rs, (h \ rs)(r := o)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: in-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s)

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

  ⊦ a ≠ b → st(b := d)(a) = st(a)

• Proof step 7:

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

• Proof step 10:

  r0 ≠ r, ¬ r ∈ rs, ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h ∧ ¬ r0 ∈ rs → (r0 = r ∨ r0 ∈ h) ∧ ¬ r0 ∈ rs) ∧ (h \ rs)(r0) = (h(r := o) \ rs)(r0)

Rule argument

Additional information

Used terms: h \ rs, r, o, r0

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

A spec-lemma

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:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a = b → st(b := d)(a) = d; (s)

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: ⊦ a = b → st(b := d)(a) = d; (s) ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s) Used terms: h(r := o), rs, r

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

Rule argument

Additional information

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

Rule argument

Additional information

Used simplifier rules: at-diffs: ⊦ r ∈ h ∧ ¬ r ∈ rs → (h \ rs)(r) = h(r); ⊦ a ≠ b → st(b := d)(a) = st(a); (s) ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s) Used terms: h(r := o), rs, r0

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

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s)

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:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 16:

  (h \ rs)(r0) ≠ ∅(r0), r0 ≠ r, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ h(r := o) \ rs ⊦ r0 ∈ h ∧ ¬ r0 ∈ rs

Rule argument

Additional information

Used simplifier rules: in-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; at-diffs: ⊦ r ∈ h ∧ ¬ r ∈ rs → (h \ rs)(r) = h(r); ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s) Used terms: h(r := o) \ rs, r0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: in-diffs: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s)

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

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

Rule argument

Additional information

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

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

A spec-lemma