Proof step 1 from proof uni-inj (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(h ∪ h0 = h ∪ h1 ↔ h0 = h1), h ⊥ h1, h ⊥ h0 ⊦

Rule argument

Additional information

Proof step 2 from proof uni-inj (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h ∪ h0 = h ∪ h1, h0 ≠ h1, h ⊥ h0, h ⊥ h1 ⊦

Rule argument

Additional information

Proof step 3 from proof uni-inj (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:

  h ∪ h0 = h ∪ h1, h ⊥ h1, h ⊥ h0, ∃ r. ¬((r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))) ⊦

Rule argument

Additional information

Used terms: h1, h0

Proof step 4 from proof uni-inj (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof uni-inj (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  h ∪ h0 = h ∪ h1, h ⊥ h0, h ⊥ h1 ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

Rule argument

Additional information

Proof step 6 from proof uni-inj (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 8:

  h ⊥ h1, h ⊥ h0, ∀ r. (r ∈ h ∪ h0 ↔ r ∈ h ∪ h1) ∧ (r ∈ h ∪ h0 → (h ∪ h0)(r) = (h ∪ h1)(r)) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

Rule argument

Additional information

Used terms: h ∪ h1, h ∪ h0

Proof step 7 from proof uni-inj (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof uni-inj (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h ⊥ h0, h ⊥ h1, ∀ r0. (¬ r0 ∈ h → (r0 ∈ h0 ↔ r0 ∈ h1)) ∧ (r0 ∈ h ∨ r0 ∈ h0 → (r0 ∈ h ⊃ h(r0);h0(r0)) = (h ∪ h1)(r0)) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 9 from proof uni-inj (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  h ⊥ h1, h ⊥ h0, ¬ r ∈ h → (r ∈ h0 ↔ r ∈ h1), r ∈ h ∨ r ∈ h0 → (r ∈ h ⊃ h(r);h0(r)) = (h ∪ h1)(r), ∀ r0. (¬ r0 ∈ h → (r0 ∈ h0 ↔ r0 ∈ h1)) ∧ (r0 ∈ h ∨ r0 ∈ h0 → (r0 ∈ h ⊃ h(r0);h0(r0)) = (h ∪ h1)(r0)) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

Rule argument

Additional information

Used terms: r

Proof step 10 from proof uni-inj (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h ⊥ h0, h ⊥ h1, ¬ r ∈ h → (r ∈ h0 ↔ r ∈ h1), r ∈ h ∨ r ∈ h0 → (r ∈ h ⊃ h(r);h0(r)) = (h ∪ h1)(r), ∀ r0. (¬ r0 ∈ h → (r0 ∈ h0 ↔ r0 ∈ h1)) ∧ (r0 ∈ h ∨ r0 ∈ h0 → (r0 ∈ h ⊃ h(r0);h0(r0)) = (h ∪ h1)(r0)) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

Rule argument

Additional information

Proof step 11 from proof uni-inj (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 12:

  (r ∈ h ⊃ h(r);h0(r)) = (h ∪ h1)(r), h ⊥ h1, h ⊥ h0, ¬ r ∈ h → (r ∈ h0 ↔ r ∈ h1), ∀ r0. (¬ r0 ∈ h → (r0 ∈ h0 ↔ r0 ∈ h1)) ∧ (r0 ∈ h ∨ r0 ∈ h0 → (r0 ∈ h ⊃ h(r0);h0(r0)) = (h ∪ h1)(r0)) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

Rule argument

Additional information

Proof step 12 from proof uni-inj (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r)); disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → ¬ r ∈ h1; in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r)); disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0;