Proof step 1 from proof dups-eqsize-02 (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  # x = # y, ¬ dups(x), ∀ a. a ∈ x → a ∈ y ⊦ ¬ dups(y) ∧ (a ∈ y → a ∈ x)

Rule argument

Additional information

Proof step 2 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  #(a0 + x0) = # y, ¬ dups(a0 + x0), ∀ a. a ∈ a0 + x0 → a ∈ y, ∀ y, a. # x0 = # y ∧ ¬ dups(x0) ∧ (∀ a. a ∈ x0 → a ∈ y) → ¬ dups(y) ∧ (a ∈ y → a ∈ x0) ⊦ ¬ dups(y) ∧ (a ∈ y → a ∈ a0 + x0)

Rule argument

Additional information

Used simplifier rules: e-01: ⊦ ¬ dups([]); list freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ ¬ a ∈ []; (s)

Proof step 3 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  # x0 + 1 = # y, ¬ dups(x0), ¬ a0 ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 = a0 ∨ a1 ∈ x0 → a1 ∈ y ⊦ ¬ dups(y) ∧ (a ∈ y → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used simplifier rules: rec: ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 4 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 5:

  # x0 + 1 = # y, ¬ dups(x0), ¬ a0 ∈ x0, a0 = a0 ∨ a0 ∈ x0 → a0 ∈ y, ∀ a1. a1 ∈ x0 → a1 ∈ y, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0) ⊦ ¬ dups(y) ∧ (a ∈ y → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used terms: a0

Proof step 5 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # x0 + 1 = # y, a0 ∈ y, ¬ dups(x0), ¬ a0 ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y ⊦ ¬ dups(y) ∧ (a ∈ y → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Proof step 6 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 8:

  # x0 + 1 = # y, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1. a1 ∈ x0 → a1 ∈ y, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∃ y0, z. y = y0 + (a0 + z) ⊦ ¬ dups(y) ∧ (a ∈ y → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used terms: y, a0

Proof step 7 from proof dups-eqsize-02 (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # x0 = # y0 + # z, ¬ dups(x0), ¬ a0 ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z ⊦ ¬ dups(y0 + a0 ' + z) ∧ (a ∈ y0 ∨ a ∈ z → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ≠ b → (a ∈ b ' + x ↔ a ∈ x); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a + x = a ' + x; (s) ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 9 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  # x0 = # y0 + # z, ¬ dups(x0), ¬ a0 ∈ x0, # x0 = #(y0 + z) ∧ (∀ a. a ∈ x0 → a ∈ y0 + z) → ¬ dups(y0 + z) ∧ (a ∈ y0 + z → a ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0) ⊦ ¬ dups(y0 + a0 ' + z) ∧ (a ∈ y0 ∨ a ∈ z → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used terms: y0 + z, a

Proof step 10 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # x0 = # y0 + # z, ¬ dups(x0), ¬ a0 ∈ x0, (a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z) → ¬ dups(y0 + z) ∧ (a ∈ y0 ∨ a ∈ z → a ∈ x0), ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z ⊦ ¬ dups(y0 + a0 ' + z) ∧ (a ∈ y0 ∨ a ∈ z → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 11 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  # x0 = # y0 + # z, ¬ dups(x0), ¬ a0 ∈ x0, (a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z) → ¬ dups(y0 + z) ∧ (a ∈ y0 ∨ a ∈ z → a ∈ x0), a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0) ⊦ ¬ dups(y0 + a0 ' + z) ∧ (a ∈ y0 ∨ a ∈ z → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used terms: a1

Proof step 12 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # x0 = # y0 + # z, ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, a ∈ y0 ∨ a ∈ z → a ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z ⊦ ¬ dups(y0 + a0 ' + z) ∧ (a ∈ y0 ∨ a ∈ z → a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Proof step 13 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a ∈ y0 ∨ a ∈ z → a ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0) ⊦

Rule argument

Additional information

Proof step 14 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, a ∈ y0 ∨ a ∈ z → a ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z ⊦

Rule argument

Additional information

Proof step 15 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ ¬ a ∈ x ∧ ¬ a ∈ y → (dups(x + a ' + y) ↔ dups(x + y))

• Proof step 17:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a ∈ y0 ∨ a ∈ z → a ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0) ⊦ ¬ a0 ∈ y0 ∧ ¬ a0 ∈ z

Rule argument

Additional information

Used terms: z, a0, y0

Proof step 16 from proof dups-eqsize-02 (previous step) (back to tree)

Lemma d

Proof step 17 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, a ∈ y0 ∨ a ∈ z → a ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z ⊦ ¬ a0 ∈ y0 ∧ ¬ a0 ∈ z

Rule argument

Additional information

Proof step 18 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 19:

  # x = # y, ¬ dups(x), ¬ dups(y), ∀ a. a ∈ x → a ∈ y ⊦ ∀ a. a ∈ y → a ∈ x

• Proof step 20:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a ∈ y0 ∨ a ∈ z → a ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0) ⊦ ¬ a0 ∈ y0 ∧ ¬ a0 ∈ z, # x0 = #(y0 + z) ∧ (∀ a. a ∈ x0 → a ∈ y0 + z)

• Proof step 22:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a ∈ y0 ∨ a ∈ z → a ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a. a ∈ y0 + z → a ∈ x0 ⊦ ¬ a0 ∈ y0 ∧ ¬ a0 ∈ z

Rule argument

Additional information

Used terms: x0, y0 + z

Proof step 19 from proof dups-eqsize-02 (previous step) (back to tree)

Lemma dups-eqsize-01

Proof step 20 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), a2 ∈ x0, ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, ¬ a2 ∈ y0, ¬ a2 ∈ z, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, a ∈ y0 ∨ a ∈ z → a ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z ⊦ ¬ a0 ∈ y0 ∧ ¬ a0 ∈ z

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 21 from proof dups-eqsize-02 (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 22 from proof dups-eqsize-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # x0 = # y0 + # z, dups(y0 + a0 ' + z), ¬ dups(x0), ¬ dups(y0 + z), ¬ a0 ∈ x0, a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, a ∈ y0 ∨ a ∈ z → a ∈ x0, ∀ y0, a1. # x0 = # y0 ∧ (∀ a. a ∈ x0 → a ∈ y0) → ¬ dups(y0) ∧ (a1 ∈ y0 → a1 ∈ x0), ∀ a1. a1 ∈ x0 → a1 ∈ y0 ∨ a1 ∈ z, ∀ a2. a2 ∈ y0 ∨ a2 ∈ z → a2 ∈ x0 ⊦ ¬ a0 ∈ y0 ∧ ¬ a0 ∈ z

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 23 from proof dups-eqsize-02 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: f-01: ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a0