ack_ack_lt_ack_max_add_two — Mathlib

English

For all m,n,k, ack(m, ack(n,k)) < ack(max(m,n) + 2, k).

Русский

Для всех m,n,k: ack(m, ack(n,k)) < ack(max(m,n) + 2, k).

LaTeX

$$$$\\forall m,n,k \\in \\mathbb{N}, \\operatorname{ack}(m, \operatorname{ack}(n,k)) < \\operatorname{ack}(\\max(m,n) + 2, k).$$$$

Lean4

theorem ack_ack_lt_ack_max_add_two (m n k : ℕ) : ack m (ack n k) < ack (max m n + 2) k :=
  calc
    ack m (ack n k) ≤ ack (max m n) (ack n k) := ack_mono_left _ (le_max_left _ _)
    _ < ack (max m n) (ack (max m n + 1) k) :=
      (ack_strictMono_right _ <| ack_strictMono_left k <| lt_succ_of_le <| le_max_right m n)
    _ = ack (max m n + 1) (k + 1) := (ack_succ_succ _ _).symm
    _ ≤ ack (max m n + 2) k := ack_succ_right_le_ack_succ_left _ _

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