| ¬ ⌜n⌝ < #((σ to m + n0) from m), #((σ to n0 + m) + σ0 from m) = #((σ to m + n0) from m) + # σ0, ⌜n⌝ < #((σ to m + n0) from m) + # σ0, ⌜n0⌝ + # σ0 < #((σ to m + n0) from m) + # σ0 ⊦ ((σ to n0 + m) + σ0 from m)[n] = (((σ to m + n0) from m) + σ0)[n], # σ < ⌜n0⌝ + ⌜m⌝ , # σ < ⌜m⌝ + ⌜n0⌝ , ⌜n⌝ < ⌜n0⌝ + # σ0 |
#((σ to n0 + m) + σ0 from m) = #((σ to m + n0) from m) + # σ0, ⌜n⌝ < #((σ to m + n0) from m) + # σ0, ⌜n0⌝ + # σ0 < #((σ to m + n0) from m) + # σ0, n0 ≤ n ⊦ ((σ to n0 + m) + σ0 from m)[n] = σ0[n - (#((σ to m + n0) from m)).n], # σ < ⌜n0⌝ + ⌜m⌝ , # σ < ⌜m⌝ + ⌜n0⌝ , ⌜n⌝ < ⌜n0⌝ + # σ0
Used simplifier rules: get-append-notls: ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)[m] = σ1[m - (# σ).n];%append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2;%size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ;%size-empty-equiv: ⊦ # σ = ⌜0⌝ ↔ σ = [];%ton-fromn: ⊦ ¬ # σ < ⌜n⌝ → (σ to n) from n = [];%size-empty: ⊦ # [] = ⌜0⌝ ;%less-size-from: ⌜n⌝ < # σ ⊦ ⌜n0⌝ < #(σ from n) ↔ ⌜n0 + n⌝ < # σ;%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%sub-base: ⊦ m - 0 = m; from specification nat%sel: ⊦ ⌜m⌝ .n = m; from specification nat-inf-basic%add-less: ⊦ n∞1 < n∞ + n∞1 ↔ ¬ ¬(n∞ ≠ ⌜0⌝ ∧ n∞1 ≠ ∞); from specification nat-inf%add-all-zero: ⊦ n∞ + ⌜0⌝ = n∞; from specification nat-inf%add-base: ⊦ n + 0 = n; from specification nat-basic2%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%le-add: ⊦ m + m0 ≤ m ↔ m0 = 0; from specification nat%lels: ⊦ ¬ m < n ↔ n ≤ m; from specification nat%ls-natinf-to-nat-1-2: ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; 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