Proof step 1 from proof array-le-one-diffrent-position (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1[m] < ar2[m], m < # ar2, m < # ar1, ¬ ar1 ≤ ar2 ⊦

Rule argument

Additional information

Proof step 2 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ [], ar2 ≠ [], ar1[m] < ar2[m], m < # ar2, m < # ar1, ¬ ar1 ≤ ar2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  subarray(i + ar, 0, m) = subarray(ar2, 0, m), i + ar ≠ [], ar2 ≠ [], m < #(i + ar), m < # ar2, (i + ar)[m] < ar2[m], ¬ i + ar ≤ ar2, ∀ m, ar2. ¬(subarray(ar, 0, m) = subarray(ar2, 0, m) ∧ ar ≠ [] ∧ ar2 ≠ [] ∧ ar[m] < ar2[m] ∧ m < # ar2 ∧ m < # ar ∧ ¬ ar ≤ ar2) ⊦

Rule argument

Additional information

Used simplifier rules: array freely generated by [], +;;

Proof step 4 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  subarray(i ' + ar, 0, m) = subarray(ar2, 0, m), ar2 ≠ [], (i ' + ar)[m] < ar2[m], m < # ar2, m ≤ # ar, ¬ i ' + ar ≤ ar2, ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ a + x = a ' + x; (s) 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) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a ' + x ≠ []; (s)

Proof step 5 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  subarray(i ' + ar, 0, m) = subarray(i0 + ar0, 0, m), i0 + ar0 ≠ [], m < #(i0 + ar0), (i ' + ar)[m] < (i0 + ar0)[m], m ≤ # ar, ¬ i ' + ar ≤ i0 + ar0, ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0, ∀ i, ar, m. ¬ ( subarray(i ' + ar, 0, m) = subarray(ar0, 0, m) ∧ ar0 ≠ [] ∧ (i ' + ar)[m] < ar0[m] ∧ m < # ar0 ∧ m ≤ # ar ∧ ¬ i ' + ar ≤ ar0 ∧ (∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0)) ⊦

Rule argument

Additional information

Used simplifier rules: array freely generated by [], +;;

Proof step 6 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  subarray(i ' + ar, 0, m) = subarray(i0 ' + ar0, 0, m), (i ' + ar)[m] < (i0 ' + ar0)[m], m ≤ # ar0, m ≤ # ar, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar0 = [] ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0 ⊦ (i = i0 ⊃ ar ≤ ar0;i < i0)

Rule argument

Additional information

Used simplifier rules: lexicographic-rec1: ⊦ n ' + ar1 ≤ m ' + ar2 ↔ (n = m ⊃ ar1 ≤ ar2;n ≤ m); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) ⊦ a + x = a ' + x; (s) 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) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a ' + x ≠ []; (s)

