| mon≤(nσ) ∧ m0 ≤ n1 + m + 1 ∧ ⌜n1 + m + 1⌝ < # nσ → nσ[m0] ≤ nσ[n1 + m + 1], nσ[n] = nσ[n1] + 1, # nσ = ⌜m0⌝ + ⌜1⌝ , nσ[n1 + m + 1] < nσ[m0], n1 + m < m0, nσ[n1 + m + 1] < nσ[n], n1 + m < n, nσ[n] ≤ nσ[m0], n1 + m + 1 < m0, n ≤ m0, n1 + m + 1 < n, nσ[n1] < nσ[m0], stutf(nσ), n1 < m0, nσ[n1 + m + 1] ≤ nσ[n1], ∀ m. ¬ m0 < m ∧ nσ[m] = nσ[n1] → ¬ n1 < m, ∀ m. ¬ m0 < m ∧ nσ[m] = nσ[n] → ¬ n < m ⊦ nσ[n] = 0, n = 0, nσ[n1 + m + 1] = nσ[n], nσ[m0] = 0, m0 = 0, n1 = m0 |
# nσ = ⌜m0⌝ + ⌜1⌝ , nσ[n] = nσ[n1] + 1, nσ[n1 + m + 1] ≤ nσ[n1], n1 < m0, stutf(nσ), nσ[n1] < nσ[m0], n1 + m + 1 < n, n ≤ m0, n1 + m + 1 < m0, nσ[n] ≤ nσ[m0], n1 + m < n, nσ[n1 + m + 1] < nσ[n], n1 + m < m0, nσ[n1 + m + 1] < nσ[m0], ∀ m. ¬ m0 < m ∧ nσ[m] = nσ[n] → ¬ n < m, ∀ m. ¬ m0 < m ∧ nσ[m] = nσ[n1] → ¬ n1 < m ⊦ n1 = m0, m0 = 0, nσ[m0] = 0, nσ[n1 + m + 1] = nσ[n], n = 0, nσ[n] = 0, m0 = (n1 + m) + 1
Used simplifier rules: stutf-monle: ⊦ stutf(nσ) → (¬ mon≤(nσ) ↔ false);%ref-1: ⊦ ¬ n < n; from specification nat-basic1%eq: ⊦ m = m + n ↔ n = 0; from specification nat-basic2%oz: ⊦ m + 1 ≠ 0; 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%num-add: ⊦ ⌜(* n)⌝ + ⌜(* m)⌝ = ⌜n + m⌝ ; from specification nat-inf%ls-le-simp: ⊦ m < n → (n ≤ m ↔ false); from specification nat%add-fin: ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; from specification nat-inf%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%les: ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); from specification nat