Hyperoperation sequence

This file defines the Hyperoperation sequence. hyperoperation 0 m k = k + 1 hyperoperation 1 m k = m + k hyperoperation 2 m k = m * k hyperoperation 3 m k = m ^ k hyperoperation (n + 3) m 0 = 1 hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

References

• https://en.wikipedia.org/wiki/Hyperoperation

Tags

hyperoperation

@[irreducible]

def hyperoperation : ℕ → ℕ → ℕ → ℕ

Implementation of the hyperoperation sequence where hyperoperation n m k is the nth hyperoperation between m and k.

Equations

• hyperoperation 0 x✝ x = x + 1
• hyperoperation 1 x 0 = x
• hyperoperation 2 x 0 = 0
• hyperoperation n.succ.succ.succ x 0 = 1
• hyperoperation n.succ x k.succ = hyperoperation n x (hyperoperation (n + 1) x k)

@[simp]

theorem hyperoperation_zero (m : ℕ) : hyperoperation 0 m = Nat.succ

theorem hyperoperation_ge_three_eq_one (n : ℕ) (m : ℕ) : hyperoperation (n + 3) m 0 = 1

theorem hyperoperation_recursion (n : ℕ) (m : ℕ) (k : ℕ) : hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

@[simp]

theorem hyperoperation_one : hyperoperation 1 = fun (x1 x2 : ℕ) => x1 + x2

@[simp]

theorem hyperoperation_two : hyperoperation 2 = fun (x1 x2 : ℕ) => x1 * x2

@[simp]

theorem hyperoperation_three : hyperoperation 3 = fun (x1 x2 : ℕ) => x1 ^ x2

theorem hyperoperation_ge_two_eq_self (n : ℕ) (m : ℕ) : hyperoperation (n + 2) m 1 = m

theorem hyperoperation_two_two_eq_four (n : ℕ) : hyperoperation (n + 1) 2 2 = 4

theorem hyperoperation_ge_three_one (n : ℕ) (k : ℕ) : hyperoperation (n + 3) 1 k = 1

theorem hyperoperation_ge_four_zero (n : ℕ) (k : ℕ) : hyperoperation (n + 4) 0 k = if Even k then 1 else 0