| (n0 + m) + 1 = n1 + n, 0 < sum(ar, n, n1), n0 + m < # ar, m < # ar, sum(ar, m, n0) + ar[n0 + m] < sum(ar, n, n1), suffix-upper-bound(subarray(ar, 0, n0 + m), sum(ar, m, n0)), n1 + n ≤ # ar, 0 ≤ sum(ar, m, n0) + ar[n0 + m], 0 ≤ sum(ar, m, n0), n ≤ # ar, n ≤ n0 + m → sum(ar, n, n0 + m - n) ≤ sum(ar, m, n0) ⊦ |
Used simplifier rules: sum-zero: ⊦ sum(ar, n, 0) = 0;%sum-succ: n + m < # ar ⊦ sum(ar, n, m + 1) = sum(ar, n, m) + ar[n + m];%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ 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% ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)% ⊦ m < n → m ≤ n; (s)% ⊦ m ≤ m + n; (s)% ⊦ m + 1 ≤ n ↔ m < n; (s)% ⊦ i + j < i + i0 ↔ j < i0; (s)% ⊦ i ≤ j → ¬ j < i; (s)%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%# ar0 = n ⊦ subarray(ar0, 0, n) = ar0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat%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 + m0 ≤ m ↔ m0 = 0; (s)% ⊦ n + 0 = n; (s)%n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, n0 + m, n2