| #((σ from m) to n) = #((σ to m + n) from m), ⌜n0⌝ < #((σ from m) to n), #(σ from m) < ⌜n⌝ ⊦ ((σ from m) to n)[n0] = ((σ to m + n) from m)[n0], # σ < ⌜m⌝ + ⌜n⌝ , ⌜m⌝ < # σ ∧ finp(σ) |
Used simplifier rules: from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ;%to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ;%size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ;%sel-fin: ⊦ ⌜x⌝ [n] = x[n];%length-to: ¬ # x < n ⊦ #(x to n) = n;%length-from: ¬ # x < n ⊦ #(x from n) = # x - n;%get-from-01: m + m0 < # x ⊦ (x from m)[m0] = x[m + m0];%get-finto: ¬ # x < n, m < n ⊦ (x to n)[m] = x[m];%from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ;%to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ;%inf-size-to: ⊦ # ⌜nf to n⌝ = ⌜n⌝ ;%from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ;%size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ;%size-inf-to: ⊦ #(nf to n) = n;%length-from: ¬ # x < n ⊦ #(x from n) = # x - n;%sel-fin: ⊦ ⌜x⌝ [n] = x[n];%get-from-01: m + m0 < # x ⊦ (x from m)[m0] = x[m + m0];%size-inf: ⊦ # ⌜nf⌝ = ∞;%stream freely generated by ⌜ ⌝, ⌜ ⌝;;% ⊦ ¬ m + n < m; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m + n - m = n; (s)% ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; (s)% ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ ¬ ∞ < n∞; (s)% ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s)%add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf%add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ m < n → n ≠ 0; (s)% ⊦ # x = 0 ↔ x = []; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)