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

@[irreducible]
def hyperoperation :

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

Equations
Instances For
    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_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