| mon≤(nσ) ∧ n1 + m + 1 ≤ n ∧ ⌜n⌝ < # nσ → nσ[n1 + m + 1] ≤ nσ[n], nσ[n] = nσ[n1] + 1, # nσ = ⌜m0⌝ + ⌜1⌝ , nσ[n] ≤ nσ[m0], n1 + m + 1 < m0, n ≤ m0, n1 + m + 1 < n, nσ[n1] < nσ[m0], stutf(nσ), n1 < m0, ∀ m. ¬ m0 < m ∧ nσ[m] = nσ[n1] → ¬ n1 < m, ∀ m. ¬ m0 < m ∧ nσ[m] = nσ[n] → ¬ n < m ⊦ n = 0, nσ[n1 + m + 1] = nσ[n], nσ[m0] = 0, m0 = 0, n1 = m0 |
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
Used simplifier rules: stutf-monle: ⊦ stutf(nσ) → (¬ mon≤(nσ) ↔ false);%lels: ⊦ ¬ m < n ↔ n ≤ m; from specification nat%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic1%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%nls-fst: ⊦ ¬ m < n → ¬ m + m0 < n; from specification nat-basic2%lels-02: ⊦ m ≠ n → (m ≤ n ↔ m < n); from specification nat%le-ls-simp: ⊦ m ≤ n → (n < m ↔ false); from specification nat%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2%inf-inseq-reduce: ⊦ n∞ = ⌜m⌝ + ⌜n0⌝ → (⌜n⌝ < n∞ ↔ n < m + n0); from specification nat-inf%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%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%succ-01: ⊦ m + 1 ≤ n ↔ m < n; from specification nat