| ii(n0) = m0 + 1, ii(0) = 0, (σ from m0 + 1) to # x0 = ⌜x0⌝ , ii(n0 + 1) = (# x0 + m0) + 1, m0 + # lf(n0) - 1 = # x0 + m0, lf(n0) = a ' + x0, ⌜m0⌝ < # σ, ⌜# x0⌝ + ⌜m0⌝ < # σ, a ∈ lf(n0), σ[ii((n0 - 1) + 1) - 1] = lf((n0 - 1) + 1).first, ∀ n. σ[ii(n + 1) - 1] = lf(n + 1).first, ∀ n. n ≠ 0 → ii(n) ≠ 0, ∀ n. ii(n + 1) = ii(n) + # (n = 0 ⊃ lf(0);lf(n).rest) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # (n = 0 ⊃ lf(0);lf(n).rest) = ⌜(n = 0 ⊃ lf(0);lf(n).rest)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n).last = lf(n + 1).first ∧ lf(n) ≠ [], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → (m = 0 ⊃ lf(0);lf(m).rest) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ ⌜σ[m0] '⌝ + (σ from m0 + 1) to # lf(n0) = ⌜lf(n0)⌝ , lf(n0) = [] |
Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%oz: ⊦ m + 1 ≠ 0; from specification nat-basic2%in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list%a: ⊦ (x + y) + z = x + y + z; from specification list%add-01: ⊦ n ≤ m → m + n0 - n = (m - n) + n0; from specification nat%add-base: ⊦ n + 0 = n; from specification nat-basic2%c-08: ⊦ (a ' + x).first = a; from specification list%len-05: ⊦ #(a ' + x) = (# x)+1; from specification list%succ: ⊦ m +1 = m + 1; from specification nat-basic2%eq-01: ⊦ m + n = m + n0 ↔ n = n0; from specification nat-basic2%e-01: ⊦ a ' + x ≠ []; from specification list%to-succ-cons: ⊦ ⌜a '⌝ + σ to n + 1 = a + (σ to n); from specification stream%cons-append: ⊦ a + σ = ⌜a '⌝ + σ; from specification stream%append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream%append-finfin: ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; from specification stream%cons-eq: ⊦ ⌜a '⌝ + σ = ⌜a0 '⌝ + σ0 ↔ a = a0 ∧ σ = σ0; from specification stream%from-zero: ⊦ σ from 0 = σ; from specification stream%z-01: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; from specification nat-basic2%n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n0, m1