Proof step 7 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  subarray(i ' + ar, 0, m) = subarray(i0 ' + ar0, 0, m), ar0 ≠ [], (i ' + ar)[m] < (i0 ' + ar0)[m], m ≤ # ar, m ≤ # ar0, ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar0 = [] ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦ (i = i0 ⊃ ar ≤ ar0;i < i0)

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ x + [] = x; (s) ⊦ subarray(ar, n, 0) = mkarray(0); (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ a '[0] = a; (s) ⊦ 0 ≤ m; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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 < n → n ≠ 0; (s) ⊦ m < n → ¬ n < m; (s) Used formulas: ar0 = []

Proof step 8 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  subarray(i ' + ar, 0, m) = subarray(i0 ' + ar0, 0, m), ar0 ≠ [], (i ' + ar)[m] < (i0 ' + ar0)[m], m ≤ # ar0, m ≤ # ar, ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦ (i = i0 ⊃ ar ≤ ar0;i < i0)

Rule argument

Additional information

Proof step 9 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  subarray(i ' + ar, 0, m) = subarray(i0 ' + ar0, 0, m), ar0 ≠ [], (i ' + ar)[m] < (i0 ' + ar0)[m], m ≤ # ar, m ≤ # ar0, ¬ i < i0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0 ⊦ (i = i0 ⊃ ar ≤ ar0;i < i0)

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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 < n → n ≠ 0; (s) ⊦ m < n → ¬ n < m; (s) Used formulas: i < i0

Proof step 10 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  subarray(i ' + ar, 0, m) = subarray(i0 ' + ar0, 0, m), ar0 ≠ [], (i ' + ar)[m] < (i0 ' + ar0)[m], m ≤ # ar0, m ≤ # ar, i0 ≤ i, ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦ i = i0 ∧ ar ≤ ar0

Rule argument

Additional information

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

Proof step 11 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  m + n ≤ # ar, n ≠ 0 ⊦ subarray(ar, m, n) = ar[m] + subarray(ar, m + 1, n - 1)

• Proof step 13:

  (i ' + ar)[0] + subarray(i ' + ar, 0 + 1, m - 1) = subarray(i0 ' + ar0, 0, m), ar0 ≠ [], m ≠ 0, (i ' + ar)[m] < (i0 ' + ar0)[m], i0 ≤ i, m ≤ # ar, m ≤ # ar0, 0 + m ≤ #(i ' + ar), ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0 ⊦ i = i0 ∧ ar ≤ ar0

Rule argument

Additional information

Used simplifier rules: ⊦ n + 0 = n; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (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 ⊦ subarray(ar, n, 0) = mkarray(0); (s) ⊦ 0 ≤ m; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: 0, m, i ' + ar

Proof step 12 from proof array-le-one-diffrent-position (previous step) (back to tree)

Lemma subarray-inc-offset0

Proof step 13 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  i ' + subarray(i ' + ar, 1, m - 1) = subarray(i0 ' + ar0, 0, m), ar0 ≠ [], m ≠ 0, (i ' + ar)[m] < (i0 ' + ar0)[m], i ∈ subarray(i0 ' + ar0, 0, m), m ≤ # ar0, m ≤ # ar, i0 ≤ i, m ≤ # ar + 1, ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦ i = i0 ∧ ar ≤ ar0

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list[natarray-oarray-sort] ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x)[0] = a; (s)

Proof step 14 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  i ' + subarray(i ' + ar, 1, m1) = subarray(i0 ' + ar0, 0, m), m = m1 + 1, ar0 ≠ [], m ≠ 0, (i ' + ar)[m] < (i0 ' + ar0)[m], i ∈ subarray(i0 ' + ar0, 0, m), m ≤ # ar + 1, i0 ≤ i, m ≤ # ar, m ≤ # ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar0. subarray(ar, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar = [] ∨ ar0 = [] ∨ ¬ ar[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar ∨ ar ≤ ar0 ⊦ i = i0 ∧ ar ≤ ar0

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: m, m1

