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