Proof step 1 from proof remains-ordered-by-swap (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # ar1 = n0 + m + 1, n0 ≠ 0, ar1[m] < ar1[j], j < # ar1, m < j, ordered≤(rev(subarray(ar1, m + 1, n0))), ¬ ordered≤(rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))), ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Proof step 2 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # ar1 = n0 + m + 1, ar1 ≠ [], n0 ≠ 0, m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], ordered≤(rev(subarray(ar1, m + 1, n0))), j ≤ n0 + m, ¬ ordered≤(rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))), ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 3 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ordered≤(x) ↔ (∀ m, n. m ≤ n ∧ n < # x → ¬ x[n] < x[m])

• Proof step 5:

  # ar1 = n0 + m + 1, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, j ≤ n0 + m, ¬ ordered≤(rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))), ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m], ∀ m0, n. m0 ≤ n ∧ n < # rev(subarray(ar1, m + 1, n0)) → ¬ rev(subarray(ar1, m + 1, n0))[n] < rev(subarray(ar1, m + 1, n0))[m0] ⊦

Rule argument

Additional information

Used terms: rev(subarray(ar1, m + 1, n0))

Proof step 4 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # ar1 = n0 + m + 1, ar1 ≠ [], n0 ≠ 0, m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], j ≤ n0 + m, ¬ ordered≤(rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))), ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m], ∀ m0, n. m0 ≤ n ∧ n < n0 → ¬ rev(subarray(ar1, m + 1, n0))[n] < rev(subarray(ar1, m + 1, n0))[m0] ⊦

Rule argument

Additional information

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

Proof step 6 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ordered≤(x) ↔ (∀ m, n. m ≤ n ∧ n < # x → ¬ x[n] < x[m])

• Proof step 8:

  # ar1 = n0 + m + 1, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, j ≤ n0 + m, ∀ m0, n. m0 ≤ n ∧ n < n0 → ¬ rev(subarray(ar1, m + 1, n0))[n] < rev(subarray(ar1, m + 1, n0))[m0], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m], ∃ m0, n. ¬ ( m0 ≤ n ∧ n < # rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0)) → ¬ rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[n] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[m0]) ⊦

Rule argument

Additional information

Used terms: rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))

Proof step 7 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # ar1 = n0 + m + 1, ar1 ≠ [], m0 < n0, n < n0, rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[n] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[m0], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, m0 ≤ n, j ≤ n0 + m, ∀ m0, n. m0 ≤ n ∧ n < n0 → ¬ rev(subarray(ar1, m + 1, n0))[n] < rev(subarray(ar1, m + 1, n0))[m0], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

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

Proof step 9 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  # ar1 = n0 + m + 1, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[n] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[m0], n < n0, m0 < n0, j ≤ n0 + m, m0 ≤ n, m0 ≤ n ∧ n < n0 → ¬ rev(subarray(ar1, m + 1, n0))[n] < rev(subarray(ar1, m + 1, n0))[m0], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used terms: m0, n

Proof step 10 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # ar1 = n0 + m + 1, ar1 ≠ [], m0 < n0, n < n0, rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[n] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[m0], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, m0 ≤ n, j ≤ n0 + m, rev(subarray(ar1, m + 1, n0))[m0] ≤ rev(subarray(ar1, m + 1, n0))[n], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 11 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  # ar1 = n0 + m + 1, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0)[# subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0) - n + 1] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[m0], n < n0, m0 < n0, n < # subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0), rev(subarray(ar1, m + 1, n0))[m0] ≤ rev(subarray(ar1, m + 1, n0))[n], j ≤ n0 + m, m0 ≤ n, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0), n

Proof step 12 from proof remains-ordered-by-swap (previous step) (back to tree)

Lemma get-rev

Proof step 13 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  # ar1 = n0 + m + 1, ar1 ≠ [], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, m0 < n0, n < n0, subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0)[n0 - n + 1] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[m0], m0 ≤ n, j ≤ n0 + m, rev(subarray(ar1, m + 1, n0))[m0] ≤ rev(subarray(ar1, m + 1, n0))[n], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

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

Proof step 14 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  # ar1 = n0 + m + 1, n0 = n1 + n + 1, ar1 ≠ [], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0)[n1] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))[m0], n < n0, m0 < n0, m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], rev(subarray(ar1, m + 1, n0))[m0] ≤ rev(subarray(ar1, m + 1, n0))[n], j ≤ n0 + m, m0 ≤ n, n + 1 ≤ n0, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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: n0, n + 1, n1

