| ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , nextl(0, a) = a ' + y, lf(1) = nextl(0, a), lf(0) = a ', ii(0) = 0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , lf(n0 + 1) = nextl(n0, lf(n0).last), ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , # nextl(0, a) = ii(1) + 1, lf(n2 + 1) = nextl(n2, lf(n2).last), ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, lf(n2 + 1) = lf(n2).last ' + y0, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, lf(n2).last ∈ lf(n2 + 1), #(σ from ii(n2)) < ⌜# lf(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).rest = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).first = 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)⌝ ⊦ nextl(0, a) = [], σ = [], lf(n0) = [], σ[ii(n2)] = lf(n2).last, lf(n2) = [], lf(n2 + 1) = [], (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 ⌜ ⌝, ⌜ ⌝;;%from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; from specification stream%to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; from specification stream%sel-fin: ⊦ ⌜x⌝ [n] = x[n]; from specification stream%zero: ⊦ 0 < m ↔ m ≠ 0; from specification nat-basic1%l: ⊦ # x = 0 ↔ x = []; from specification list-data%get-infto: m < n ⊦ (nf to n)[m] = nf(m); from specification stream%get-from-inf-zero: ⊦ ((nf from n))(0) = nf(n); from specification stream%inf-size-to: ⊦ # ⌜nf to n⌝ = ⌜n⌝ ; from specification stream%inj: ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; from specification nat-inf-basic%inj-02: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; from specification stream-basic%fun-nonempty: ⊦ [] ≠ ⌜nf⌝ ; from specification stream%sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); from specification stream%from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; from specification stream%to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; from specification stream%size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; from specification stream%fin-empty: ⊦ ⌜x⌝ = [] ↔ x = []; from specification stream%less-fin: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; from specification nat-inf%test-02: ⊦ finp(⌜x⌝ ); from specification stream-basic%eq-natinf-to-nat-2-1: ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; from specification nat-inf%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%get-zero: ⊦ x ≠ [] → x[0] = x.first; from specification list-del%eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic1%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic1%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2%lels: ⊦ ¬ 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%succ: ⊦ m +1 = m + 1; from specification nat-basic2%l-02: ⊦ ¬ m + n < m; from specification nat-basic2%length-from: ¬ # x < n ⊦ #(x from n) = # x - n; from specification stream%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%ls-01: n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; from specification nat%le-ls-simp: ⊦ m ≤ n → (n < m ↔ false); from specification nat