ack_three — Mathlib

English

A(3,n) = 2^{n+3} - 3 for all n.

Русский

A(3,n) = 2^{n+3} - 3 для всех n.

LaTeX

$$$$\operatorname{ack}(3,n) = 2^{n+3} - 3.$$$$

Lean4

@[simp]
theorem ack_three (n : ℕ) : ack 3 n = 2 ^ (n + 3) - 3 := by
  induction n with
  | zero => simp
  | succ n
    IH =>
    rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2, Nat.mul_sub_left_distrib, ←
      Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]
    calc
      2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> omega

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