Proof step 1 from proof nodups-rmposnodups (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(dups(x -p n) ↔ false), ¬ dups(x) ⊦

Rule argument

Additional information

Proof step 2 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  dups(x -p n), ¬ dups(x) ⊦

Rule argument

Additional information

Proof step 3 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  dups((a + x0) -p n), ¬ dups(a + x0), ∀ n. ¬(dups(x0 -p n) ∧ ¬ dups(x0)) ⊦

Rule argument

Additional information

Used simplifier rules: delpos-empty: ⊦ [] -p n = []; list freely generated by [], +;; ⊦ ¬ dups([]); (s)

Proof step 4 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  dups((a ' + x0) -p n), ¬ dups(x0), ¬ a ∈ x0, ∀ n0. ¬ dups(x0 -p n0) ⊦

Rule argument

Additional information

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

Proof step 5 from proof nodups-rmposnodups (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  n = n1 +1, dups((a ' + x0) -p n), ¬ dups(x0), ¬ a ∈ x0, ∀ n0. ¬ dups(x0 -p n0) ⊦

Rule argument

Additional information

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

Proof step 6 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ¬ dups(x0), ¬ a ∈ x0, ∀ n0. ¬ dups(x0 -p n0), a ∈ x0 -p n1 ∨ dups(x0 -p n1) ⊦

Rule argument

Additional information

Used simplifier rules: delpos-rec: ⊦ (a ' + x) -p (n + 1) = a + (x -p n); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(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)

Proof step 7 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  dups(x0 -p n1), ¬ dups(x0), ¬ a ∈ x0, ∀ n0. ¬ dups(x0 -p n0), a ∈ x0 -p n1 ∨ dups(x0 -p n1) ⊦

• Proof step 10:

  ¬ dups(x0 -p n1), ¬ dups(x0), ¬ a ∈ x0, ∀ n0. ¬ dups(x0 -p n0), a ∈ x0 -p n1 ∨ dups(x0 -p n1) ⊦

Rule argument

Additional information

Used formulas: dups(x0 -p n1)

Proof step 8 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  dups(x0 -p n1), ¬ dups(x0), ¬ a ∈ x0, ∀ n0. ¬ dups(x0 -p n0) ⊦

Rule argument

Additional information

Proof step 9 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n1

Proof step 10 from proof nodups-rmposnodups (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ∈ x0 -p n1, ¬ dups(x0 -p n1), ¬ dups(x0), ¬ a ∈ x0, ∀ n0. ¬ dups(x0 -p n0) ⊦

Rule argument

Additional information

Proof step 11 from proof nodups-rmposnodups (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: rmtoobigpos: ⊦ # x ≤ n → x -p n = x; ⊦ m < n ↔ ¬ n ≤ m; (ss) Used terms: n1, x0, a

Proof step 12 from proof nodups-rmposnodups (previous step) (back to tree)

Lemma rmpos-in