ack_succ_right_le_ack_succ_left — Mathlib

English

For all m,n, ack(m, n+1) ≤ ack(m+1, n).

Русский

Для всех m,n: Ackermann(m, n+1) ≤ Ackermann(m+1, n).

LaTeX

$$$$\\forall m,n \\in \\mathbb{N}, \\ operatorname{ack}(m, n+1) \\le \\ operatorname{ack}(m+1, n).$$$$

Lean4

theorem ack_succ_right_le_ack_succ_left (m n : ℕ) : ack m (n + 1) ≤ ack (m + 1) n :=
  by
  rcases n with - | n
  · simp
  · rw [ack_succ_succ]
    apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)
    cutsat
      -- All the inequalities from this point onwards are specific to the main proof.

Похожие утверждения