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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(a + x = a0 + x0 ↔ a = a0 ∧ x = x0) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  a + x = a0 + x0 ⊦ a = a0 ∧ x = x0

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  a + x = copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0] ⊦ a = a0 ∧ x = x0

Rule argument

Additional information

Used terms: a0, x0

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] = copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0] ⊦ a = a0 ∧ x = x0

Rule argument

Additional information

Used terms: a, x

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

A spec-lemma

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] = copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0], x ≠ x0 ⊦ a = a0 ∧ x = x0

Rule argument

Additional information

Used simplifier rules: ⊦ ar[n := a] = ar[n := b] ↔ n < # ar → a = b; (s) ⊦ # 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 Used formulas: x = x0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  # copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] = # copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0], x ≠ x0, ∀ n. n < # copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] → (copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a])[n] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n] ⊦

Rule argument

Additional information

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

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

A spec-lemma

Proof step 11 from proof inj-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # x = # x0, x ≠ x0, ∀ n. ¬ # x0 < n → (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n] ⊦

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 + 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 12 from proof inj-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

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

Rule argument

Additional information

Used terms: x, x0

Proof step 13 from proof inj-add (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # x = # x0, x[n] ≠ x0[n], n < # x0, ∀ n. ¬ # x0 < n → (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

User applied rule all left

And obtained the following new goals

• Proof step 16:

  # x = # x0, x[n] ≠ x0[n], n < # x0, ¬ # x0 < n + 1 → (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n + 1] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n + 1], ∀ n. ¬ # x0 < n → (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n] ⊦

Rule argument

Additional information

Used terms: n + 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # x = # x0, (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n + 1] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n + 1], x[n] ≠ x0[n], n < # x0, ∀ n. ¬ # x0 < n → (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n] ⊦

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 + 1 ↔ ¬ n < m; (s)

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 18:

  # x = # x0, (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n + 1] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n + 1], n + 1 ≠ 0, x[n] ≠ x0[n], n < # x0, ∀ n. ¬ # x0 < n → (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n] ⊦

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 18 from proof inj-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # x = # x0, copy(x, 0, mkarray(# x0 + 1), 1, # x0)[n + 1] = copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[n + 1], x[n] ≠ x0[n], n < # x0, ∀ n. ¬ # x0 < n → (copy(x, 0, mkarray(# x0 + 1), 1, # x0)[0 := a])[n] = (copy(x0, 0, mkarray(# x0 + 1), 1, # x0)[0 := a0])[n] ⊦

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) ⊦ m ≠ n → (ar[n := a])[m] = ar[m]; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

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

A spec-lemma