Proof step 1 from proof diffone-nodupsget (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (x \ a ')[n] ≠ (n < pos(a, x) ⊃ x[n];x[n + 1]), n + 1 < # x, a ∈ x, ¬ dups(x) ⊦

Rule argument

Additional information

Proof step 2 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (x \ a ')[n] ≠ (n < pos(a, x) ⊃ x[n];x[n + 1]), x ≠ [], n + 1 < # x, a ∈ x, ¬ dups(x) ⊦

Rule argument

Additional information

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

Proof step 3 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a0 + x0 ≠ [], ((a0 + x0) \ a ')[n] ≠ (n < pos(a, a0 + x0) ⊃ (a0 + x0)[n];(a0 + x0)[n + 1]), n + 1 < #(a0 + x0), a ∈ a0 + x0, ¬ dups(a0 + x0), ∀ a, n. ¬((x0 \ a ')[n] ≠ (n < pos(a, x0) ⊃ x0[n];x0[n + 1]) ∧ x0 ≠ [] ∧ n + 1 < # x0 ∧ a ∈ x0 ∧ ¬ dups(x0)) ⊦

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

Proof step 4 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ((a0 ' + x0) \ a ')[n] ≠ (¬ pos(a, x0) < n ⊃ (a0 ' + x0)[n];x0[n]), a ≠ a0, x0 ≠ [], n < # x0, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: diff-firstofapp: ⊦ (x + y) \ x = y \ x; diff-onenonmember: ⊦ ¬ a ∈ x → x \ a ' = x; 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) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ≠ b → pos(a, b ' + x) = pos(a, x) + 1; (s) ⊦ m < # x ∧ n < # x ∧ ¬ dups(x) → (x[m] = x[n] ↔ m = n); (s) ⊦ ¬ n < 0; (s) ⊦ pos(a, a ' + x) = 0; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s) ⊦ a + x = a ' + x; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ a ' + x ≠ []; (s)

Proof step 5 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  ((a0 ' + x0) \ a ')[n] ≠ (¬ pos(a, x0) < n ⊃ (a0 ' + x0)[n];x0[n]), a ≠ a0, x0 ≠ [], n < # x0, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ a ', ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: diff-y: ⊦ a ∈ y → (a ' + x) \ y = x \ y; a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) Used formulas: a0 ∈ a '

Proof step 6 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (a0 ' + (x0 \ a '))[n] ≠ (¬ pos(a, x0) < n ⊃ (a0 ' + x0)[n];x0[n]), a ≠ a0, x0 ≠ [], n < # x0, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: diff-n: ⊦ ¬ a ∈ y → (a ' + x) \ y = a + (x \ y); ⊦ a ∈ a0 ' ↔ a = a0; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a + x = a ' + x; (s)

Proof step 7 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  (a0 ' + (x0 \ a '))[n] ≠ (¬ pos(a, x0) < n ⊃ (a0 ' + x0)[n];x0[n]), a ≠ a0, x0 ≠ [], n < # x0, pos(a, x0) < n, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

• Proof step 15:

  (a0 ' + (x0 \ a '))[n] ≠ (¬ pos(a, x0) < n ⊃ (a0 ' + x0)[n];x0[n]), a ≠ a0, x0 ≠ [], n < # x0, a ∈ x0, ¬ pos(a, x0) < n, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used formulas: pos(a, x0) < n

Proof step 8 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (a0 ' + (x0 \ a '))[n] ≠ x0[n], a ≠ a0, x0 ≠ [], n < # x0, pos(a, x0) < n, pos(a, x0) + 1 < # x0, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x → pos(a, x) < # x; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 9 from proof diffone-nodupsget (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]

• Proof step 11:

  (x0 \ a ')[n - # a0 '] ≠ x0[n], a ≠ a0, x0 ≠ [], pos(a, x0) + 1 < # x0, pos(a, x0) < n, n < # x0, a ∈ x0, ¬ n < # a0 ', ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m < n → n ≠ 0; (s) Used terms: n, x0 \ a ', a0 '

Proof step 10 from proof diffone-nodupsget (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (x0 \ a ')[n - 1] ≠ x0[n], a ≠ a0, x0 ≠ [], n < # x0, pos(a, x0) < n, pos(a, x0) + 1 < # x0, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s)

Proof step 12 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  n = m + 1, (x0 \ a ')[m] ≠ x0[n], a ≠ a0, n ≠ 0, x0 ≠ [], pos(a, x0) + 1 < # x0, pos(a, x0) < n, n < # x0, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ ¬ n < 0; (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m

Proof step 13 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  (x0 \ a ')[m] ≠ x0[m + 1], a ≠ a0, x0 ≠ [], pos(a, x0) + 1 < # x0, m + 1 < # x0, a ∈ x0, pos(a, x0) ≤ m, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 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 ≠ 0; (s)

Proof step 14 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: a, m

Proof step 15 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (a0 ' + (x0 \ a '))[n] ≠ (a0 ' + x0)[n], a ≠ a0, x0 ≠ [], n < # x0, a ∈ x0, n ≤ pos(a, x0), ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 16 from proof diffone-nodupsget (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]

• Proof step 18:

  (x0 \ a ')[n - # a0 '] ≠ (a0 ' + x0)[n], a ≠ a0, x0 ≠ [], n < # x0, a ∈ x0, n ≤ pos(a, x0), ¬ n < # a0 ', ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: n, x0 \ a ', a0 '

Proof step 17 from proof diffone-nodupsget (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  (x0 \ a ')[n - 1] ≠ x0[n - 1], a ≠ a0, n ≠ 0, x0 ≠ [], n < # x0, a ∈ x0, n ≤ pos(a, x0), ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 19 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  n = m + 1, (x0 \ a ')[m] ≠ x0[m], a ≠ a0, n ≠ 0, x0 ≠ [], n < # x0, a ∈ x0, n ≤ pos(a, x0), ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m

Proof step 20 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  (x0 \ a ')[m] ≠ x0[m], a ≠ a0, x0 ≠ [], m < pos(a, x0), m + 1 < # x0, a ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (x0 \ a1 ')[n0] = (n0 < pos(a1, x0) ⊃ x0[n0];x0[n0 + 1]) ∨ ¬ n0 + 1 < # x0 ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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 ≠ 0; (s)

Proof step 21 from proof diffone-nodupsget (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a, m