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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (b + x)[n + 1 := a] ≠ b + x[n := a] ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ a + ar = copy(ar, 0, mkarray(# ar + 1), 1, # ar)[0 := a]

• Proof step 4:

  (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a] ≠ b + x[n := a] ⊦

Rule argument

Additional information

Used terms: b, x

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ a + ar = copy(ar, 0, mkarray(# ar + 1), 1, # ar)[0 := a]

• Proof step 6:

  (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a] ≠ copy(x[n := a], 0, mkarray(# x[n := a] + 1), 1, # x[n := a])[0 := b] ⊦

Rule argument

Additional information

Used terms: b, x[n := a]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a] ≠ copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n := a] = # ar; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])

• Proof step 9:

  # (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a] ≠ # copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b] ∨ (∃ n0. ¬ ( n0 < # (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a] → ((copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a])[n0] = (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n0])) ⊦

Rule argument

Additional information

Used terms: (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a], copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ((copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a])[n0] ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n0], n0 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 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) ⊦ # mkarray(n) = n; (s) ⊦ # copy(ar, m, ar0, m0, n) = # ar0; (s) ⊦ # ar[n := a] = # ar; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 11:

  n0 = n + 1, ((copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a])[n0] ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n0], n0 ≤ # x ⊦

• Proof step 19:

  ((copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1 := a])[n0] ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n0], n0 ≠ n + 1, n0 ≤ # x ⊦

Rule argument

Additional information

Used formulas: n0 = n + 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  a ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1], n < # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (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 < # ar ⊦ (ar[m := a])[m] = a; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ # mkarray(n) = n; (s) ⊦ # copy(ar, m, ar0, m0, n) = # ar0; (s) ⊦ # ar[n := a] = # ar; (s)

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 13:

  n + 1 ≠ 0, a ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1], n < # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: n + 1 = 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  a ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n + 1], n < # x ⊦

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 + 1 ≠ 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ m ≠ n → (ar[n := a])[m] = ar[m]

• Proof step 16:

  n + 1 ≠ 0, a ≠ copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[n + 1], n < # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: copy(x[n := a], 0, mkarray(# x + 1), 1, # x), 0, b, n + 1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  a ≠ copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[n + 1], n < # x ⊦

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 + 1 ≠ 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0])

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m < n → ¬ m + m0 < n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < # ar → (ar[m := a])[m] = a; (s) ⊦ # mkarray(n) = n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) Used terms: 1, 0, mkarray(# x + 1), # x, n + 1, x[n := a]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n0] ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n0], n0 ≠ n + 1, n0 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (ar[n := a])[m] = ar[m]; (s)

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 21:

  (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := b])[n0] ≠ (copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[0 := b])[n0], n0 ≠ 0, n0 ≠ n + 1, n0 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # copy(ar, m, ar0, m0, n) = # ar0; (s) ⊦ # mkarray(n) = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic m < # ar ⊦ (ar[m := a])[m] = a; (s) Used formulas: n0 = 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  copy(x, 0, mkarray(# x + 1), 1, # x)[n0] ≠ copy(x[n := a], 0, mkarray(# x + 1), 1, # x)[n0], n0 ≠ 0, n0 ≠ n + 1, n0 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (ar[n := a])[m] = ar[m]; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0])

• Proof step 24:

  copy(x, 0, mkarray(# x + 1), 1, # x)[n0] ≠ (n0 < 1 ∨ 1 + # x ≤ n0 ⊃ mkarray(# x + 1)[n0];(x[n := a])[n0 + 0 - 1]), n0 ≠ 0, n0 ≠ n + 1, n0 < # mkarray(# x + 1), n0 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # mkarray(n) = n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ n → (n < m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: 1, 0, mkarray(# x + 1), # x, n0, x[n := a]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  x[n0 - 1] ≠ (x[n := a])[n0 - 1], n0 ≠ 0, n0 ≠ n + 1, n0 ≤ # x ⊦

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 ≤ n → (n < m ↔ false); (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ # mkarray(n) = n; (s) ⊦ n + 0 = n; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0]); (s)

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

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

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