| # nextl(0, a) = ii(1) + 1, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n2 + 1) = lf(n2).last ' + y0, nextl(0, a) = a ' + y, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, #(σ from ii(n2)) < ⌜# lf(n2 + 1)⌝ , a ∈ nextl(0, a), lf(n2).last ∈ lf(n2 + 1), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ σ[ii(n2)] = lf(n2).last, lf(n2 + 1) = [], lf(n0) = [], lf(n2) = [], nextl(0, a) = [], σ = [], (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a |
Used simplifier rules: stream freely generated by ⌜ ⌝, ⌜ ⌝;;% ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; (s)% ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s)% ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; (s)% ⊦ ⌜x⌝ [n] = x[n]; (s)% ⊦ 0 < m ↔ m ≠ 0; (s)% ⊦ # x = 0 ↔ x = []; (s)%m < n ⊦ (nf to n)[m] = nf(m); (s)% ⊦ ((nf from n))(0) = nf(n); (s)% ⊦ # ⌜nf to n⌝ = ⌜n⌝ ; (s)% ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; (s)% ⊦ [] ≠ ⌜nf⌝ ; (s)% ⊦ ⌜nf⌝ [n] = nf(n); (s)% ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; (s)% ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; (s)% ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)% ⊦ ⌜x⌝ = [] ↔ x = []; (s)% ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)% ⊦ finp(⌜x⌝ ); (s)% ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s)%add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf%add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf% ⊦ x ≠ [] → x[0] = x.head; (s)%eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ m < n → n ≠ 0; (s)% ⊦ m +1 = m + 1; (s)% ⊦ ¬ m + n < m; (s)%¬ # x < n ⊦ #(x from n) = # x - n; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)