| #((σ 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⌝ |
⊦ ⌜n⌝ < # σ ∧ finp(σ) → #(σ from n) = ⌜(# σ).n - n⌝
#((σ from m) to n) = #((σ to m + n) from m), #(σ from m) < ⌜n⌝ , ⌜n0⌝ < #((σ from m) to 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-from: ¬ # x < n ⊦ #(x from n) = # x - n;%length-to: ¬ # x < n ⊦ #(x to n) = n;%get-finto: ¬ # x < n, m < n ⊦ (x to n)[m] = x[m];%get-from-01: m + m0 < # x ⊦ (x from m)[m0] = x[m + m0];% ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%stream-fin-forward: ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ); (forward) from specification stream-basic% ⊦ m < n → n ≠ 0; (s)% ⊦ finp(⌜x⌝ ); (s)% ⊦ m < n → ¬ n < m; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ ⌜m⌝ .n = m; (s)% ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (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%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ ¬ m + n < m; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + n - m = n; (s)% ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; (s)%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat% ⊦ # x = 0 ↔ x = []; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s) Used terms: m, σ