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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x ≠ [], # y < # x, ¬ dups(y), ¬ dups(x), ∀ a. a ∈ x → a ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a + x0 ≠ [], # y < #(a + x0), ¬ dups(y), ¬ dups(a + x0), ∀ a0. a0 ∈ a + x0 → a0 ∈ y, ∀ y. ¬(x0 ≠ [] ∧ # y < # x0 ∧ ¬ dups(y) ∧ ¬ dups(x0) ∧ (∀ a. a ∈ x0 → a ∈ y)) ⊦

Rule argument

Additional information

Used simplifier rules: list freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # y ≤ # x0, ¬ dups(y), ¬ dups(x0), ¬ a ∈ x0, ∀ a0. a0 = a ∨ a0 ∈ x0 → a0 ∈ y, x0 = [] ∨ (∀ y0. ¬ # y0 < # x0 ∨ dups(y0) ∨ ¬(∀ a. a ∈ x0 → a ∈ y0)) ⊦

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 < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a ' + x ≠ []; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 6:

  # y ≤ # x0, ¬ dups(y), ¬ dups(x0), ¬ a ∈ x0, a = a ∨ a ∈ x0 → a ∈ y, ∀ a0. a0 ∈ x0 → a0 ∈ y, x0 = [] ∨ (∀ y0. ¬ # y0 < # x0 ∨ dups(y0) ∨ ¬(∀ a. a ∈ x0 → a ∈ y0)) ⊦

Rule argument

Additional information

Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  a ∈ y, # y ≤ # x0, ¬ dups(y), ¬ dups(x0), ¬ a ∈ x0, ∀ a0. a0 ∈ x0 → a0 ∈ y, x0 = [] ∨ (∀ y0. ¬ # y0 < # x0 ∨ dups(y0) ∨ ¬(∀ a. a ∈ x0 → a ∈ y0)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  # y ≤ # x0, ¬ dups(y), ¬ dups(x0), ¬ a ∈ x0, ∀ a0. a0 ∈ x0 → a0 ∈ y, ∃ y0, z. y = y0 + (a + z), x0 = [] ∨ (∀ y0. ¬ # y0 < # x0 ∨ dups(y0) ∨ ¬(∀ a. a ∈ x0 → a ∈ y0)) ⊦

Rule argument

Additional information

Used terms: y, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  x0 ≠ [], # y0 + # z < # x0, ¬ dups(y0 + z), ¬ dups(x0), ¬ a ∈ z, ¬ a ∈ y0, ¬ a ∈ x0, ∀ a0. a0 ∈ x0 → a0 ∈ y0 ∨ a0 ∈ z, ∀ y0. ¬ # y0 < # x0 ∨ dups(y0) ∨ ¬(∀ a. a ∈ x0 → a ∈ y0) ⊦

Rule argument

Additional information

Used simplifier rules: f-01: ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a + x = a ' + x; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ #(x + y) = # x + # y; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 11:

  x0 ≠ [], # y0 + # z < # x0, ¬ dups(y0 + z), ¬ dups(x0), ¬ a ∈ z, ¬ a ∈ y0, ¬ a ∈ x0, ∀ a0. a0 ∈ x0 → a0 ∈ y0 ∨ a0 ∈ z, ¬ #(y0 + z) < # x0 ∨ dups(y0 + z) ∨ ¬(∀ a. a ∈ x0 → a ∈ y0 + z) ⊦

Rule argument

Additional information

Used terms: y0 + z

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  x0 ≠ [], # y0 + # z < # x0, a0 ∈ x0, ¬ dups(y0 + z), ¬ dups(x0), ¬ a ∈ z, ¬ a ∈ y0, ¬ a ∈ x0, ¬ a0 ∈ y0, ¬ a0 ∈ z, ∀ a0. a0 ∈ 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) ⊦ #(x + y) = # x + # y; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0