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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(x0 < a + x ↔ x0 = x ∨ x0 < x) ⊦

Rule argument

Additional information

Proof step 2 from proof less-add (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:

  ¬(x0 < copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] ↔ x0 = x ∨ x0 < x) ⊦

Rule argument

Additional information

Used terms: a, x

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

A spec-lemma

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

User applied rule cut formula

And obtained the following new goals

• Proof step 5:

  x0 = x, ¬(x0 < copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] ↔ x0 = x ∨ x0 < x) ⊦

• Proof step 8:

  ¬(x0 < copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] ↔ x0 = x ∨ x0 < x), x0 ≠ x ⊦

Rule argument

Additional information

Used formulas: x0 = x

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)

• Proof step 11:

  ¬ ( # x0 < # copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] ∧ x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a], # copy(x, 0, mkarray(# x + 1), 1, # x)[0 := a] - # x0, # x0) ↔ x0 < x), x0 ≠ x ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ¬(¬ # x < # x0 ∧ x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), # x + 1 - # x0, # x0) ↔ x0 < x), x0 ≠ x ⊦

Rule argument

Additional information

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

Proof step 12 from proof less-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)

• Proof step 14:

  ¬ ( ¬ # x < # x0 ∧ x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), # x + 1 - # x0, # x0) ↔ # x0 < # x ∧ x0 = subarray(x, # x - # x0, # x0)), x0 ≠ x ⊦

Rule argument

Additional information

Used terms: x0, x

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

A spec-lemma

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  # x = n0 + # x0, ¬ ( ¬ # x < # x0 ∧ x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), # x + 1 - # x0, # x0) ↔ # x0 < # x ∧ x0 = subarray(x, n0, # x0)), x0 ≠ x, # x0 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m < n → ¬ m + m0 < n; (s) n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m + m0 ≤ m ↔ m0 = 0; (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 ↔ ¬ n ≤ m; (ss) m0 + m1 ≤ n1, m0 + m1 ≤ # ar ⊦ subarray(copy(ar0, n0, ar, n1, n2), m0, m1) = subarray(ar, m0, m1); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x, # x0, n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  # x = n0 + # x0, ¬ ( x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), (# x - # x0) + 1, # x0) ↔ # x0 < # x ∧ x0 = subarray(x, n0, # x0)), x0 ≠ x, # x0 ≤ # 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 ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  # x = n0 + # x0, # x = n1 + # x0, ¬(x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), n1 + 1, # x0) ↔ # x0 < # x ∧ x0 = subarray(x, n0, # x0)), x0 ≠ x, # x0 ≤ # x ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  # x = n1 + # x0, ¬(x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), n1 + 1, # x0) ↔ # x0 < # x ∧ x0 = subarray(x, n1, # x0)), x0 ≠ x, # x0 ≤ # 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 eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 19:

  # x = n1 + # x0, ¬(x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), n1 + 1, # x0) ↔ # x0 < # x ∧ x0 = subarray(x, n1, # x0)), x0 ≠ x, # x0 < # x, # x0 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ m = m + n ↔ n = 0; (s) ⊦ m ≤ m; (s) ⊦ # mkarray(n) = n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic m1 + n ≤ # ar1 ⊦ subarray(copy(ar0, m0, ar1, m1, n), m1, n) = subarray(ar0, m0, n); (s) # ar = n ⊦ subarray(ar, 0, n) = ar; (s) Used formulas: # x0 < # x

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  # x = n1 + # x0, ¬(x0 = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), n1 + 1, # x0) ↔ x0 = subarray(x, n1, # x0)), n1 ≠ 0, x0 ≠ x, # x0 < # 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 < m + n ↔ n ≠ 0; (s) ⊦ 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 ⊦ m < n → m ≤ n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  # x = n1 + # x0, n1 ≠ 0, x0 ≠ x, # x0 < # x ⊦ # x0 = # subarray(copy(x, 0, mkarray(# x + 1), 1, # x), n1 + 1, # x0) ∧ (∀ n. n < # x0 → x0[n] = subarray(copy(x, 0, mkarray(# x + 1), 1, # x), n1 + 1, # x0)[n]) ↔ x0 = subarray(x, n1, # x0)

Rule argument

Additional information

Used terms: x0, subarray(copy(x, 0, mkarray(# x + 1), 1, # x), n1 + 1, # x0)

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

A spec-lemma

Proof step 22 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # x = n1 + # x0, n1 ≠ 0, x0 ≠ x, # x0 < # x ⊦ (∀ n. n < # x0 → x0[n] = copy(x, 0, mkarray(# x + 1), 1, # x)[(n1 + 1) + n]) ↔ x0 = subarray(x, n1, # x0)

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 23 from proof less-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  # x = n1 + # x0, n1 ≠ 0, x0 ≠ x, # x0 < # x ⊦ (∀ n. n < # x0 → x0[n] = copy(x, 0, mkarray(# x + 1), 1, # x)[(n1 + 1) + n]) ↔ # x0 = # subarray(x, n1, # x0) ∧ (∀ n. n < # x0 → x0[n] = subarray(x, n1, # x0)[n])

Rule argument

Additional information

Used terms: x0, subarray(x, n1, # x0)

Proof step 24 from proof less-add (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 26 from proof less-add (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 27:

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

• Proof step 36:

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

Rule argument

Additional information

Proof step 27 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

Proof step 28 from proof less-add (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Used terms: n

Proof step 29 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Proof step 30 from proof less-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

  # x = n1 + # x0, x0[n] = ((n1 + 1) + n < 1 ∨ 1 + # x ≤ (n1 + 1) + n ⊃ mkarray(# x + 1)[(n1 + 1) + n];x[((n1 + 1) + n) + 0 - 1]), x0[n] ≠ x[n1 + n], n1 ≠ 0, x0 ≠ x, n < # x, # x0 < # x, n < # x0, n + 1 < # x, (n1 + 1) + n < # mkarray(# x + 1), ∀ n. n < # x0 → x0[n] = copy(x, 0, mkarray(# x + 1), 1, # x)[(n1 + 1) + n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # mkarray(n) = n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (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, (n1 + 1) + n, x

Proof step 31 from proof less-add (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # x = n1 + # x0, x0[n] = (# x ≤ n1 + n ⊃ mkarray(# x + 1)[(n1 + 1) + n];x[n1 + n]), x0[n] ≠ x[n1 + n], n1 ≠ 0, x0 ≠ x, n + 1 < # x, n < # x0, # x0 < # x, n < # x, ∀ n. n < # x0 → x0[n] = copy(x, 0, mkarray(# x + 1), 1, # x)[(n1 + 1) + 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 = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ # mkarray(n) = n; (s) ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ ¬ m < n → ¬ m + m0 < n; (s)

Proof step 33 from proof less-add (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 34:

  # x = n1 + # x0, x0[n] = (# x ≤ n1 + n ⊃ mkarray(# x + 1)[(n1 + 1) + n];x[n1 + n]), x0[n] ≠ x[n1 + n], n1 ≠ 0, x0 ≠ x, n < # x, # x0 < # x, n < # x0, n + 1 < # x, # x ≤ n1 + n, ∀ n. n < # x0 → x0[n] = copy(x, 0, mkarray(# x + 1), 1, # x)[(n1 + 1) + n] ⊦

Rule argument

Additional information

Used formulas: # x ≤ n1 + n

Proof step 34 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # x = n1 + # x0, x0[n] = mkarray(# x + 1)[(n1 + 1) + n], x0[n] ≠ x[n1 + n], n1 ≠ 1, n1 ≠ 0, x0 ≠ x, # x0 < n1 + n, n + 1 < # x, n < # x0, # x0 < # x, n < # x, # x ≤ n1 + n, ∀ n. n < # x0 → x0[n] = copy(x, 0, mkarray(# x + 1), 1, # x)[(n1 + 1) + 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 ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat

Proof step 35 from proof less-add (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (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

Proof step 36 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

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

Rule argument

Additional information

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

Proof step 37 from proof less-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

• Proof step 39:

  # x = n1 + # x0, x0[n] ≠ ((n1 + 1) + n < 1 ∨ 1 + # x ≤ (n1 + 1) + n ⊃ mkarray(# x + 1)[(n1 + 1) + n];x[((n1 + 1) + n) + 0 - 1]), n1 ≠ 0, x0 ≠ x, n < # x, # x0 < # x, n < # x0, n + 1 < # x, (n1 + 1) + n < # mkarray(# x + 1), ∀ n. n < # x0 → x0[n] = x[n1 + n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # mkarray(n) = n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (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, (n1 + 1) + n, x

Proof step 38 from proof less-add (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  # x = n1 + # x0, x0[n] ≠ (# x ≤ n1 + n ⊃ mkarray(# x + 1)[(n1 + 1) + n];x[n1 + n]), n1 ≠ 0, x0 ≠ x, n + 1 < # x, n < # x0, # x0 < # x, n < # x, ∀ n. n < # x0 → x0[n] = x[n1 + 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 = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ # mkarray(n) = n; (s) ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ ¬ m < n → ¬ m + m0 < n; (s)

Proof step 40 from proof less-add (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 41:

  # x = n1 + # x0, x0[n] ≠ mkarray(# x + 1)[(n1 + 1) + n], n1 ≠ 0, x0 ≠ x, n < # x, # x0 < # x, n < # x0, n + 1 < # x, # x ≤ n1 + n, ∀ n. n < # x0 → x0[n] = x[n1 + n] ⊦

• Proof step 43:

  # x = n1 + # x0, x0[n] ≠ x[n1 + n], n1 ≠ 0, x0 ≠ x, n < # x, # x0 < # x, n < # x0, n + 1 < # x, ¬ # x ≤ n1 + n, ∀ n. n < # x0 → x0[n] = x[n1 + n] ⊦

Rule argument

Additional information

Proof step 41 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  # x = n1 + # x0, x0[n] ≠ mkarray(# x + 1)[(n1 + 1) + n], n1 ≠ 1, n1 ≠ 0, x0 ≠ x, # x0 < n1 + n, n + 1 < # x, n < # x0, # x0 < # x, n < # x, # x ≤ n1 + n, ∀ n. n < # x0 → x0[n] = x[n1 + 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 ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat

Proof step 42 from proof less-add (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (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

Proof step 43 from proof less-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  # x = n1 + # x0, x0[n] ≠ x[n1 + n], n1 ≠ 0, x0 ≠ x, n + 1 < # x, n < # x0, # x0 < # x, n < # x, ∀ n. n < # x0 → x0[n] = x[n1 + 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 = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 44 from proof less-add (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n