| #((σ 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 |
⊦ ⌜m⌝ < # σ → (σ + σ1)[m] = σ[m]
¬ ⌜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
Used simplifier rules: 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⌝ < # σ;%add-fin: ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; from specification nat-inf%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; 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%le-add: ⊦ m + m0 ≤ m ↔ m0 = 0; from specification nat%add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf%add-base: ⊦ n + 0 = n; from specification nat-basic2%add-all-zero: ⊦ n∞ + ⌜0⌝ = n∞; from specification nat-inf%add-less: ⊦ n∞1 < n∞ + n∞1 ↔ ¬ ¬(n∞ ≠ ⌜0⌝ ∧ n∞1 ≠ ∞); from specification nat-inf%ls-natinf-to-nat-2-2: ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; from specification nat-inf%l: ⊦ m + n < m + n0 ↔ n < n0; from specification nat-basic2%ls-lsadd: ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; from specification nat-inf Used terms: n, σ0, (σ to m + n0) from m