Proof step 15 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  i ' + subarray(i ' + ar, 1, m1) = subarray(i0 ' + ar0, 0, m1 + 1), ar ≠ [], ar0 ≠ [], ar[m1] < ar0[m1], m1 < # ar, m1 < # ar0, i ∈ subarray(i0 ' + ar0, 0, m1 + 1), i0 ≤ i, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(ar, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ ar[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ ¬ m0 < # ar ∨ ar ≤ ar1 ⊦ i = i0 ∧ ar ≤ ar0

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list[natarray-oarray-sort] c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ m < n → m ≤ n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 16 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  m + n ≤ # ar, n ≠ 0 ⊦ subarray(ar, m, n) = ar[m] + subarray(ar, m + 1, n - 1)

• Proof step 18:

  i ' + subarray(i ' + ar, 1, m1) = (i0 ' + ar0)[0] + subarray(i0 ' + ar0, 0 + 1, m1 + 1 - 1), m1 + 1 ≠ 0, ar ≠ [], ar0 ≠ [], m1 < # ar0, m1 < # ar, ar[m1] < ar0[m1], i ∈ (i0 ' + ar0)[0] + subarray(i0 ' + ar0, 0 + 1, m1 + 1 - 1), i0 ≤ i, 0 + m1 + 1 ≤ #(i0 ' + ar0), ∀ m0, ar1. subarray(ar, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ ar[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ ¬ m0 < # ar ∨ ar ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦ i = i0 ∧ ar ≤ ar0

Rule argument

Additional information

Used simplifier rules: ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m < n → m ≤ n; (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: 0, m1 + 1, i0 ' + ar0

Proof step 17 from proof array-le-one-diffrent-position (previous step) (back to tree)

Lemma subarray-inc-offset0

Proof step 18 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  subarray(i0 ' + ar, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar ≠ [], ar0 ≠ [], m1 < # ar0, m1 < # ar, ar[m1] < ar0[m1], ¬ ar ≤ ar0, ∀ m0, ar1. subarray(ar, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ ar[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ ¬ m0 < # ar ∨ ar ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ (a ' + x)[0] = a; (s) ⊦ m < n → m ≤ n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m + 1 ≠ 0; (s) ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; (ws)

Proof step 19 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 20:

  ar = i + ar2, subarray(i0 ' + ar, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar ≠ [], ar0 ≠ [], ar[m1] < ar0[m1], m1 < # ar, m1 < # ar0, ¬ ar ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(ar, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ ar[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ ¬ m0 < # ar ∨ ar ≤ ar1 ⊦

Rule argument

Additional information

Used simplifier rules: array freely generated by [], +;;

Proof step 20 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar0 ≠ [], m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) 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) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ a ' + x ≠ []; (s)

Proof step 21 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar0 ≠ [], (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), subarray(i ' + ar2, 0, m1) ≠ subarray(ar0, 0, m1) ∨ ¬ (i ' + ar2)[m1] < ar0[m1] ∨ ¬ m1 < # ar0 ∨ ¬ m1 ≤ # ar2 ∨ i ' + ar2 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar2, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar2 = [] ∨ ar0 = [] ∨ ¬ ar2[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar2 ∨ ar2 ≤ ar0) ⊦

Rule argument

Additional information

Used terms: i, ar2, m1

Proof step 22 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar0 ≠ [], m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, subarray(i ' + ar2, 0, m1) ≠ subarray(ar0, 0, m1) ∨ subarray(ar2, 0, m0) = subarray(ar, 0, m0) ∧ ar2 ≠ [] ∧ ar ≠ [] ∧ ar2[m0] < ar[m0] ∧ m0 < # ar ∧ m0 < # ar2 ∧ ¬ ar2 ≤ ar ⊦

Rule argument

Additional information

Proof step 23 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 24:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar0 ≠ [], ar2 ≠ [], (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), subarray(i ' + ar2, 0, m1) ≠ subarray(ar0, 0, m1) ∨ subarray(ar2, 0, m0) = subarray(ar, 0, m0) ∧ ar2 ≠ [] ∧ ar ≠ [] ∧ ar2[m0] < ar[m0] ∧ m0 < # ar ∧ m0 < # ar2 ∧ ¬ ar2 ≤ ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ # [] = 0; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ a '[0] = a; (s) ⊦ x ≠ [] → x[0] = x.first; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem[natarray] ⊦ subarray(ar, n, 0) = mkarray(0); (s) Used formulas: ar2 = []

Proof step 24 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar0 ≠ [], ar2 ≠ [], m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, subarray(i ' + ar2, 0, m1) ≠ subarray(ar0, 0, m1) ∨ subarray(ar2, 0, m0) = subarray(ar, 0, m0) ∧ ar ≠ [] ∧ ar2[m0] < ar[m0] ∧ m0 < # ar ∧ m0 < # ar2 ∧ ¬ ar2 ≤ ar ⊦

Rule argument

Additional information

Proof step 25 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar0 ≠ [], ar2 ≠ [], subarray(i ' + ar2, 0, m1) ≠ subarray(ar0, 0, m1), (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦

• Proof step 33:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), subarray(ar2, 0, m0) = subarray(ar, 0, m0), ar ≠ [], ar0 ≠ [], ar2 ≠ [], (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, ar2[m0] < ar[m0], m0 < # ar, m0 < # ar2, m1 ≤ # ar2, ¬ ar2 ≤ ar, ¬ i ' + ar2 ≤ ar0, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦

Rule argument

Additional information

Proof step 26 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar0 ≠ [], ar2 ≠ [], m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, # subarray(i ' + ar2, 0, m1) ≠ # subarray(ar0, 0, m1) ∨ (∃ n. ¬(n < # subarray(i ' + ar2, 0, m1) → subarray(i ' + ar2, 0, m1)[n] = subarray(ar0, 0, m1)[n])) ⊦

Rule argument

Additional information

Used terms: subarray(i ' + ar2, 0, m1), subarray(ar0, 0, m1)

Proof step 27 from proof array-le-one-diffrent-position (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), (i ' + ar2)[n] ≠ ar0[n], ar0 ≠ [], ar2 ≠ [], n < # ar2, n < m1, m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], n < # ar0, n + 1 < # ar0, m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1 ⊦

Rule argument

Additional information

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

Proof step 29 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  # subarray(i0 ' + i ' + ar2, 1, m1) = # subarray(i0 ' + ar0, 1, m1), (i ' + ar2)[n] ≠ ar0[n], ar0 ≠ [], ar2 ≠ [], n + 1 < # ar0, n < # ar0, (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, n < m1, n < # ar2, m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ n. n < # subarray(i0 ' + i ' + ar2, 1, m1) → subarray(i0 ' + i ' + ar2, 1, m1)[n] = subarray(i0 ' + ar0, 1, m1)[n] ⊦

Rule argument

Additional information

Used terms: subarray(i0 ' + i ' + ar2, 1, m1), subarray(i0 ' + ar0, 1, m1)

Proof step 30 from proof array-le-one-diffrent-position (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  (i ' + ar2)[n] ≠ ar0[n], ar0 ≠ [], ar2 ≠ [], n < # ar2, n < m1, m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], n < # ar0, n + 1 < # ar0, m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ n0. n0 < m1 → (i ' + ar2)[n0] = ar0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 32 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 33 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 34:

  subarray(ar2, 0, m0) = subarray(ar, 0, m0), subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar ≠ [], ar0 ≠ [], ar2 ≠ [], m0 < # ar2, m0 < # ar, ar2[m0] < ar[m0], m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], m1 ≤ # ar2, ¬ ar2 ≤ ar, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, subarray(i ' + ar2, 0, m1) ≠ subarray(ar0, 0, m1) ∨ ar0 = [] ∨ ¬ (i ' + ar2)[m1] < ar0[m1] ∨ ¬ m1 < # ar0 ∨ # ar2 < m1 ∨ i ' + ar2 ≤ ar0 ⊦

Rule argument

Additional information

Used terms: m1, ar0

Proof step 34 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  subarray(ar2, 0, m0) = subarray(ar, 0, m0), subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), ar ≠ [], ar0 ≠ [], ar2 ≠ [], subarray(i ' + ar2, 0, m1) ≠ subarray(ar0, 0, m1), m0 < # ar2, m0 < # ar, ar2[m0] < ar[m0], m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ¬ ar2 ≤ ar, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 35 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), subarray(ar2, 0, m0) = subarray(ar, 0, m0), ar ≠ [], ar0 ≠ [], ar2 ≠ [], (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, ar2[m0] < ar[m0], m0 < # ar, m0 < # ar2, m1 ≤ # ar2, ¬ i ' + ar2 ≤ ar0, ¬ ar2 ≤ ar, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), # subarray(i ' + ar2, 0, m1) ≠ # subarray(ar0, 0, m1) ∨ (∃ n. ¬(n < # subarray(i ' + ar2, 0, m1) → subarray(i ' + ar2, 0, m1)[n] = subarray(ar0, 0, m1)[n])) ⊦

Rule argument

Additional information

Used terms: subarray(i ' + ar2, 0, m1), subarray(ar0, 0, m1)

Proof step 36 from proof array-le-one-diffrent-position (previous step) (back to tree)

A spec-lemma

Proof step 37 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  subarray(i0 ' + i ' + ar2, 1, m1) = subarray(i0 ' + ar0, 1, m1), subarray(ar2, 0, m0) = subarray(ar, 0, m0), (i ' + ar2)[n] ≠ ar0[n], ar ≠ [], ar0 ≠ [], ar2 ≠ [], n < # ar2, n < m1, (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, ar2[m0] < ar[m0], m0 < # ar, m0 < # ar2, n < # ar0, n + 1 < # ar0, m1 ≤ # ar2, ¬ ar2 ≤ ar, ¬ i ' + ar2 ≤ ar0, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0) ⊦

Rule argument

Additional information

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

Proof step 38 from proof array-le-one-diffrent-position (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

  # subarray(i0 ' + i ' + ar2, 1, m1) = # subarray(i0 ' + ar0, 1, m1), subarray(ar2, 0, m0) = subarray(ar, 0, m0), (i ' + ar2)[n] ≠ ar0[n], ar ≠ [], ar0 ≠ [], ar2 ≠ [], n + 1 < # ar0, n < # ar0, m0 < # ar2, m0 < # ar, ar2[m0] < ar[m0], m1 < # ar0, (i ' + ar2)[m1] < ar0[m1], n < m1, n < # ar2, m1 ≤ # ar2, ¬ ar2 ≤ ar, ¬ i ' + ar2 ≤ ar0, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ n. n < # subarray(i0 ' + i ' + ar2, 1, m1) → subarray(i0 ' + i ' + ar2, 1, m1)[n] = subarray(i0 ' + ar0, 1, m1)[n] ⊦

Rule argument

Additional information

Used terms: subarray(i0 ' + i ' + ar2, 1, m1), subarray(i0 ' + ar0, 1, m1)

Proof step 39 from proof array-le-one-diffrent-position (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  subarray(ar2, 0, m0) = subarray(ar, 0, m0), (i ' + ar2)[n] ≠ ar0[n], ar ≠ [], ar0 ≠ [], ar2 ≠ [], n < # ar2, n < m1, (i ' + ar2)[m1] < ar0[m1], m1 < # ar0, ar2[m0] < ar[m0], m0 < # ar, m0 < # ar2, n < # ar0, n + 1 < # ar0, m1 ≤ # ar2, ¬ ar2 ≤ ar, ¬ i ' + ar2 ≤ ar0, ∀ m0, ar1. subarray(i ' + ar2, 0, m0) ≠ subarray(ar1, 0, m0) ∨ ar1 = [] ∨ ¬ (i ' + ar2)[m0] < ar1[m0] ∨ ¬ m0 < # ar1 ∨ # ar2 < m0 ∨ i ' + ar2 ≤ ar1, ∀ i1, ar1, m0. subarray(i1 ' + ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ¬ (i1 ' + ar1)[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 ≤ # ar1 ∨ i1 ' + ar1 ≤ ar0 ∨ ¬ (∀ m0, ar0. subarray(ar1, 0, m0) ≠ subarray(ar0, 0, m0) ∨ ar1 = [] ∨ ar0 = [] ∨ ¬ ar1[m0] < ar0[m0] ∨ ¬ m0 < # ar0 ∨ ¬ m0 < # ar1 ∨ ar1 ≤ ar0), ∀ n0. n0 < m1 → (i ' + ar2)[n0] = ar0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 41 from proof array-le-one-diffrent-position (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n