| ¬ finp(σ), # nextl(0, a) = ii(1) + 1, lf(n0 + 1) = nextl(n0, lf(n0).last), σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , ii(0) = 0, lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + y, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , ⌜ii(1)⌝ < # σ, a ∈ nextl(0, a), ⌜ii(n0 + 1)⌝ < # σ, ∀ n. σ[ii(n)] = lf(n).last, ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).first = a, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).rest = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1), lf(n0) = [], σ = [], nextl(0, a) = [] |
# nextl(0, a) = ii(1) + 1, lf(n0 + 1) = nextl(n0, lf(n0).last), nf to ii(1) + 1 = nextl(0, a), ii(0) = 0, lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + y, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, (nf from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), a ∈ nextl(0, a), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).first = a, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. nf(ii(n)) = lf(n).last, ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ (nf from ii(n)) to # lf(n + 1) = lf(n + 1) ⊦ lf(n0) = [], nextl(0, a) = [], ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)
Used simplifier rules: sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); from specification stream%test-01: ⊦ ¬ finp(⌜nf⌝ ); from specification stream-basic%fun-nonempty: ⊦ [] ≠ ⌜nf⌝ ; from specification stream%from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; from specification stream%inj-02: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; from specification stream-basic%to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; from specification stream%stream-inf-forward: ⊦ ¬ finp(σ) → (∃ nf. ⌜nf⌝ = σ); (forward) from specification stream-basic%less-inf2: ⊦ ⌜m⌝ < ∞; from specification nat-inf%notfin-sizeinf: ⊦ ¬ finp(σ) → # σ = ∞; from specification stream