| ⌜n1 + n⌝ < #((σ to n) + ⌜x⌝ ) ∧ finp((σ to n) + ⌜x⌝ ), # x = n2 + n1 ⊦ n2 = 0, x = [], n2 + n1 = 0, # σ < ⌜n⌝ , ⌜(#((σ to n) + ⌜x⌝ )).n - n1 + n⌝ = ⌜n2⌝ ∧ (n0 < n2 → ((σ to n) + ⌜x⌝ from n1 + n)[n0] = x[n1 + n0]) |
# x = n2 + n1, ⌜x0⌝ = (σ to n) + ⌜x⌝ , n0 < n2 ⊦ (x0 from n1 + n)[n0] = x[n1 + n0], n2 + n1 = 0, x = [], n2 = 0, # σ < ⌜n⌝
Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1;%size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ;%size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ;%append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2;%from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ;%sel-fin: ⊦ ⌜x⌝ [n] = x[n];%inj-02: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; from specification stream-basic%test-02: ⊦ finp(⌜x⌝ ); from specification stream-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%eq-01: ⊦ m + n - m = n; from specification nat%l-01: ⊦ m < m + n ↔ n ≠ 0; from specification nat-basic2%stream-fin-forward: ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ); (forward) from specification stream-basic%ls: n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; from specification nat%lels-03: ⊦ m < n → m ≤ n; from specification nat%inj: ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; from specification nat-inf-basic%cancel-01: ⊦ m + n - n + n1 = m - n1; from specification nat%sel: ⊦ ⌜m⌝ .n = m; from specification nat-inf-basic%prime-add-fin: n∞ ≠ ∞ ⊦ (⌜m⌝ + n∞).n = m + n∞.n; from specification nat-inf%disj: ⊦ ⌜m⌝ ≠ ∞; from specification nat-inf-basic%addeqinf-cancel: ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; from specification nat-inf%add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf%add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf%l: ⊦ m + n < m + n0 ↔ n < n0; from specification nat-basic2%ls-natinf-to-nat-2-2: ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; from specification nat-inf%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%add-fin: ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; from specification nat-inf