Proof step 15 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  # ar1 = 2 + n1 + n + m, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1)[n1] < rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1))[m0], m0 ≤ n1 + n, rev(subarray(ar1, m + 1, n1 + n + 1))[m0] ≤ rev(subarray(ar1, m + 1, n1 + n + 1))[n], j ≤ (n1 + n + 1) + m, m0 ≤ n, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 16 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  # ar1 = 2 + n1 + n + m, ar1 ≠ [], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1)[# subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1) - m0 + 1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, m0 < # subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1), m0 ≤ n, j ≤ (n1 + n + 1) + m, rev(subarray(ar1, m + 1, n1 + n + 1))[m0] ≤ rev(subarray(ar1, m + 1, n1 + n + 1))[n], m0 ≤ n1 + n, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, 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: subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1), m0

Proof step 17 from proof remains-ordered-by-swap (previous step) (back to tree)

Lemma get-rev

Proof step 18 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # ar1 = 2 + n1 + n + m, ar1 ≠ [], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1)[(n - m0) + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, m0 ≤ n, j ≤ (n1 + n + 1) + m, rev(subarray(ar1, m + 1, n1 + n + 1))[m0] ≤ rev(subarray(ar1, m + 1, n1 + n + 1))[n], m0 ≤ n1 + n, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 19 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  # ar1 = 2 + n1 + n + m, n = n0 + m0, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + n + 1)[n0 + n1], m0 ≤ n1 + n, rev(subarray(ar1, m + 1, n1 + n + 1))[m0] ≤ rev(subarray(ar1, m + 1, n1 + n + 1))[n], j ≤ (n1 + n + 1) + m, m0 ≤ n, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

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

Proof step 20 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], rev(subarray(ar1, m + 1, n1 + (n0 + m0) + 1))[m0] ≤ rev(subarray(ar1, m + 1, n1 + (n0 + m0) + 1))[n0 + m0], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m ≤ m + n; (s)

Proof step 21 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, m0 < # subarray(ar1, m + 1, n1 + (n0 + m0) + 1), j ≤ (n1 + (n0 + m0) + 1) + m, subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[# subarray(ar1, m + 1, n1 + (n0 + m0) + 1) - m0 + 1] ≤ rev(subarray(ar1, m + 1, n1 + (n0 + m0) + 1))[n0 + m0], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (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(ar1, m + 1, n1 + (n0 + m0) + 1), m0

Proof step 22 from proof remains-ordered-by-swap (previous step) (back to tree)

Lemma get-rev

Proof step 23 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], j ≤ (n1 + (n0 + m0) + 1) + m, subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[n1 + n0] ≤ rev(subarray(ar1, m + 1, n1 + (n0 + m0) + 1))[n0 + m0], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 24 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, n0 + m0 < # subarray(ar1, m + 1, n1 + (n0 + m0) + 1), subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[n1 + n0] ≤ subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[# subarray(ar1, m + 1, n1 + (n0 + m0) + 1) - (n0 + m0) + 1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (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(ar1, m + 1, n1 + (n0 + m0) + 1), n0 + m0

Proof step 25 from proof remains-ordered-by-swap (previous step) (back to tree)

Lemma get-rev

Proof step 26 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], j ≤ (n1 + (n0 + m0) + 1) + m, subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[n1 + n0] ≤ subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 27 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, n1 + n0 < n1 + (n0 + m0) + 1, ar1[(m + 1) + n1 + n0] ≤ subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[n1], j ≤ (n1 + (n0 + m0) + 1) + m, (n1 + (n0 + m0) + 1) + m + 1 ≤ # ar1, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (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 ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem[natarray] lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: ar1, m + 1, n1 + (n0 + m0) + 1, n1 + n0

Proof step 28 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m + 1 < # ar1, subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, ar1[(m + 1) + n1 + n0] ≤ subarray(ar1, m + 1, n1 + (n0 + m0) + 1)[n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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 + n < m + n0 ↔ n < n0; (s)

Proof step 30 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], m + 1 < # ar1, n1 < n1 + (n0 + m0) + 1, j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], (n1 + (n0 + m0) + 1) + m + 1 ≤ # ar1, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (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 ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: ar1, m + 1, n1 + (n0 + m0) + 1, n1

Proof step 31 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], m + 1 < # ar1, j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 33 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m + 1 < # ar1, ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, n1 < n1 + (n0 + m0) + 1, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, (n1 + (n0 + m0) + 1) + m + 1 ≤ # ar1[m, ar1[j]][j, ar1[m]], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ m < n + 1 ↔ ¬ n < m; (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 ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1, n1

