Proof step 1 from proof rev-subarray-split-step (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1) ≠ subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0), 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Proof step 2 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

  3 + n0 + k + n + m ≤ # ar, # ( subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)) ≠ #(subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0)) ∨ (∃ n1. ¬ ( n1 < # ( subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)) → ( subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1) )[n1 ] = (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1])) ⊦

Rule argument

Additional information

Used terms: subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1), subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0)

Proof step 3 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ( subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1) )[n1 ] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1], n1 < 2 + n + k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

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 < n0 ⊦ (* n) ≠ m0 + (* n0); (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ # subarray(ar, m, n) = n; (s) ⊦ # rev(x) = # x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 5 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 7:

  ( subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1) )[n1 ] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1], n1 < 2 + n + k + n0, 3 + n0 + k + n + m ≤ # ar, ¬ n1 < # subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) ⊦

• Proof step 56:

  subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1)[n1] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1], n1 < 2 + n + k + n0, n1 < # subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1), 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used terms: subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1), rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1), n1

Proof step 6 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1))[n1 - n + 1] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1], n < n1, n1 < 2 + n + k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

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 < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m < n → n ≠ 0; (s) lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem[natarray] f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ # subarray(ar, m, n) = n; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 8 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  n1 = n2 + n + 1, (rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1))[n2] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1], n1 < 2 + n + k + n0, n < n1, 3 + n0 + k + n + m ≤ # ar, n + 1 ≤ n1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ 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 n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n1, n + 1, n2

Proof step 9 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1))[n2] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + n + 1], 3 + n0 + k + n + m ≤ # ar, n2 ≤ k + n0 ⊦

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) n < n0 ⊦ m + (* n) < m0 + (* n0) ↔ m < m0 + (n0 - n); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) ⊦ m ≤ m + n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)

Proof step 10 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]

• Proof step 12:

  (rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1))[n2] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + n + 1 - # subarray(ar, m + 1, n)], n2 ≤ k + n0, 3 + n0 + k + n + m ≤ # ar, ¬ n2 + n + 1 < # subarray(ar, m + 1, n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ # subarray(ar, m, n) = n; (s) ⊦ ¬ m + 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: subarray(ar, m + 1, n), rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0), n2 + n + 1

Proof step 11 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1))[n2] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + 1], 3 + n0 + k + n + m ≤ # ar, n2 ≤ k + n0 ⊦

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 < m; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ m + n - m = n; (s)

Proof step 13 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 15:

  (rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1))[n2] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + 1], n2 ≤ k + n0, 3 + n0 + k + n + m ≤ # ar, ¬ n2 < # rev(subarray(ar, m + n + 2, k)) ⊦

• Proof step 39:

  rev(subarray(ar, m + n + 2, k))[n2] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + 1], n2 < # rev(subarray(ar, m + n + 2, k)), n2 ≤ k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used terms: rev(subarray(ar, m + n + 2, k)), subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1), n2

Proof step 14 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n2 - k] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + 1], k ≤ n2, n2 ≤ k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

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; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ # subarray(ar, m, n) = n; (s) ⊦ # rev(x) = # x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 16 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  n2 = n1 + k, subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n1] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + 1], 3 + n0 + k + n + m ≤ # ar, n2 ≤ k + n0, k ≤ n2 ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n2, k, n1

Proof step 17 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n1] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[(n1 + k) + 1], 3 + n0 + k + n + m ≤ # ar, n1 ≤ n0 ⊦

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 ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m ≤ m + n; (s)

Proof step 18 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 20:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n1] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[(n1 + k) + 1], n1 ≤ n0, 3 + n0 + k + n + m ≤ # ar, ¬ (n1 + k) + 1 < # rev(subarray(ar, m + n + 1, k + 2)) ⊦

