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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  σ from n ≠ σ[n] + (σ from n + 1), ⌜n⌝ < # σ ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  σ from n ≠ ⌜σ[n] '⌝ + (σ from n + 1), ⌜n⌝ < # σ ⊦

Rule argument

Additional information

Used simplifier rules: cons-append: ⊦ a + σ = ⌜a '⌝ + σ;

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ⌜x⌝ from n ≠ ⌜⌜x⌝ [n] '⌝ + (⌜x⌝ from n + 1), ⌜n⌝ < # ⌜x⌝ ⊦

• Proof step 13:

  ⌜nf⌝ from n ≠ ⌜⌜nf⌝ [n] '⌝ + (⌜nf⌝ from n + 1), ⌜n⌝ < # ⌜nf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: stream freely generated by ⌜ ⌝, ⌜ ⌝;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  x[n] ' + (x from n + 1) ≠ x from n, x ≠ [], n < # x ⊦

Rule argument

Additional information

Used simplifier rules: sel-fin: ⊦ ⌜x⌝ [n] = x[n]; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; eq-stream-to-list-2-1: ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  (a + x0)[n] ' + (a + x0 from n + 1) ≠ a + x0 from n, a + x0 ≠ [], n < #(a + x0), ∀ n. ¬(x0[n] ' + (x0 from n + 1) ≠ x0 from n ∧ x0 ≠ [] ∧ n < # x0) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  n ≠ 0 ⊦ (a ' + x)[(* n)] = x[n -1]

• Proof step 9:

  x0[n -1] ' + (x0 from n) ≠ a ' + x0 from n, n ≠ 0, n ≤ # x0, ∀ n0. x0[n0] ' + (x0 from n0 + 1) = x0 from n0 ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: from-zero-l: ⊦ x from 0 = x; ⊦ (a ' + x)[0] = a; (s) ⊦ x + y = x + z ↔ y = z; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n, x0, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  x0[n - 1] ' + (x0 from n) ≠ a ' + x0 from n, n ≠ 0, n ≤ # x0, ∀ n0. x0[n0] ' + (x0 from n0 + 1) = x0 from n0 ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  n = n1 + 1, x0[n1] ' + (x0 from n) ≠ a ' + x0 from n, n ≠ 0, n ≤ # x0, ∀ n0. x0[n0] ' + (x0 from n0 + 1) = x0 from n0 ∨ 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 11 from proof from-succ (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  x0[n1] ' + (x0 from n1 + 1) ≠ x0 from n1, x0 ≠ [], n1 < # x0, ∀ n0. x0[n0] ' + (x0 from n0 + 1) = x0 from n0 ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

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

Proof step 12 from proof from-succ (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 13 from proof from-succ (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ⌜nf from n⌝ ≠ ⌜nf(n) '⌝ + ⌜nf from n + 1⌝ ⊦

Rule argument

Additional information

Used simplifier rules: sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; size-inf: ⊦ # ⌜nf⌝ = ∞; ⊦ ⌜m⌝ < ∞; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ nf from n = (λ m. nf(n + m))

• Proof step 16:

  ⌜nf from n⌝ ≠ ⌜nf(n) '⌝ + ⌜λ m. nf((n + 1) + m)⌝ ⊦

Rule argument

Additional information

Used terms: n + 1, nf

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

Lemma from-nf

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ ⌜a '⌝ + ⌜nf⌝ = ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝

• Proof step 18:

  ⌜nf from n⌝ ≠ ⌜λ n0. (n0 = 0 ⊃ nf(n);nf((n + 1) + n0 -1))⌝ ⊦

Rule argument

Additional information

Used terms: λ m. nf((n + 1) + m), nf(n)

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

Lemma one-inf

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  nf(n0 + n) ≠ (n0 = 0 ⊃ nf(n);nf((n + 1) + (n0 - 1))) ⊦

Rule argument

Additional information

Used simplifier rules: get-from-inf: ⊦ ((nf from n))(m) = nf(m + n); ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s) ⊦ n -1 = n - 1; (s)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 20:

  n0 ≠ 0, nf(n0 + n) ≠ nf((n + 1) + (n0 - 1)) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  n0 ≠ 0, nf(n0 + n) ≠ nf((n + 1) + (n0 - 1)) ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n0, m