Registry · Definition I.D13 established formalized

I.D13 — Index Tetration

n ^^m = n^(n^(...^n)) (m times): tetration earned by structural recursion on exponentiation. Terminal operation (ladder saturates here).

Book I Part 3 Ch. 12

Dependency Graph

Depends on (3)

Depended on by (3)

Lean Formalization

Module: TauLib.BookI.Denotation.Arithmetic

Symbol: Tau.Denotation.idx_tetration