| finp(σ), # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextli0(lf(m)) = [] ∧ ii(m) = ii(n)), ∀ m. n0 < m → ii(m) = ii(n0) ∧ lf(m) = lf(n0), lf(0) = [], ii(0) = 0, nextli0(lf(n0)) = [], ii(n0 + 1) = ii(n0), ∀ x. nextli(x) = x + nextli0(x), ∀ n. lf(n + 1) = nextli(lf(n)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextli0(lf(n)) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # nextli0(lf(n)) = ⌜nextli0(lf(n))⌝ , ∀ n0. lf(n0) = (σ to ii(n0)).l ⊦ # σ = ⌜ii(n0)⌝ , # σ < ⌜ii(n0)⌝ |
# x = ii(n), ii(n0 + 1) = ii(n0), nextli0(lf(n0)) = [], ii(0) = 0, lf(0) = [], ii(n0) < ii(n), ∀ n1. lf(n1) = x to ii(n1), ∀ n1. ii(n1 + 1) = ii(n1) + # nextli0(lf(n1)) ∧ ¬ ii(n) < ii(n1 + 1) ∧ (x from ii(n1)) to # nextli0(lf(n1)) = nextli0(lf(n1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextli(lf(n)), ∀ x. nextli(x) = x + nextli0(x), ∀ m. n0 < m → ii(m) = ii(n0) ∧ lf(m) = lf(n0), ∀ m. n ≤ m → nextli0(lf(m)) = [] ∧ ii(m) = ii(n) ⊦ ii(n) = ii(n0), ii(n) = 0
Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic1%sel-02: ⊦ ⌜x⌝ .l = x; from specification stream-basic%inj-02: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; from specification stream-basic%to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; from specification stream%from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; from specification stream%test-02: ⊦ finp(⌜x⌝ ); from specification stream-basic%size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; from specification stream%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic1%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%neq-01: ⊦ m ≠ n → (¬ m < n ↔ n < m); from specification nat-basic1%less-fin: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; from specification nat-inf%inj: ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; from specification nat-inf-basic%stream-fin-forward: ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ); (forward) from specification stream-basic