• Proof step 30:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n1] ≠ rev(subarray(ar, m + n + 1, k + 2))[(n1 + k) + 1], (n1 + k) + 1 < # rev(subarray(ar, m + n + 1, k + 2)), n1 ≤ n0, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used terms: rev(subarray(ar, m + n + 1, k + 2)), subarray(ar, n + m + 3 + k, n0), (n1 + k) + 1

Proof step 19 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n1] ≠ subarray(ar, n + m + 3 + k, n0)[n1 + 1 - 2], n1 ≠ 0, 3 + n0 + k + n + m ≤ # ar, n1 ≤ n0 ⊦

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 ↔ m = 0; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ # rev(x) = # x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m + n - n + n1 = m - n1; (s) ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 21 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 22:

  n1 + 1 = n2 + 2, subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n1] ≠ subarray(ar, n + m + 3 + k, n0)[n2], n1 ≠ 0, n1 ≤ n0, 3 + n0 + k + n + m ≤ # ar, 2 ≤ n1 + 1 ⊦

Rule argument

Additional information

Used simplifier rules: n0 < n ⊦ (* n) ≤ m0 + (* n0) ↔ n - n0 ≤ m0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n1 + 1, 2, n2

Proof step 22 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[n2 + 1] ≠ ar[(n + m + 3 + k) + n2], n2 < n0, 1 ≤ n0, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) 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 ≤ m + n; (s) ⊦ m + 1 ≠ 0; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat n0 < n ⊦ (* n) ≤ m0 + (* n0) ↔ n - n0 ≤ m0; (s) n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s)

Proof step 23 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

• Proof step 25:

  ar[m + n + 2 + k, ar[m + n + 1]][(n + m + 2 + k) + n2 + 1] ≠ ar[(n + m + 3 + k) + n2], n2 < n0, n2 + 1 < n0 + 1, 3 + n0 + k + n + m ≤ # ar, 1 ≤ n0, (n0 + 1) + n + m + 2 + k ≤ # ar[m + n + 2 + k, ar[m + n + 1]] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (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 Used terms: ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1, n2 + 1

Proof step 24 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ar[m + n + 2 + k, ar[m + n + 1]][3 + n + m + k + n2] ≠ ar[(n + m + 3 + k) + n2], n2 < n0, 3 + n0 + n + m + k ≤ # ar, 1 ≤ n0, 3 + n0 + k + n + m ≤ # ar ⊦

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 < m + n0 ↔ n < n0; (s) ⊦ # ar[n, a] = # ar; (s)

Proof step 26 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 27:

  3 + n + m + k + n2 ≠ m + n + 2 + k, ar[m + n + 2 + k, ar[m + n + 1]][3 + n + m + k + n2] ≠ ar[(n + m + 3 + k) + n2], n2 < n0, 3 + n0 + k + n + m ≤ # ar, 1 ≤ n0, 3 + n0 + n + m + k ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: 3 + n + m + k + n2 = m + n + 2 + k

Proof step 27 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ar[m + n + 2 + k, ar[m + n + 1]][3 + n + m + k + n2] ≠ ar[(n + m + 3 + k) + n2], n2 < n0, 3 + n0 + n + m + k ≤ # ar, 1 ≤ n0, 3 + n0 + k + n + m ≤ # ar ⊦

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 < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 28 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ m ≠ n → ar[n, a][m] = ar[m]

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 ⊦ m + n = m + n0 ↔ n = n0; (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) Used terms: ar, m + n + 2 + k, ar[m + n + 1], 3 + n + m + k + n2

Proof step 29 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[0] ≠ rev(subarray(ar, m + n + 1, k + 2))[1 + k], 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < 1 ↔ m = 0; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ # rev(x) = # x; (s)

Proof step 31 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ n < # ar → rev(ar)[n] = ar[# ar - n + 1]

