Documentation

Mathlib.Data.Nat.Hyperoperation

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

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 (Nat.succ (Nat.succ (Nat.succ n))) x 0 = 1
hyperoperation (Nat.succ n) x (Nat.succ k) = 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 x x_1 => x + x_1

@[simp]

theorem hyperoperation_two :

hyperoperation 2 = fun x x_1 => x * x_1

@[simp]

theorem hyperoperation_three :

hyperoperation 3 = fun x x_1 => x ^ x_1

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