About

This is a Brainfuck busy beaver champion.

>+++++++[-[-[->>[+>]+[<]<]+>+[>]]>+<<]

Update: The following shorter variant produces a slightly smaller number, but we analyse the above, earlier version first:

>++++++[-[-[->>[>]+[+<]<]+>+[>]]>+<<]

With wrapping cells, one can replace the >++++++ by >-.

Execution

The state of the program at the start of the outer loop has the shape

0 n₁ n₂ ... n_k-1 *n_k 0 1 ... 1 0

where n₁...n_k are positive integers, the pointer points to the n_k and there are m 1-s to the right of the pointer.

If n_k = 1, the loop changes this to the following, incrementing m by 1:

0 n₁ n₂ ... *n_k-1 0 1 1 ... 1 0

Otherwise, the loop replaces the m 1-s by n_k-1 and adds some more, smaller numbers, and sets m to 1:

0 n₁ ... n_k-1 1 1 n_k-1 ... n_k-1 n_k-2 ... *1 0 1

Note that because m is stored in unary and the n_k never increase, all cells stay in range 0..7 at all times.

We can read the part to the left of the pointer as a stack for a program that evaluates

α_n₁∘...∘α_{n_k}(m)

where α_n(m) is similar to the Ackermann function

α₁(m) = 1+m

α_n(m) = α₁∘α₁∘α_n-1^m∘α_n-2∘...∘α₁(1)

We can show by induction that

α₂(m) = 3+m

α₃(m) = 3m+4

α₄(m) = 7·3^m

The program evaluates

α₇(0) = α₁∘α₁∘α₅∘α₄∘α₃∘α₂∘α₁(1)

= 2 + α₅(8135830269)

= 2 + α₁∘α₁∘α₄^8135830269∘α₃∘α₂∘α₁(1)

> 3 ↑ 8135830269

The modified program executes in a similar way but it defines the function

β₁(m) = 1+m

β_n(m) = β₁∘β₁∘β_n-1^m∘β_n-1∘...∘β₂(1)

(Note the increased subscripts to the right.) We can show by induction that

β_n(m) = α_n(m+1) - 1

So

β₆(0) = α₆(1) - 1 = α₇(0) - 1 > 3 ↑ 8135830269