• Proof step 33:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[0] ≠ subarray(ar, m + n + 1, k + 2)[# subarray(ar, m + n + 1, k + 2) - (1 + k) + 1], 1 + k < # subarray(ar, m + n + 1, k + 2), 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (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 Used terms: subarray(ar, m + n + 1, k + 2), 1 + k

Proof step 32 from proof rev-subarray-split-step (previous step) (back to tree)

Lemma get-rev

Proof step 33 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1)[0] ≠ subarray(ar, m + n + 1, k + 2)[0], 3 + n0 + k + n + m ≤ # ar ⊦

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 < m + n0 ↔ n < n0; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ m - m = 0; (s) ⊦ m + n - n + n1 = m - n1; (s)

Proof step 34 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

• Proof step 36:

  ar[m + n + 2 + k, ar[m + n + 1]][(n + m + 2 + k) + 0] ≠ subarray(ar, m + n + 1, k + 2)[0], 0 < n0 + 1, 3 + n0 + k + n + m ≤ # ar, (n0 + 1) + n + m + 2 + k ≤ # ar[m + n + 2 + k, ar[m + n + 1]] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (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 terms: ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1, 0

Proof step 35 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  ar[m + n + 1] ≠ subarray(ar, m + n + 1, k + 2)[0], 3 + n0 + k + n + m ≤ # ar, 3 + n0 + n + m + k ≤ # ar ⊦

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) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # ar[n, a] = # ar; (s) m < # ar ⊦ ar[m, a][m] = a; (s) n0 < n ⊦ ¬ m + (* n) ≤ (* n0); (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 37 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

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 ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) Used terms: ar, m + n + 1, k + 2, 0

Proof step 38 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  rev(subarray(ar, m + n + 2, k))[n2] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n2 + 1], n2 < k, n2 ≤ k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # subarray(ar, m, n) = n; (s) ⊦ # rev(x) = # x; (s)

Proof step 40 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 42:

  rev(subarray(ar, m + n + 2, k))[n2] ≠ rev(subarray(ar, m + n + 1, k + 2))[n2 + 1], n2 < k, n2 + 1 < # rev(subarray(ar, m + n + 1, k + 2)), 3 + n0 + k + n + m ≤ # ar, n2 ≤ k + n0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ # rev(x) = # x; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ m < m0 ∧ n < n0 → (m + n < m0 + n0 ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: rev(subarray(ar, m + n + 1, k + 2)), subarray(ar, n + m + 3 + k, n0), n2 + 1