Proof step 34 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], m + 1 < # ar1, ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 36 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 37:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 = j, ar1 ≠ [], m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], m + 1 < # ar1, j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

• Proof step 54:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, ar1 ≠ [], m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], m + 1 < # ar1, j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used formulas: (m + 1) + n1 = j

Proof step 37 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], ar1[m] < subarray(ar1[m, ar1[(m + 1) + n1]][(m + 1) + n1, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n1 < # ar1, ar1[m] < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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 < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ ¬ m + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) m < # ar ⊦ ar[m, a][m] = a; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ m ≤ m + n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)

Proof step 38 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], ar1[m] < ar1[(m + 1) + n1], (m + 1) + n1 < # ar1, m < # ar1, m + 1 < # ar1, ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n1, ar1[m]][(m + 1) + n0 + n1], n0 + n1 < n1 + (n0 + m0) + 1, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], (n1 + (n0 + m0) + 1) + m + 1 ≤ # ar1[m, ar1[(m + 1) + n1]][(m + 1) + n1, ar1[m]], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (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 ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem[natarray] lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: ar1[m, ar1[(m + 1) + n1]][(m + 1) + n1, ar1[m]], m + 1, n1 + (n0 + m0) + 1, n0 + n1

Proof step 39 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], ar1[m] < ar1[(m + 1) + n1], (m + 1) + n1 < # ar1, m < # ar1, m + 1 < # ar1, ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n1, ar1[m]][(m + 1) + n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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 + n < m + n0 ↔ n < n0; (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ # ar[n, a] = # ar; (s)

