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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x + y from n ≠ (x from n) + y, n ≤ # x ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x + y from n ≠ (x from n) + y, n ≤ # x ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  (a + x0) + y from n ≠ (a + x0 from n) + y, n ≤ #(a + x0), ∀ y, n. ¬(x0 + y from n ≠ (x0 from n) + y ∧ n ≤ # x0) ⊦

Rule argument

Additional information

Used simplifier rules: from-zero-l: ⊦ x from 0 = x; list freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (a ' + x0) + y from n ≠ (a ' + x0 from n) + y, n ≤ 1 + # x0, ∀ y0, n0. x0 + y0 from n0 = (x0 from n0) + y0 ∨ ¬ n0 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ a + x = a ' + x; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  (a ' + x0) + y from n0 +1 ≠ (a ' + x0 from n0 +1) + y, n0 +1 ≤ 1 + # x0, ∀ y0, n0. x0 + y0 from n0 = (x0 from n0) + y0 ∨ ¬ n0 ≤ # x0, ∀ a, x0, y. ¬((a ' + x0) + y from n0 ≠ (a ' + x0 from n0) + y ∧ n0 ≤ 1 + # x0 ∧ (∀ y0, n0. x0 + y0 from n0 = (x0 from n0) + y0 ∨ ¬ n0 ≤ # x0)) ⊦

Rule argument

Additional information

Used simplifier rules: from-zero-l: ⊦ x from 0 = x; nat freely generated by 0, +1;; ⊦ x + y = x + z ↔ y = z; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  x0 + y from n0 ≠ (x0 from n0) + y, n0 ≤ # x0, ∀ y0, n0. x0 + y0 from n0 = (x0 from n0) + y0 ∨ ¬ n0 ≤ # x0, ∀ a, x, y0. (a ' + x) + y0 from n0 = (a ' + x from n0) + y0 ∨ ¬ n0 ≤ 1 + # x ∨ ¬(∀ y0, n0. x + y0 from n0 = (x from n0) + y0 ∨ ¬ n0 ≤ # x) ⊦

Rule argument

Additional information

Used simplifier rules: from-succ-cons-l-lem: ⊦ a ' + x from n + 1 = x from n; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y, n0