hyperoperation_recursion
theorem hyperoperation_recursion :
∀ (n m k : ℕ), hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)
This theorem states a recursion property of the hyperoperation sequence. For all non-negative integers `n`, `m`, and `k`, the (n+1)th hyperoperation between `m` and (k + 1) is equal to the nth hyperoperation between `m` and the result of the (n + 1)th hyperoperation between `m` and `k`. In other words, the value of a hyperoperation at a certain level is derived from the value of the hyperoperation at the previous level and the current level.
More concisely: For all non-negative integers n, m, and k, the (n+1)th hyperoperation between m and k is equal to the nth hyperoperation between m and the (n+1)th hyperoperation result between m and k.
|
hyperoperation_ge_three_eq_one
theorem hyperoperation_ge_three_eq_one : ∀ (n m : ℕ), hyperoperation (n + 3) m 0 = 1
The theorem `hyperoperation_ge_three_eq_one` states that for all natural numbers `n` and `m`, the `n+3`rd hyperoperation applied to `m` and `0` is always equal to `1`. Here, the hyperoperation is a sequence of operations defined such that `hyperoperation n m k` is the `n`th operation applied between `m` and `k`.
More concisely: For all natural numbers n and m, the n+3-th hyperoperation between m and 0 is equal to 1.
|