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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #(x from n) ≠ # x - n, ¬ # x < n ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  #(x from n) ≠ # x - n, n ≤ # x ⊦

Rule argument

Additional information

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

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  # x = n0 + n, #(x from n) ≠ n0, n ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x, n, n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # x = n0 + n, #(x from n) ≠ n0 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  # x = n0 + n1 +1, #(x from n1 +1) ≠ n0, ∀ x, n0. ¬(# x = n0 + n1 ∧ #(x from n1) ≠ n0) ⊦

Rule argument

Additional information

Used simplifier rules: from-zero-l: ⊦ x from 0 = x; nat freely generated by 0, +1;; ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # x = n0 + n1 + 1, #(x from n1 + 1) ≠ n0, ∀ x0, n. # x0 ≠ n + n1 ∨ #(x0 from n1) = n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

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

User applied rule structural induction

And obtained the following new goals

• Proof step 8:

  #(a + x0) = n0 + n1 + 1, #(a + x0 from n1 + 1) ≠ n0, ∀ x0, n. # x0 ≠ n + n1 ∨ #(x0 from n1) = n, ∀ n0, n1. ¬(# x0 = n0 + n1 + 1 ∧ #(x0 from n1 + 1) ≠ n0 ∧ (∀ x0, n. # x0 ≠ n + n1 ∨ #(x0 from n1) = n)) ⊦

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # x0 = n0 + n1, #(x0 from n1) ≠ n0, ∀ x0, n. # x0 ≠ n + n1 ∨ #(x0 from n1) = n, ∀ n, n2. n0 + n1 ≠ n + n2 + 1 ∨ #(x0 from n2 + 1) = n ∨ ¬(∀ x0, n. # x0 ≠ n + n2 ∨ #(x0 from n2) = n) ⊦

Rule argument

Additional information

Used simplifier rules: from-succ-cons-l-lem: ⊦ a ' + x from n + 1 = x from n; a: ⊦ (x + y) + z = x + y + z; from specification list 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 + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x0, n0