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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  alldisjointp(ts, f) ⊦ alldisjointp(ts, f0) ↔ (∀ tid1, tid2, np. (tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2) ⊦ (∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f0(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f0(tid2)) ↔ (∀ tid1, tid2, np. (np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2))

Rule argument

Additional information

Used simplifier rules: alldisjointp-def: ⊦ alldisjointp(ts, f) ↔ (∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2));

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

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2), ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f0(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f0(tid2) ⊦ ∀ tid1, tid2, np. (np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2)

• Proof step 6:

  ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2), ∀ tid1, tid2, np. (np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2) ⊦ ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f0(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f0(tid2)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # ts ≠ 0, tid1 ≠ tid2, ts ≠ ∅, np ∈ f0(tid1), tid2 ∈ ts, tid1 ∈ ts, np ∈ f0(tid2), np ∈ f(tid1) → ¬ np ∈ f(tid2), ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2), ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f0(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f0(tid2) ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic[tidset-npset] ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic[tidset-npset]

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid1, tid2, np

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # ts ≠ 0, tid1 ≠ tid2, ts ≠ ∅, np ∈ f0(tid1), tid2 ∈ ts, tid1 ∈ ts, np ∈ f0(tid2), ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2), ∀ tid1, tid2, np. (np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2) ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic[tidset-npset] ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic[tidset-npset]

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

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 8:

  # ts ≠ 0, tid1 ≠ tid2, ts ≠ ∅, np ∈ f0(tid2), tid1 ∈ ts, tid2 ∈ ts, np ∈ f0(tid1), (np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2), ∀ tid1, tid2, np. (np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2), ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2) ⊦

Rule argument

Additional information

Used terms: tid1, tid2, np

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # ts ≠ 0, tid1 ≠ tid2, ts ≠ ∅, np ∈ f0(tid1), tid2 ∈ ts, tid1 ∈ ts, np ∈ f0(tid2), np ∈ f(tid2), np ∈ f(tid1), ∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2), ∀ tid1, tid2, np. (np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid1, tid2, np