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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(h0 ∪ h1 ⊆ h ↔ h0 ⊆ h ∧ h1 ⊆ h), h0 ⊥ h1 ⊦

Rule argument

Additional information

Proof step 2 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

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

Rule argument

Additional information

Used terms: h0 ∪ h1, h

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

Lemma subset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  h0 ⊥ h1 ⊦ (∀ r. (r ∈ h0 ∨ r ∈ h1 → r ∈ h) ∧ (r ∈ h0 ∨ r ∈ h1 → (r ∈ h0 ⊃ h0(r);h1(r)) = h(r))) ↔ h0 ⊆ h ∧ h1 ⊆ h

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 5 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  h0 ⊥ h1 ⊦ (∀ r. (r ∈ h0 ∨ r ∈ h1 → r ∈ h) ∧ (r ∈ h0 ∨ r ∈ h1 → (r ∈ h0 ⊃ h0(r);h1(r)) = h(r))) ↔ (∀ r. (r ∈ h0 → r ∈ h) ∧ (r ∈ h0 → h0(r) = h(r))) ∧ h1 ⊆ h

Rule argument

Additional information

Used terms: h0, h

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

Lemma subset

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

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

Rule argument

Additional information

Used terms: h1, h

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

Lemma subset

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

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 10:

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

• Proof step 36:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

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

• Proof step 28:

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

Rule argument

Additional information

Used formulas: r ∈ h0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 14:

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

• Proof step 26:

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

Rule argument

Additional information

Used formulas: r ∈ h

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

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

• Proof step 24:

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

Rule argument

Additional information

Used formulas: h0(r) = h(r)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used formulas: r0 ∈ h1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Proof step 19 from proof union-subset (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

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

• Proof step 22:

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

Rule argument

Additional information

Used formulas: r0 ∈ h

Proof step 20 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Proof step 21 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; Used terms: r0

Proof step 22 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Proof step 23 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; Used terms: r0

Proof step 24 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h0(r) ≠ h(r), h0 ⊥ h1, r ∈ h, r ∈ h0, ∀ r. (r ∈ h0 ∨ r ∈ h1 → r ∈ h) ∧ (r ∈ h0 ∨ r ∈ h1 → (r ∈ h0 ⊃ h0(r);h1(r)) = h(r)) ⊦

Rule argument

Additional information

Proof step 25 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 26 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Proof step 27 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 28 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Proof step 29 from proof union-subset (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Used formulas: r0 ∈ h1

Proof step 30 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Proof step 31 from proof union-subset (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 32:

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

• Proof step 34:

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

Rule argument

Additional information

Used formulas: r0 ∈ h

Proof step 32 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

Proof step 33 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; Used terms: r0

Proof step 34 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

Proof step 35 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; Used terms: r0

Proof step 36 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

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

Rule argument

Additional information

Proof step 37 from proof union-subset (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 38:

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

• Proof step 44:

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

Rule argument

Additional information

Used formulas: r ∈ h0

Proof step 38 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

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

Rule argument

Additional information

Proof step 39 from proof union-subset (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 40:

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

• Proof step 42:

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

Rule argument

Additional information

Used formulas: r ∈ h

Proof step 40 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

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

Rule argument

Additional information

Proof step 41 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 42 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

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

Rule argument

Additional information

Proof step 43 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 44 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

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

Rule argument

Additional information

Proof step 45 from proof union-subset (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

Used formulas: r ∈ h1

Proof step 46 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

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

Rule argument

Additional information

Proof step 47 from proof union-subset (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 48:

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

• Proof step 50:

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

Rule argument

Additional information

Used formulas: r ∈ h

Proof step 48 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  h1(r) ≠ h(r), h0 ⊥ h1, r ∈ h, r ∈ h1, ¬ r ∈ h0, ∀ r. (r ∈ h1 → r ∈ h) ∧ (r ∈ h1 → h1(r) = h(r)), ∀ r. (r ∈ h0 → r ∈ h) ∧ (r ∈ h0 → h0(r) = h(r)) ⊦

Rule argument

Additional information

Proof step 49 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 50 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

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

Rule argument

Additional information

Proof step 51 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r