| ⌜m0⌝ < # σ, m0 + 1 = #(y + a '), (σ to m0) + ⌜σ[m0] '⌝ = ⌜y + a '⌝ , ii(0) = 0, ii(1) = m0 + 1, lf(1) = a ' + x0, ⌜m0⌝ < # σ, a ∈ lf(1), ∀ n. n ≠ 0 → ii(n) ≠ 0, ∀ n. ii(n + 1) = ii(n) + # (n = 0 ⊃ y + a ';lf(n).rest) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # (n = 0 ⊃ y + a ';lf(n).rest) = ⌜(n = 0 ⊃ y + a ';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 ⊃ y + a ';lf(m).rest) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ y + a ' = [], σ[m0] = a, lf(1) = [] |
(σ to # y) + ⌜σ[# y] '⌝ = ⌜y⌝ + ⌜a '⌝ , lf(1) = a ' + x0, ii(1) = # y + 1, ii(0) = 0, a ∈ lf(1), ⌜# y⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → (m = 0 ⊃ y + a ';lf(m).rest) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. lf(n).last = lf(n + 1).first ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # (n = 0 ⊃ y + a ';lf(n).rest) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # (n = 0 ⊃ y + a ';lf(n).rest) = ⌜(n = 0 ⊃ y + a ';lf(n).rest)⌝ , ∀ n. n ≠ 0 → ii(n) ≠ 0 ⊦ lf(1) = [], σ[# y] = a
Used simplifier rules: in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list%e-02: ⊦ x + a ' ≠ []; from specification list%append-finfin: ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; from specification stream%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%eq-01: ⊦ m + n = m + n0 ↔ n = n0; from specification nat-basic2%a: ⊦ (x + y) + z = x + y + z; from specification list%len-02: ⊦ # a ' = 0 +1; from specification list%len: ⊦ #(x + y) = # x + # y; from specification list