| (n * n + n) / 2 ≤ m, (m0 * m0 + m0) / 2 ≤ m, ((m0 + 2) * m0 + m0) / 2 < m, m ≤ (m - m0 + 1) + m0, m * 2 ≤ (n + 2) * n + n, (n * n + n) / 2 ≤ (m - m0 + 1) + m0, (m0 * m0 + m0) / 2 ≤ (m - m0 + 1) + m0, ((m0 + 2) * m0 + m0) / 2 < (m - m0 + 1) + m0, ∀ m2, m3, n. m2 - m3 < m - m0 → true → (n * (n + 1)) / 2 ≤ m2 ∧ m2 < ((n + 1) * (n + 2)) / 2 ∧ (m3 * (m3 + 1)) / 2 ≤ m2 → maxenc(m3, m2) = n ⊦ maxenc(m0 + 1, m) = n, m = 0, m = 1 |
Used simplifier rules: one: ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%lep: ⊦ m ≤ m + n; from specification nat%cancel-01: ⊦ m + n - n + n1 = m - n1; from specification nat%lep-02: ⊦ m + n ≤ m + n0 ↔ n ≤ n0; from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%leprf: ⊦ m ≤ m - 1 → m = 0; (forward) from specification nat%add-base: ⊦ n + 0 = n; from specification nat-basic2%lez: ⊦ 0 ≤ m; from specification nat%two-loup-12: ⊦ (m + n) / 2 < n ↔ m < n; from specification nat-div%ls-01: ⊦ m0 * m < m ↔ m0 = 0 ∧ m ≠ 0; from specification nat-mult%add-num-03: n < n0 ⊦ (* n) ≠ m0 + (* n0); from specification nat%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic1%trans-1: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic1%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m, m0, n0