Proof step 1 from proof union-left-singleton (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ∅(r := h(r)) ∪ (h -- r) ≠ h, r ∈ h ⊦

Rule argument

Additional information

Proof step 2 from proof union-left-singleton (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 ∈ h, ∃ a. ¬((a ∈ h ↔ a ∈ ∅(r := h(r)) ∪ (h -- r)) ∧ h(a) = (∅(r := h(r)) ∪ (h -- r))(a)) ⊦

Rule argument

Additional information

Used terms: ∅(r := h(r)) ∪ (h -- r), h

Proof step 3 from proof union-left-singleton (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof union-left-singleton (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  r ∈ h ⊦ (r0 ∈ h ↔ r0 ∈ ∅(r := h(r)) ∪ (h -- r)) ∧ h(r0) = (∅(r := h(r)) ∪ (h -- r))(r0)

Rule argument

Additional information

Proof step 5 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 7:

  r ∈ h, ∅(r := h(r)) ⊥ h -- r ⊦ (r0 ∈ h ↔ r0 ∈ ∅(r := h(r)) ∨ r0 ∈ h -- r) ∧ h(r0) = (∅(r := h(r)) ∪ (h -- r))(r0)

Rule argument

Additional information

Used simplifier rules: disj-singleton-write: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) Used terms: r0, ∅(r := h(r)), h -- r

Proof step 6 from proof union-left-singleton (previous step) (back to tree)

Lemma in-uni

Proof step 7 from proof union-left-singleton (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  h(r0) ≠ (∅(r := h(r)) ∪ (h -- r))(r0), r ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: disj-singleton-write: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s)

Proof step 8 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r))

• Proof step 10:

  h(r0) ≠ (∅(r := h(r)) ∪ (h -- r))(r0), r ∈ h ⊦ r0 ∈ ∅(r := h(r)) ∪ (h -- r) ∧ ∅(r := h(r)) ⊥ h -- r

• Proof step 17:

  h(r0) ≠ (r0 ∈ ∅(r := h(r)) ⊃ ∅(r := h(r))(r0);(h -- r)(r0)), r ∈ h, r0 ∈ ∅(r := h(r)) ∪ (h -- r), ∅(r := h(r)) ⊥ h -- r ⊦

Rule argument

Additional information

Used terms: ∅(r := h(r)), h -- r, r0

Proof step 9 from proof union-left-singleton (previous step) (back to tree)

Lemma at-uni

Proof step 10 from proof union-left-singleton (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h(r0) ≠ (∅(r := h(r)) ∪ (h -- r))(r0), r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-singleton-write: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s)

Proof step 11 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  h(r0) ≠ (∅(r := h(r)) ∪ (h -- r))(r0), r ∈ h, r0 ∈ ∅(r := h(r)) ∪ (h -- r), ¬ r0 ∈ h ⊦

• Proof step 15:

  h(r0) ≠ ∅(r0), r ∈ h, ¬ r0 ∈ ∅(r := h(r)) ∪ (h -- r), ¬ r0 ∈ h ⊦

Rule argument

Additional information

Used terms: ∅(r := h(r)) ∪ (h -- r), r0

Proof step 12 from proof union-left-singleton (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

Rule argument

Additional information

Used simplifier rules: disj-singleton-write: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; disj-singleton-write: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) Used terms: r0, ∅(r := h(r)), h -- r

Proof step 14 from proof union-left-singleton (previous step) (back to tree)

Lemma in-uni

Proof step 15 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used terms: h, r0

Proof step 16 from proof union-left-singleton (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof union-left-singleton (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  h(r0) ≠ (r0 = r ⊃ h(r);h(r0)), r ∈ h, r0 ∈ ∅(r := h(r)) ∪ (h -- r) ⊦

Rule argument

Additional information

Used simplifier rules: disj-singleton-write: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ a ≠ b → (st -- b)(a) = st(a); (s) ⊦ a = b → st(b := d)(a) = d; (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s)

Proof step 18 from proof union-left-singleton (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information