1RB0RF_1RC0LD_1LB1RC_---0LE_1RA1LE_---0RC
1RB0RF_1RC0LD_1LB1RC_---0LE_1RA1LE_---0RC (bbch) is a machine on the critical path to proving the busy beaver value "BB(6, 2, 2)" (6-state, 2-symbol, 2 undefined transitions).
(Machines 1RB0RB_1LC1RB_---0LD_1RA0LE_1RF1LE_---0RA (bbch), 1RB1LA_1LA0RC_---0RD_1LE1RD_0LA0LF_---0LA (bbch), and 1RB1LA_1LA0RC_---0RD_1LE1RD_1LB0LF_---0LA (bbch) [1] appear to be in the same category.)
The machine behaves as a double counter in base 2; at key steps, the left and right tapes are and must be mirror images (aside from a terminal "1" on the right). It's easily proven infinite as follows by forward analysis: we can define a CFL [1] where <L> shows the rule "0(11)*1B1 -> (11)*1C>", and <M> is a closed language for the TM:
<L> ::= 0(11)*(1B1|D10)
| 0(11)*(1E1|E11)(11)*00
| E0(11)*00
| 1A00|11B0
| (1A11|10F1)(11)*00
| 100(11)*(C11|1C1)(11)*00
| 100(11)*C00
| 10B010|101C10|1011C0|101B11|10D101|1E0001|11A001|111B01|1111C1
| 10<L>10
| 10(11)*(1C10|11C0)
| 1<L>1
| 1(11)*1C1
<M> ::= A0|1B0
| (11)*11C0
| <L>1
| (11)*1(C1|1C0)
In particular, <L> includes 10<L>10 and 1<L>1, but not for example 1<L>10; indeed, a config of the form (1<L>10)1 will halt the TM. It therefore provides an example of "BB(6, 2, 2)" needing an inductive or closed-language decider stronger than (weighted) finite automata methods.
Note: A simpler multi-symbol example of the phenomenon is 1RB2LA0LA_1LA2RC0RC_---2RB0RB (bbch), with the rule "bin(n) <A reversed(bin(n)) |- bin(n+1) <A reversed(bin(n+1))".
References
- ↑ The holdout list omits the last one. Since holdout lists are useless, it's unspecified whether this case was easier or pruned.