| (# x0 + m0) + 1 = ii(n0 + 1), m0 + # lf(n0) - 1 = # x0 + m0, σ[ii((n0 - 1) + 1) - 1] = lf((n0 - 1) + 1).head, ii(0) = 0, ii(n0) = m0 + 1, lf(n0) = a ' + x0, (σ from m0 + 1) to # x0 = ⌜x0⌝ , ⌜# x0⌝ + ⌜m0⌝ < # σ, ⌜m0⌝ < # σ, a ∈ lf(n0), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → (m = 0 ⊃ lf(0);lf(m).tail) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. n ≠ 0 → ii(n) ≠ 0, ∀ n. ii(n + 1) = ii(n) + # (n = 0 ⊃ lf(0);lf(n).tail) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # (n = 0 ⊃ lf(0);lf(n).tail) = ⌜(n = 0 ⊃ lf(0);lf(n).tail)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n).last = lf(n + 1).head ∧ lf(n) ≠ [], ∀ n. σ[ii(n + 1) - 1] = lf(n + 1).head ⊦ lf(n0) = [], ⌜σ[m0] '⌝ + (σ from m0 + 1) to # lf(n0) = ⌜lf(n0)⌝ |
Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m + 1 ≠ 0; (s)%in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list%a: ⊦ (x + y) + z = x + y + z; from specification list% ⊦ #(x + y) = # x + # y; (s)% ⊦ # a ' = 0 +1; (s)% ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)% ⊦ n + 0 = n; (s)% ⊦ m + n = m + n0 ↔ n = n0; (s)% ⊦ (a ' + x).head = a; (s)% ⊦ a ' + x ≠ []; (s)% ⊦ ⌜a '⌝ + σ to n + 1 = a + (σ to n); (s)% ⊦ a + σ = ⌜a '⌝ + σ; (s)%append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream% ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s)% ⊦ ⌜a '⌝ + σ = ⌜a0 '⌝ + σ0 ↔ a = a0 ∧ σ = σ0; (ws)%n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n0, m1