Proof step 1 from proof sep-com (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  hP0 * hP1 ≠ hP1 * hP0 ⊦

Rule argument

Additional information

Proof step 2 from proof sep-com (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 3:

  ¬(((hP0 * hP1))(h) ↔ ((hP1 * hP0))(h)) ⊦

Rule argument

Additional information

Proof step 3 from proof sep-com (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ((hP0 * hP1))(h), ¬ ((hP1 * hP0))(h) ⊦

• Proof step 12:

  ((hP1 * hP0))(h), ¬ ((hP0 * hP1))(h) ⊦

Rule argument

Additional information

Proof step 4 from proof sep-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 6:

  ¬ ((hP1 * hP0))(h), ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1) ⊦

Rule argument

Additional information

Used terms: h, hP1, hP0

Proof step 5 from proof sep-com (previous step) (back to tree)

Lemma sep

Proof step 6 from proof sep-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  hP0(h0), hP1(h1), h0 ⊥ h1, ¬ ((hP1 * hP0))(h0 ∪ h1) ⊦

Rule argument

Additional information

Proof step 7 from proof sep-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 9:

  hP0(h0), hP1(h1), h0 ⊥ h1, h1 ⊥ h0, ¬ ((hP1 * hP0))(h1 ∪ h0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (s) Used terms: h1, h0

Proof step 8 from proof sep-com (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof sep-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  hP0(h0), hP1(h1), h0 ⊥ h1, ¬ ((hP1 * hP0))(h1 ∪ h0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (s)

Proof step 10 from proof sep-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1))(h0 ∪ h1)

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (s) Used terms: h0, h1, hP0, hP1

Proof step 11 from proof sep-com (previous step) (back to tree)

Lemma split-union

Proof step 12 from proof sep-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 14:

  ¬ ((hP0 * hP1))(h), ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP1(h0) ∧ hP0(h1) ⊦

Rule argument

Additional information

Used terms: h, hP0, hP1

Proof step 13 from proof sep-com (previous step) (back to tree)

Lemma sep

Proof step 14 from proof sep-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  hP0(h1), hP1(h0), h0 ⊥ h1, ¬ ((hP0 * hP1))(h0 ∪ h1) ⊦

Rule argument

Additional information

Proof step 15 from proof sep-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 17:

  hP0(h1), hP1(h0), h0 ⊥ h1, h1 ⊥ h0, ¬ ((hP0 * hP1))(h1 ∪ h0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (s) Used terms: h1, h0

Proof step 16 from proof sep-com (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof sep-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  hP0(h1), hP1(h0), h0 ⊥ h1, ¬ ((hP0 * hP1))(h1 ∪ h0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (s)

Proof step 18 from proof sep-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1))(h0 ∪ h1)

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (s) Used terms: h0, h1, hP1, hP0

Proof step 19 from proof sep-com (previous step) (back to tree)

Lemma split-union