Proof step 41 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  rev(subarray(ar, m + n + 2, k))[n2] ≠ rev(subarray(ar, m + n + 1, k + 2))[n2 + 1], n2 < k, n2 ≤ k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

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 ⊦ a < b → (b < a ↔ false); (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) n < n0 ⊦ m + (* n) < m0 + (* n0) ↔ m < m0 + (n0 - n); (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ # rev(x) = # x; (s)

Proof step 43 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ n < # ar → rev(ar)[n] = ar[# ar - n + 1]

• Proof step 45:

  subarray(ar, m + n + 2, k)[# subarray(ar, m + n + 2, k) - n2 + 1] ≠ rev(subarray(ar, m + n + 1, k + 2))[n2 + 1], n2 < k, n2 < # subarray(ar, m + n + 2, k), 3 + n0 + k + n + m ≤ # ar, n2 ≤ k + n0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: subarray(ar, m + n + 2, k), n2

Proof step 44 from proof rev-subarray-split-step (previous step) (back to tree)

Lemma get-rev

Proof step 45 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  subarray(ar, m + n + 2, k)[k - n2 + 1] ≠ rev(subarray(ar, m + n + 1, k + 2))[n2 + 1], n2 < k, n2 ≤ k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s)

Proof step 46 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 47:

  k = n1 + n2 + 1, subarray(ar, m + n + 2, k)[n1] ≠ rev(subarray(ar, m + n + 1, k + 2))[n2 + 1], n2 < k, 3 + n0 + k + n + m ≤ # ar, n2 ≤ k + n0, n2 + 1 ≤ k ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ 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 n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: k, n2 + 1, n1

Proof step 47 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  subarray(ar, m + n + 2, n1 + n2 + 1)[n1] ≠ rev(subarray(ar, m + n + 1, 3 + n1 + n2))[n2 + 1], 4 + n0 + n1 + n2 + n + m ≤ # ar ⊦

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

Proof step 48 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

• Proof step 50:

  ar[(m + n + 2) + n1] ≠ rev(subarray(ar, m + n + 1, 3 + n1 + n2))[n2 + 1], n1 < n1 + n2 + 1, 4 + n0 + n1 + n2 + n + m ≤ # ar, (n1 + n2 + 1) + m + n + 2 ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) n0 < n ⊦ ¬ m + (* n) < (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: ar, m + n + 2, n1 + n2 + 1, n1

Proof step 49 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  ar[(m + n + 2) + n1] ≠ rev(subarray(ar, m + n + 1, 3 + n1 + n2))[n2 + 1], 4 + n0 + n1 + n2 + n + m ≤ # ar, 3 + n1 + n2 + m + n ≤ # ar ⊦

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

Proof step 51 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ n < # ar → rev(ar)[n] = ar[# ar - n + 1]

• Proof step 53:

  ar[(m + n + 2) + n1] ≠ subarray(ar, m + n + 1, 3 + n1 + n2)[# subarray(ar, m + n + 1, 3 + n1 + n2) - (n2 + 1) + 1], n2 + 1 < # subarray(ar, m + n + 1, 3 + n1 + n2), 3 + n1 + n2 + m + n ≤ # ar, 4 + n0 + n1 + n2 + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: subarray(ar, m + n + 1, 3 + n1 + n2), n2 + 1

Proof step 52 from proof rev-subarray-split-step (previous step) (back to tree)

Lemma get-rev

Proof step 53 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  ar[(m + n + 2) + n1] ≠ subarray(ar, m + n + 1, 3 + n1 + n2)[1 + n1], 4 + n0 + n1 + n2 + n + m ≤ # ar, 3 + n1 + n2 + m + n ≤ # ar ⊦

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 < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + n - n + n1 = m - n1; (s)

Proof step 54 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

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 ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) Used terms: ar, m + n + 1, 3 + n1 + n2, 1 + n1

Proof step 55 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1)[n1] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1], n1 < 2 + n + k + n0, 3 + n0 + k + n + m ≤ # ar, n1 ≤ n ⊦

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) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 57 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 59:

  subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1)[n1] ≠ (subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[n1], n1 < 2 + n + k + n0, n1 ≤ n, 3 + n0 + k + n + m ≤ # ar, ¬ n1 < # subarray(ar, m + 1, n) ⊦

• Proof step 71:

  subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1)[n1] ≠ subarray(ar, m + 1, n)[n1], n1 < 2 + n + k + n0, n1 < # subarray(ar, m + 1, n), n1 ≤ n, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used terms: subarray(ar, m + 1, n), rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0), n1

Proof step 58 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 59 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1)[n] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[0], 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m - m = 0; (s) lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem[natarray] ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ # subarray(ar, m, n) = n; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 60 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 61:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

• Proof step 62:

  ar[m + n + 1, ar[m + n + 2 + k]][(m + 1) + n] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[0], n < n + 1, 3 + n0 + k + n + m ≤ # ar, (n + 1) + m + 1 ≤ # ar[m + n + 1, ar[m + n + 2 + k]] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ a < a; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) n0 < n ⊦ ¬ m + (* n) < (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1, n

Proof step 61 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 62 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  ar[m + n + 2 + k] ≠ (rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0))[0], 3 + n0 + k + n + m ≤ # ar, 2 + n + m ≤ # ar ⊦

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 ⊦ ¬ a < a; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ # ar[n, a] = # ar; (s) m < # ar ⊦ ar[m, a][m] = a; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 63 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 65:

  ar[m + n + 2 + k] ≠ rev(subarray(ar, m + n + 1, k + 2))[0], 0 < # rev(subarray(ar, m + n + 1, k + 2)), 2 + n + m ≤ # ar, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ # rev(x) = # x; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: rev(subarray(ar, m + n + 1, k + 2)), subarray(ar, n + m + 3 + k, n0), 0

