Proof step 1 from proof rmpos-in (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(a ∈ x -p n ↔ a ≠ x[n] ∧ a ∈ x), n < # x, ¬ dups(x) ⊦

Rule argument

Additional information

Proof step 2 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(a ∈ x -p n ↔ a ≠ x[n] ∧ a ∈ x), x ≠ [], n < # 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 rmpos-in (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a0 + x0 ≠ [], ¬(a ∈ (a0 + x0) -p n ↔ a ≠ (a0 + x0)[n] ∧ a ∈ a0 + x0), n < #(a0 + x0), ¬ dups(a0 + x0), ∀ a, n. ¬(¬(a ∈ x0 -p n ↔ a ≠ x0[n] ∧ a ∈ x0) ∧ x0 ≠ [] ∧ n < # x0 ∧ ¬ dups(x0)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(a ∈ (a0 ' + x0) -p n ↔ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)), n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (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 < n + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) ⊦ a ' + x ≠ []; (s)

Proof step 5 from proof rmpos-in (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  ¬(a ∈ (a0 ' + x0) -p n ↔ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)), x0 ≠ [], n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: delnr-one: ⊦ a ' -p 0 = []; one-03: ⊦ a '[0] = a; ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # [] = 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ ¬ dups([]); (s) ⊦ ¬ a ∈ []; (s) Used formulas: x0 = []

Proof step 6 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ¬(a ∈ (a0 ' + x0) -p n ↔ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)), x0 ≠ [], n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Proof step 7 from proof rmpos-in (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  ¬(a ∈ (a0 ' + x0) -p n ↔ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)), x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

• Proof step 28:

  ¬(a ∈ (a0 ' + x0) -p n ↔ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)), x0 ≠ [], n ≤ # x0, ¬ dups(x0), ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used formulas: a ∈ (a0 ' + x0) -p n

Proof step 8 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Proof step 9 from proof rmpos-in (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  a = a0, x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)

• Proof step 15:

  a ≠ a0, x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦ a ≠ (a0 ' + x0)[n] ∧ (a = a0 ∨ a ∈ x0)

Rule argument

Additional information

Used formulas: a = a0

Proof step 10 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a0 = (a0 ' + x0)[n], x0 ≠ [], a0 ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Proof step 11 from proof rmpos-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  a0 = x0[n - # a0 '], x0 ≠ [], a0 ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ n < # a0 ', ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: get-zero-01: ⊦ (a ' + x)[0] = a; delpos-base: ⊦ (a ' + x) -p 0 = x; ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n, x0, a0 '

Proof step 12 from proof rmpos-in (previous step) (back to tree)

Lemma get-append-grt

Proof step 13 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  n ≠ 0, x0 ≠ [], x0[n - 1] ∈ (x0[n - 1] ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ x0[n - 1] ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

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

Proof step 14 from proof rmpos-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: delpos-rec: ⊦ (a ' + x) -p (n + 1) = a + (x -p n); get-in: ⊦ m < # x → (x[m] ∈ x ↔ true); ⊦ m + 1 ≠ 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ a + x = a ' + x; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m

Proof step 15 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  a ≠ a0, x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦ a ≠ (a0 ' + x0)[n] ∧ a ∈ x0

Rule argument

Additional information

Proof step 16 from proof rmpos-in (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  a ≠ a0, x0 ≠ [], a ∈ (a0 ' + x0) -p n, a ∈ x0, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦ a ≠ (a0 ' + x0)[n] ∧ a ∈ x0

• Proof step 24:

  a ≠ a0, x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a ∈ x0, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦ a ≠ (a0 ' + x0)[n] ∧ a ∈ x0

Rule argument

Additional information

Used formulas: a ∈ x0

Proof step 17 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (a0 ' + x0)[n] ≠ a0, x0 ≠ [], (a0 ' + x0)[n] ∈ (a0 ' + x0) -p n, (a0 ' + x0)[n] ∈ x0, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Proof step 18 from proof rmpos-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  x0[n - # a0 '] ≠ a0, x0 ≠ [], x0[n - # a0 '] ∈ x0, x0[n - # a0 '] ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ n < # a0 ', ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: get-zero-01: ⊦ (a ' + x)[0] = a; ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n, x0, a0 '

Proof step 19 from proof rmpos-in (previous step) (back to tree)

Lemma get-append-grt

Proof step 20 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  x0[n - 1] ≠ a0, n ≠ 0, x0 ≠ [], x0[n - 1] ∈ (a0 ' + x0) -p n, x0[n - 1] ∈ x0, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

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

Proof step 21 from proof rmpos-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 22:

  n = m + 1, x0[m] ≠ a0, n ≠ 0, x0 ≠ [], x0[m] ∈ x0, x0[m] ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

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

Proof step 22 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  x0[m] ≠ a0, x0 ≠ [], m < # x0, x0[m] ∈ x0 -p m, x0[m] ∈ x0, ¬ dups(x0), ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: delpos-rec: ⊦ (a ' + x) -p (n + 1) = a + (x -p n); ⊦ # 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) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 23 from proof rmpos-in (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x0[m], m

Proof step 24 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  a ≠ a0, x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a ∈ x0, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Proof step 25 from proof rmpos-in (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 26:

  n = n1 +1, a ≠ a0, x0 ≠ [], a ∈ (a0 ' + x0) -p n, n ≤ # x0, ¬ dups(x0), ¬ a ∈ x0, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: delpos-base: ⊦ (a ' + x) -p 0 = x; nat freely generated by 0, +1;; ⊦ 0 ≤ m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 26 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  a ≠ a0, x0 ≠ [], n1 < # x0, a ∈ x0 -p n1, ¬ dups(x0), ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: delpos-rec: ⊦ (a ' + x) -p (n + 1) = a + (x -p n); ⊦ # 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 → (a ∈ b ' + x ↔ a ∈ x); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

Proof step 27 from proof rmpos-in (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a, n1

Proof step 28 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  a ≠ (a0 ' + x0)[n], x0 ≠ [], n ≤ # x0, ¬ dups(x0), ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0, a = a0 ∨ a ∈ x0 ⊦

Rule argument

Additional information

Proof step 29 from proof rmpos-in (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 30:

  a ≠ (a0 ' + x0)[n], x0 ≠ [], a ∈ x0, n ≤ # x0, ¬ dups(x0), ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0, a = a0 ∨ a ∈ x0 ⊦

• Proof step 37:

  a ≠ (a0 ' + x0)[n], x0 ≠ [], n ≤ # x0, ¬ dups(x0), ¬ a ∈ x0, ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0, a = a0 ∨ a ∈ x0 ⊦

Rule argument

Additional information

Used formulas: a ∈ x0

Proof step 30 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  a ≠ (a0 ' + x0)[n], x0 ≠ [], a ∈ x0, n ≤ # x0, ¬ dups(x0), ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Proof step 31 from proof rmpos-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

  a ≠ x0[n - # a0 '], x0 ≠ [], a ∈ x0, n ≤ # x0, ¬ n < # a0 ', ¬ dups(x0), ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: get-zero-01: ⊦ (a ' + x)[0] = a; delpos-base: ⊦ (a ' + x) -p 0 = x; ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ 0 ≤ m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n, x0, a0 '

Proof step 32 from proof rmpos-in (previous step) (back to tree)

Lemma get-append-grt

Proof step 33 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  a ≠ x0[n - 1], n ≠ 0, x0 ≠ [], a ∈ x0, n ≤ # x0, ¬ dups(x0), ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

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

Proof step 34 from proof rmpos-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 35:

  n = m + 1, a ≠ x0[m], n ≠ 0, x0 ≠ [], a ∈ x0, n ≤ # x0, ¬ dups(x0), ¬ a ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

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

Proof step 35 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  a ≠ x0[m], x0 ≠ [], m < # x0, a ∈ x0, ¬ dups(x0), ¬ a ∈ x0 -p m, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: delpos-rec: ⊦ (a ' + x) -p (n + 1) = a + (x -p n); ⊦ # 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); (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 36 from proof rmpos-in (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a, m

Proof step 37 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  a0 ≠ (a0 ' + x0)[n], x0 ≠ [], n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Proof step 38 from proof rmpos-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

  a0 ≠ x0[n - # a0 '], x0 ≠ [], n ≤ # x0, ¬ n < # a0 ', ¬ dups(x0), ¬ a0 ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: get-zero-01: ⊦ (a ' + x)[0] = a; ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n, x0, a0 '

Proof step 39 from proof rmpos-in (previous step) (back to tree)

Lemma get-append-grt

Proof step 40 from proof rmpos-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  a0 ≠ x0[n - 1], n ≠ 0, x0 ≠ [], n ≤ # x0, ¬ dups(x0), ¬ a0 ∈ (a0 ' + x0) -p n, ¬ a0 ∈ x0, ∀ a1, n0. (a1 ∈ x0 -p n0 ↔ a1 ≠ x0[n0] ∧ a1 ∈ x0) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

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

Proof step 41 from proof rmpos-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: delpos-rec: ⊦ (a ' + x) -p (n + 1) = a + (x -p n); ⊦ m + 1 ≠ 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ a + x = a ' + x; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ a ∈ b ' + x ↔ ¬(a ≠ b ∧ ¬ a ∈ x); (ss) a: ⊦ (x + y) + z = x + y + z; from specification list n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m