Proof step 41 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 42:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 ≠ (m + 1) + n1, ar1 ≠ [], ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n1, ar1[m]][(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n1 < # ar1, ar1[m] < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

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

Proof step 42 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[(m + 1) + n1], (m + 1) + n1 < # ar1, m < # ar1, m + 1 < # ar1, ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n1, ar1[m]][(m + 1) + n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 43 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 ≠ (m + 1) + n1, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n1 < # ar1, ar1[m] < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

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

Proof step 44 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n1 < # ar1, ar1[m] < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 46 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 47:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 ≠ m, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[(m + 1) + n1], (m + 1) + n1 < # ar1, m < # ar1, m + 1 < # ar1, ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ 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: (m + 1) + n0 + n1 = m

Proof step 47 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[m, ar1[(m + 1) + n1]][(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n1 < # ar1, ar1[m] < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 48 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 ≠ m, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[(m + 1) + n1], (m + 1) + n1 < # ar1, m < # ar1, m + 1 < # ar1, ar1[m] < ar1[(m + 1) + n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ 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: ar1, m, ar1[(m + 1) + n1], (m + 1) + n0 + n1

Proof step 49 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[(m + 1) + n1], (m + 1) + n1 < # ar1, m < # ar1, m + 1 < # ar1, ar1[m] < ar1[(m + 1) + n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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 ≠ 0; (s) ⊦ m = m + n ↔ n = 0; (s)

Proof step 51 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 52:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n1 < # ar1, ar1[m] < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], (m + 1) + n1 < (m + 1) + n0 + n1 ∧ (m + 1) + n0 + n1 < # ar1 → ar1[(m + 1) + n0 + n1] ≤ ar1[m] ⊦

Rule argument

Additional information

Used terms: (m + 1) + n0 + n1

Proof step 52 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  # ar1 = 2 + n1 + (n0 + m0) + m, n0 + n1 ≠ 0, ar1 ≠ [], n0 ≠ 0, ar1[m] < ar1[(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n1 < # ar1, ar1[m] < ar1[(m + 1) + n1], # ar1 ≤ (m + 1) + n0 + n1, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1] ⊦

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 < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s)

Proof step 53 from proof remains-ordered-by-swap (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) 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

Proof step 54 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, ar1 ≠ [], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, ar1[m, ar1[j]][(m + 1) + n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

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

Proof step 55 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 56:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ m, (m + 1) + n1 ≠ j, ar1 ≠ [], ar1[m, ar1[j]][(m + 1) + n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ 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: (m + 1) + n1 = m

Proof step 56 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, ar1 ≠ [], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, ar1[m, ar1[j]][(m + 1) + n1] < subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1)[n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 57 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

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

• Proof step 59:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, ar1 ≠ [], ar1[m, ar1[j]][(m + 1) + n1] < ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], n0 + n1 < n1 + (n0 + m0) + 1, j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], (n1 + (n0 + m0) + 1) + m + 1 ≤ # ar1[m, ar1[j]][j, ar1[m]], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (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 ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: ar1[m, ar1[j]][j, ar1[m]], m + 1, n1 + (n0 + m0) + 1, n0 + n1

Proof step 58 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 59 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, ar1 ≠ [], ar1[m, ar1[j]][(m + 1) + n1] < ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) ⊦ 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 + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ # ar[n, a] = # ar; (s)

Proof step 60 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 61:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 = j, (m + 1) + n1 ≠ j, ar1 ≠ [], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, ar1[m, ar1[j]][(m + 1) + n1] < ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

• Proof step 64:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 ≠ j, (m + 1) + n1 ≠ j, ar1 ≠ [], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, ar1[m, ar1[j]][(m + 1) + n1] < ar1[m, ar1[j]][j, ar1[m]][(m + 1) + n0 + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used formulas: (m + 1) + n0 + n1 = j

Proof step 61 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  # ar1 = 2 + n1 + (n0 + m0) + m, ar1 ≠ [], n0 ≠ 0, ar1[m, ar1[(m + 1) + n0 + n1]][(m + 1) + n1] + 1 < ar1[(m + 1) + n0 + n1], ar1[m, ar1[(m + 1) + n0 + n1]][(m + 1) + n1] < ar1[(m + 1) + n0 + n1], m + 1 < # ar1, m < # ar1, (m + 1) + n0 + n1 < # ar1, ar1[m] < ar1[(m + 1) + n0 + n1], ar1[m, ar1[(m + 1) + n0 + n1]][(m + 1) + n1] < ar1[m], ar1[m] < ar1[(m + 1) + n1], ar1[m, ar1[(m + 1) + n0 + n1]][(m + 1) + n1] < ar1[(m + 1) + n1], ar1[m, ar1[(m + 1) + n0 + n1]][(m + 1) + n1] + 1 < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. (m + 1) + n0 + n1 < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem[natarray] ⊦ ¬ m + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) m < # ar ⊦ ar[m, a][m] = a; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ m ≤ m + n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m = m + n ↔ n = 0; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 62 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 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 < n → (n ≤ m ↔ false); (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) Used terms: ar1, m, ar1[(m + 1) + n0 + n1], (m + 1) + n1

Proof step 63 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, (m + 1) + n0 + n1 ≠ j, ar1 ≠ [], ar1[m, ar1[j]][(m + 1) + n1] < ar1[m, ar1[j]][(m + 1) + n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

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

Proof step 65 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 66:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 ≠ m, (m + 1) + n1 ≠ j, (m + 1) + n0 + n1 ≠ j, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], ar1[m, ar1[j]][(m + 1) + n1] < ar1[m, ar1[j]][(m + 1) + n0 + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ 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: (m + 1) + n0 + n1 = m

Proof step 66 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, (m + 1) + n0 + n1 ≠ j, ar1 ≠ [], ar1[m, ar1[j]][(m + 1) + n1] < ar1[m, ar1[j]][(m + 1) + n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

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

Proof step 67 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

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

• Proof step 69:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n0 + n1 ≠ m, (m + 1) + n1 ≠ j, (m + 1) + n0 + n1 ≠ j, ar1 ≠ [], m + 1 < # ar1, m < # ar1, m < j, j < # ar1, ar1[m] < ar1[j], ar1[m, ar1[j]][(m + 1) + n1] < ar1[(m + 1) + n0 + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ 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: ar1, m, ar1[j], (m + 1) + n0 + n1

Proof step 68 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma

Proof step 69 from proof remains-ordered-by-swap (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  # ar1 = 2 + n1 + (n0 + m0) + m, (m + 1) + n1 ≠ j, (m + 1) + n0 + n1 ≠ j, ar1 ≠ [], ar1[m, ar1[j]][(m + 1) + n1] < ar1[(m + 1) + n0 + n1], ar1[m] < ar1[j], j < # ar1, m < j, m < # ar1, m + 1 < # ar1, ar1[m, ar1[j]][(m + 1) + n1] < ar1[(m + 1) + n1], ar1[(m + 1) + n1 + n0] ≤ ar1[(m + 1) + n1], j ≤ (n1 + (n0 + m0) + 1) + m, ∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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 = m + n ↔ n = 0; (s)

Proof step 70 from proof remains-ordered-by-swap (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 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 < n → (n ≤ m ↔ false); (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) Used terms: ar1, m, ar1[j], (m + 1) + n1

Proof step 71 from proof remains-ordered-by-swap (previous step) (back to tree)

A spec-lemma