Proof step 64 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 65 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  ar[m + n + 2 + k] ≠ rev(subarray(ar, m + n + 1, k + 2))[0], 3 + n0 + k + n + m ≤ # ar, 2 + n + m ≤ # ar ⊦

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 < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ # rev(x) = # x; (s)

Proof step 66 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ n < # ar → rev(ar)[n] = ar[# ar - n + 1]

• Proof step 68:

  ar[m + n + 2 + k] ≠ subarray(ar, m + n + 1, k + 2)[# subarray(ar, m + n + 1, k + 2) - 0 + 1], 0 < # subarray(ar, m + n + 1, k + 2), 2 + n + m ≤ # ar, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: subarray(ar, m + n + 1, k + 2), 0

Proof step 67 from proof rev-subarray-split-step (previous step) (back to tree)

Lemma get-rev

Proof step 68 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  ar[m + n + 2 + k] ≠ subarray(ar, m + n + 1, k + 2)[1 + k], 3 + n0 + k + n + m ≤ # ar, 2 + n + m ≤ # ar ⊦

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 < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)

Proof step 69 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 70:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

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; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) n < n0 ⊦ (* n) < m0 + (* n0); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) Used terms: ar, m + n + 1, k + 2, 1 + k

Proof step 70 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 71 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1)[n1] ≠ ar[(m + 1) + n1], n1 < n, n1 < 2 + n + k + n0, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s) ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 72 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 73:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

• Proof step 74:

  ar[m + n + 1, ar[m + n + 2 + k]][(m + 1) + n1] ≠ ar[(m + 1) + n1], n1 < 2 + n + k + n0, n1 < n, n1 < n + 1, 3 + n0 + k + n + m ≤ # ar, (n + 1) + m + 1 ≤ # ar[m + n + 1, ar[m + n + 2 + k]] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n → ¬ n < m; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) n0 < n ⊦ ¬ m + (* n) < (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1, n1

Proof step 73 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma

Proof step 74 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  ar[m + n + 1, ar[m + n + 2 + k]][(m + 1) + n1] ≠ ar[(m + 1) + n1], n1 < n, n1 < 2 + n + k + n0, 3 + n0 + k + n + m ≤ # ar, 2 + n + m ≤ # ar ⊦

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 ⊦ a < b → (b < a ↔ false); (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ # ar[n, a] = # ar; (s)

Proof step 75 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 76:

  (m + 1) + n1 ≠ m + n + 1, ar[m + n + 1, ar[m + n + 2 + k]][(m + 1) + n1] ≠ ar[(m + 1) + n1], n1 < 2 + n + k + n0, n1 < n, 2 + n + m ≤ # ar, 3 + n0 + k + n + m ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem[natarray] lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used formulas: (m + 1) + n1 = m + n + 1

Proof step 76 from proof rev-subarray-split-step (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  ar[m + n + 1, ar[m + n + 2 + k]][(m + 1) + n1] ≠ ar[(m + 1) + n1], n1 ≠ n, n1 < n, n1 < 2 + n + k + n0, 3 + n0 + k + n + m ≤ # ar, 2 + n + m ≤ # ar ⊦

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

Proof step 77 from proof rev-subarray-split-step (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

  ⊦ m ≠ n → ar[n, a][m] = ar[m]

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 ⊦ m + n = m + n0 ↔ n = n0; (s) Used terms: ar, m + n + 1, ar[m + n + 2 + k], (m + 1) + n1

Proof step 78 from proof rev-subarray-split-step (previous step) (back to tree)

A spec-lemma