| #(σ from m) < ⌜n⌝ ⊦ #((σ from m) to n) = #((σ to m + n) from m), # σ < ⌜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⌝ ;%length-to: ¬ # x < n ⊦ #(x to n) = n;%length-from: ¬ # x < n ⊦ #(x from n) = # x - n;%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;%stream freely generated by ⌜ ⌝, ⌜ ⌝;;%l-02: ⊦ ¬ m + n < m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%eq-01: ⊦ m + n - m = n; from specification nat%inj: ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; from specification nat-inf-basic%less-fin: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; from specification nat-inf%ls-natinf-to-nat-1-2: ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; from specification nat-inf%lels: ⊦ ¬ m < n ↔ n ≤ m; from specification nat%ls-le-simp: ⊦ m < n → (n ≤ m ↔ false); from specification nat%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%ls-lsadd: ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; from specification nat-inf%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%ls-01: n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; from specification nat