Proof step 1 from proof del-two (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  s -- a -- a0 = ∅, s ≠ ∅, s ≠ ∅ ++ a, s ≠ ∅ ++ a0, s ≠ ∅ ++ a ++ a0 ⊦

Rule argument

Additional information

Proof step 2 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), ¬(a3 ∈ s ↔ a3 = a0), ¬(a2 ∈ s ↔ a2 = a), a1 ∈ s, a5 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: Delete: ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; ⊦ ¬ a ∈ ∅; (s) ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2); (s) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification polyset-basic ⊦ a ∈ ∅ ++ b ↔ a = b; (s)

Proof step 3 from proof del-two (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

  ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), ¬(a3 ∈ s ↔ a3 = a0), ¬(a2 ∈ s ↔ a2 = a), a5 ∈ s, a1 ∈ s, a2 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

• Proof step 16:

  ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), ¬(a3 ∈ s ↔ a3 = a0), ¬(a2 ∈ s ↔ a2 = a), a5 ∈ s, a1 ∈ s, ¬ a2 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

Rule argument

Additional information

Used formulas: a2 ∈ s

Proof step 4 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), ¬(a3 ∈ s ↔ a3 = a0), a2 ≠ a, a2 ∈ s, a1 ∈ s, a5 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

Rule argument

Additional information

Proof step 5 from proof del-two (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), ¬(a3 ∈ s ↔ a3 = a0), a2 ≠ a, a5 ∈ s, a1 ∈ s, a2 ∈ s, a3 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

• Proof step 14:

  ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), ¬(a3 ∈ s ↔ a3 = a0), a2 ≠ a, a5 ∈ s, a1 ∈ s, a2 ∈ s, ¬ a3 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

Rule argument

Additional information

Used formulas: a3 ∈ s

Proof step 6 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ¬(a4 ∈ s ↔ a4 = a0 ∨ a4 = a), a2 ≠ a, a3 ≠ a0, a3 ∈ s, a2 ∈ s, a1 ∈ s, a5 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ ∅ ++ b ↔ a = b; (s) ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 7 from proof del-two (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 8:

  a2 ≠ a, a3 ≠ a0, a4 ≠ a0, a4 ≠ a, a5 ∈ s, a1 ∈ s, a2 ∈ s, a3 ∈ s, a4 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

• Proof step 9:

  a2 ≠ a, a3 ≠ a0, a5 ∈ s, a1 ∈ s, a2 ∈ s, a3 ∈ s, ¬ a4 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s, a4 = a0 ∨ a4 = a ⊦

Rule argument

Additional information

Proof step 8 from proof del-two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a4

Proof step 9 from proof del-two (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 10:

  a4 = a0, a2 ≠ a, a3 ≠ a0, a3 ∈ s, a2 ∈ s, a1 ∈ s, a5 ∈ s, ¬ a4 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

• Proof step 12:

  a4 = a, a2 ≠ a, a3 ≠ a0, a3 ∈ s, a2 ∈ s, a1 ∈ s, a5 ∈ s, ¬ a4 ∈ s, ∀ a5. a5 = a0 ∨ a5 = a ∨ ¬ a5 ∈ s ⊦

Rule argument

Additional information

Proof step 10 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a2 ≠ a, a3 ≠ a0, a5 ∈ s, a1 ∈ s, a2 ∈ s, a3 ∈ s, ¬ a0 ∈ s, ∀ a4. a4 = a ∨ ¬ a4 ∈ s ⊦

Rule argument

Additional information

Proof step 11 from proof del-two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a2

Proof step 12 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a2 ≠ a, a3 ≠ a0, a5 ∈ s, a1 ∈ s, a2 ∈ s, a3 ∈ s, ¬ a ∈ s, ∀ a4. a4 = a0 ∨ ¬ a4 ∈ s ⊦

Rule argument

Additional information

Proof step 13 from proof del-two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a3

Proof step 14 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), a2 ≠ a, a5 ∈ s, a1 ∈ s, a2 ∈ s, ¬ a0 ∈ s, ∀ a3. a3 = a ∨ ¬ a3 ∈ s ⊦

Rule argument

Additional information

Proof step 15 from proof del-two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a2

Proof step 16 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ¬(a3 ∈ s ↔ a3 = a0), ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), a5 ∈ s, a1 ∈ s, ¬ a ∈ s, ∀ a2. a2 = a0 ∨ ¬ a2 ∈ s ⊦

Rule argument

Additional information

Proof step 17 from proof del-two (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 18:

  ¬(a3 ∈ s ↔ a3 = a0), ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), a5 ≠ a, a1 ∈ s, a5 ∈ s, ¬ a ∈ s, ∀ a2. a2 = a0 ∨ ¬ a2 ∈ s ⊦

Rule argument

Additional information

Used formulas: a5 = a

Proof step 18 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ¬(a3 ∈ s ↔ a3 = a0), ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), a5 ≠ a, a5 ∈ s, a1 ∈ s, ¬ a ∈ s, ∀ a2. a2 = a0 ∨ ¬ a2 ∈ s ⊦

Rule argument

Additional information

Proof step 19 from proof del-two (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

  ¬(a3 ∈ s ↔ a3 = a0), ¬(a4 ∈ s ↔ a4 ∈ ∅ ++ a ++ a0), a5 ≠ a, a1 ∈ s, a5 ∈ s, ¬ a ∈ s, ∀ a2. a2 = a0 ∨ ¬ a2 ∈ s ⊦

Rule argument

Additional information

Used formulas: a5 ∈ s

Proof step 20 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ¬(a3 ∈ s ↔ a3 = a0), ¬(a4 ∈ s ↔ a4 = a0 ∨ a4 = a), a5 ≠ a, a5 ∈ s, a1 ∈ s, ¬ a ∈ s, ∀ a2. a2 = a0 ∨ ¬ a2 ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ ∅ ++ b ↔ a = b; (s) ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 21 from proof del-two (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 22:

  ¬(a4 ∈ s ↔ a4 = a0 ∨ a4 = a), a3 ≠ a0, a5 ≠ a, a1 ∈ s, a5 ∈ s, a3 ∈ s, ¬ a ∈ s, ∀ a2. a2 = a0 ∨ ¬ a2 ∈ s ⊦

• Proof step 23:

  a3 = a0, ¬(a4 ∈ s ↔ a4 = a0 ∨ a4 = a), a5 ≠ a, a1 ∈ s, a5 ∈ s, ¬ a3 ∈ s, ¬ a ∈ s, ∀ a2. a2 = a0 ∨ ¬ a2 ∈ s ⊦

Rule argument

Additional information

Proof step 22 from proof del-two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a3

Proof step 23 from proof del-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  ¬(a4 ∈ s ↔ a4 = a0 ∨ a4 = a), a5 ≠ a, a5 ∈ s, a1 ∈ s, ¬ a0 ∈ s, ¬ a ∈ s, ∀ a2. ¬ a2 ∈ s ⊦

Rule argument

Additional information

Proof step 24 from proof del-two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a1