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