| n3 + n0 = m + 1, n3 ≤ m - n0, np(n0), n0 ≤ m + 1, np(n), n0 < n, ∀ n1, n2, np. n1 - n2 < n3 → np(n2) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n1 < n0 ∧ np(n0)) ⊦ n = 0, np(m + 1), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n1. m + 1 < n1 ∧ np(n1) |
Used simplifier rules: lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%les: ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); from specification nat%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%lels: ⊦ ¬ m < n ↔ n ≤ m; from specification nat%eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat%le-one: ⊦ m ≤ n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic1%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic1%trans-1: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic1%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic1%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%ler: ⊦ m ≤ m; from specification nat%le-add: ⊦ m + m0 ≤ m ↔ m0 = 0; from specification nat%ls-le-simp: ⊦ m < n → (n ≤ m ↔ false); from specification nat%ls-02: n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; from specification nat%eq: ⊦ m = n + 1 → ¬ m ≤ n; from specification nat Used terms: n