mathlib3 documentation

data.nat.hyperoperation

Hyperoperation sequence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations
@[simp]
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)
theorem hyperoperation_ge_two_eq_self (n m : ) :
hyperoperation (n + 2) m 1 = m
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 = ite (even k) 1 0