Proof step 1 from proof disjointp-reduce (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  disjointp(spmx1, spmx2) ⊦ disjointp(spmx3, spmx4) ↔ (∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4)

Rule argument

Additional information

Proof step 2 from proof disjointp-reduce (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ (∀ np. np ∈ spmx3 → ¬ np ∈ spmx4) ↔ (∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4)

Rule argument

Additional information

Used simplifier rules: disjointp-def: ⊦ disjointp(sa1, sa2) ↔ (∀ np. np ∈ sa1 → ¬ np ∈ sa2);

Proof step 3 from proof disjointp-reduce (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ np. np ∈ spmx3 → ¬ np ∈ spmx4 ⊦ ∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4

• Proof step 6:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4 ⊦ ∀ np. np ∈ spmx3 → ¬ np ∈ spmx4

Rule argument

Additional information

Proof step 4 from proof disjointp-reduce (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  np ∈ spmx4, np ∈ spmx3, np ∈ spmx1 → ¬ np ∈ spmx2, ∀ np. np ∈ spmx3 → ¬ np ∈ spmx4, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦

Rule argument

Additional information

Proof step 5 from proof disjointp-reduce (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: np

Proof step 6 from proof disjointp-reduce (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  np ∈ spmx4, np ∈ spmx3, ∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦

Rule argument

Additional information

Proof step 7 from proof disjointp-reduce (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 8:

  np ∈ spmx3, np ∈ spmx4, (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4 ⊦

Rule argument

Additional information

Used terms: np

Proof step 8 from proof disjointp-reduce (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  np ∈ spmx4, np ∈ spmx3, np ∈ spmx2, np ∈ spmx1, ∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦

Rule argument

Additional information

Proof step 9 from proof disjointp-reduce (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: np