Sync bouncer counter

A sync bouncer counter is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:

• It has both a bouncer and a counter on the tape, and the lowest digit of the counter is adjacent to the bouncer.
• Increment: the counter is increased by one, and the bouncer finishes a period.
• Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).

A Coq proof of a kind of typical behavior doesn't halt.

Examples

1RB0LF_0RC---_1RD1LE_0RE0LA_1LF0RF_0LC0LB (bbch) (most common)

1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA (bbch) (complex)