| x = A[i + 1], y = A[i], i + 1 < # A, Inv-main(A, A0, i), y ≤ x ⊦ Inv-first-inner(A, A, x, y, i, i) |
Used simplifier rules: Inv-main: ⊦ Inv-main(A, A0, i) ↔ # A ≠ 0 ∧ # A = # A0 ∧ i ≤ # A ∧ sorted(A, 0, i) ∧ perm(A, A0);%Inv-first-inner: ⊦ Inv-first-inner(A, A0, x, y, i, j) ↔ # A ≠ 0 ∧ # A = # A0 ∧ i ≤ # A ∧ j ≤ i ∧ y ≤ x ∧ (j ≠ i → x < A[j + 2]) ∧ sorted(A, 0, j) ∧ sorted(A, j + 2, i + 2) ∧ (j ≠ i ∧ j ≠ 0 → A[j - 1] ≤ A[j + 2]) ∧ perm(A[j, y][j + 1, x], A0);% ⊦ perm(A, A); (s)% ⊦ m < n → (n ≤ m ↔ false); (s)%m < # ar ⊦ ar[m, ar[m]] = ar; (s)% ⊦ ¬ m + n < m; (s)% ⊦ m ≤ n → (n ≤ m ↔ m = n); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%1 ≤ # ar, n0 ≤ # ar, n0 - n ≤ 1 ⊦ sorted(ar, n, n0); (ss)% ⊦ ¬ n < n; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m +1 = m + 1; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)%n < n0 ⊦ (* n) ≠ m0 + (* n0); (s)%perm-trans: ⊦ perm(A, A0) ∧ perm(A0, A1) → perm(A, A1); (forward) from specification oarray-perm%trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ m < 1 ↔ m = 0; (s)% ⊦ 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 - m = 0; (s)% ⊦ m + n - n + n1 = m - n1; (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%m ≤ m0 ⊦ sorted(A, m, n) → sorted(A, m0, n); (ss)% ⊦ m ≤ m; (s)% ⊦ m < n → n ≠ 0; (s)% ⊦ x ≤ y ↔ ¬ y < x; (s)