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 #

Tags #

hyperoperation

def hyperoperation :

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

Equations
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_four_zero (n : ) (k : ) :
hyperoperation (n + 4) 0 k = if Even k then 1 else 0