Proof step 1 from proof dom-rem (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  dom(st \ s) ≠ dom st \ s ⊦

Rule argument

Additional information

Proof step 2 from proof dom-rem (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2)

• Proof step 4:

  ∃ a. ¬(a ∈ dom(st \ s) ↔ a ∈ dom st \ s) ⊦

Rule argument

Additional information

Used terms: dom st \ s, dom(st \ s)

Proof step 3 from proof dom-rem (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof dom-rem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(a ∈ st \ s ↔ a ∈ dom st \ s) ⊦

Rule argument

Additional information

Used simplifier rules: Dom: ⊦ a ∈ dom st ↔ a ∈ st;

Proof step 5 from proof dom-rem (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Diff-ext: ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s; Dom: ⊦ a ∈ dom st ↔ a ∈ st; Dom: ⊦ a ∈ dom st ↔ a ∈ st; Diff-ext: ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s; ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; (ws)