| # x = ii(n), lf(0) = [], ii(0) = 0, nextli0(lf(m)) = [], n0 < n, m < n, ii(m) < ii(n0 + 1), n0 < m, n0 + 1 < n, ∀ m0. m < m0 → lf(m0) = lf(m) ∧ nextli0(lf(m0)) = [] ∧ ii(m0) = ii(m), ∀ n0. ii(n0 + 1) = ii(n0) + # nextli0(lf(n0)) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # nextli0(lf(n0)) = nextli0(lf(n0)), ∀ n0. lf(n0) = x to ii(n0), ∀ m. n ≤ m → nextli0(lf(m)) = [] ∧ ii(m) = ii(n), ∀ x. nextli(x) = x + nextli0(x), ∀ n. lf(n + 1) = nextli(lf(n)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. nextli0(lf(n)) = [] → (∀ m. n < m → lf(m) = lf(n) ∧ nextli0(lf(m)) = [] ∧ ii(m) = ii(n)), ∀ n0, ii, lf, x, nextli0, nextli. n0 < n → ii(0) = 0 ∧ lf(0) = [] ∧ # x = ii(n0) ∧ (∀ n. nextli0(lf(n)) = [] → (∀ m. n < m → lf(m) = lf(n) ∧ nextli0(lf(m)) = [] ∧ ii(m) = ii(n))) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n. lf(n + 1) = nextli(lf(n))) ∧ (∀ x. nextli(x) = x + nextli0(x)) ∧ (∀ m. n0 ≤ m → nextli0(lf(m)) = [] ∧ ii(m) = ii(n0)) ∧ (∀ n0. lf(n0) = x to ii(n0)) ∧ (∀ n1. ii(n1 + 1) = ii(n1) + # nextli0(lf(n1)) ∧ ¬ ii(n0) < ii(n1 + 1) ∧ (x from ii(n1)) to # nextli0(lf(n1)) = nextli0(lf(n1))) → (∃ n0. ∀ m. nextli0(lf(m)) = [] ↔ n0 ≤ m) ⊦ m = 0, ii(n0 + 1) = 0, n = 0, ∃ n0. ∀ m. nextli0(lf(m)) = [] ↔ n0 ≤ m |
Used simplifier rules: succ-01: ⊦ m + 1 ≤ n ↔ m < n; from specification nat%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%ls-le-simp: ⊦ m < n → (n ≤ m ↔ false); from specification nat Used terms: n0 + 1, m