| #((σ to n0 + m) + σ0 from m) = ⌜n1⌝ + # σ0, #((σ to m + n0) from m) = ⌜n1⌝ , ⌜n1⌝ < ⌜n0⌝ + # σ0, ⌜n2⌝ < # σ0, ⌜n2⌝ + ⌜n1⌝ < ⌜n0⌝ + # σ0, n1 + n2 < n0 ⊦ σ0 = [], σ[m + n2 + n1] = σ0[n2], n0 = 0, # σ < ⌜n0⌝ + ⌜m⌝ , # σ < ⌜m⌝ + ⌜n0⌝ |
Used simplifier rules: to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ;%from-fin: ⊦ ⌜x⌝ from n = ⌜x from 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;%to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to 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-inf: ⊦ ⌜nf⌝ [n] = nf(n);%size-inf: ⊦ # ⌜nf⌝ = ∞;%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-inf1: ⊦ ¬ ∞ < n∞; from specification nat-inf%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic1%l-05: ⊦ m + m0 < n → ¬ n + n0 < m; from specification nat-basic2%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%le-ls-simp: ⊦ m ≤ n → (n < m ↔ false); from specification nat