Counters: digits as cells, words, and blocks with fuel

1Digits as cells: the Example.v counter

1RB1LA_0LA0RB is the counter from busycoq's tutorial file Example.v. Whenever B stands on cell 1 reading a blank, the cells to its left spell a binary number, and brackets appear under them. From a blank tape, every step:

It reads 1 at step 1, 10 at step 5, 11 at step 7 and 100 at step 13. Steps 7 to 13 add 1 to 11: B0 turns the head left as A, A walks over the 1s and leaves them alone (A1 = 1LA), writes a 1 on the first 0 (A0 = 1RB), and B walks back right turning each 1 into 0 (B1 = 0RB).

That is the whole carry. Over k low 1s it takes 2k + 2 steps: 6 here.

Keep just the reading moments and the history is binary counting: 1, 10, 11, 100, … up to 1111 at step 51. Tap a row to see its tape.

The tape grows only when every digit is 1 and the carry runs off the end. That happens at steps 3, 10, 25, 56, 119, … (the n-th new cell at step 2ⁿ⁺² − n − 4), so each new cell takes about twice as long as the last. After 100,000 steps the tape spans just 16 cells.

the carry as a Coq lemma, step by stepthis counter in the explorer

2Digits as words: W5-3's counter

W5-3 (1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC, one of our kills) keeps its counter right of the head. A digit is two cells: 11 is 1 and 00 is 0. The lowest digit is again the one next to the head, so the number reads backwards: 11 11 00 11 is 1011 in binary, 11.

The rows read 4, 5, 6, … 11. Between two rows the head makes a trip into the word on the left (module 4) and adds 1 on its way back.

Rows 606 to 636 are the trip into the word on the left (module 4); the jump buttons skip it. Each step below names the rule the widget shows as rule used on that row:

• 637–644 A1 (= 1RA): A walks right over cells 10 to 17 without changing them: the two 1s just left of the counter, then the counter's six 1s.
• 645–646 A0 writes a 1 on cell 18, then B0 writes a 1 on cell 19 and turns the head back left: a new digit 11 on the blank cells just past the counter.
• 647 C1 steps back over cell 18 and leaves its 1.
• 648–655 D1 (= 0LD): D walks back left and turns cells 17 … 10 into 0s. That clears the counter, and also the two 1s left of it.
• 656–661 the head writes those two 1s back (now on cells 9 and 10) and stops as B on cell 11, where the counter reads 8.

So 11 11 11 (7) became 00 00 00 11 (8). It is the Example.v carry, mirrored and two cells at a time. W5-3's Coq file calls this counter busycoq's BinInc [1;1] N, where [1;1] is the word for digit 1.

W5-3 in the explorer

3Digits as blocks with fuel: #11

#11 (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, accepted upstream) writes each digit as two runs: 10 10 …, then 01 01 …. If the runs touch, the digit is 1. If a 00 sits between them, the digit is 0. The number of 01s is the digit's fuel.

Two more parts frame the digits. The start is a fixed 10 01 at the far left. The end block is (10)^a 000 (10)^b, between the low digit and the head: a run of 10s, three blanks, another run of 10s. ((10)^4 means 10 four times.)

Compare the chips. Both digits the carry touched have one 01 less (fuel 3 → 2 and 2 → 1). The digit that flipped to 1 lost its 00 and gained a 10.

The end block grew too, from (10)^4 000 10 to (10)^5 000 (10)^3, and the head now stands 4 cells further right. That happens on every carry, so #11's tape keeps widening.

The jump buttons stop at each part of the carry:

• 284–298 a short dip left into the end block's 000, and back to the right edge.
• 299–328 one long walk left, 30 cells. The head rewrites the cells it crosses, so for a while the digits look scrambled (watch the history): the end block's 10s turn into 01s, for example. It stops on the 00 of the 0-digit, at cell −8.
• 328–330 the flip (rules D0, A0, B1): that 00 becomes 10, so the digit now reads 1.
• 331–383 back to the right in a zig-zag: two cells back after every four or eight forward, until step 372, then a straight run to the new edge. On the way the head unscrambles each digit. The flipped digit gets its 01s back, the low digit comes back as a 0 (10 00 01), and the end block's 01s turn back into 10s.

Each row is one counter reading. Three kinds of move take one row to the next:

• Carry: the add-1 you just watched. Every digit it touches burns one 01.
• Overflow (steps 752, 1,393, 2,146): every digit is 1, so a different move runs. It swaps the two halves of every digit (10s become 01s and 01s become 10s), and the end block's 10s become the fuel of a new low digit. The counter reads 0…01, one digit longer. This is where fuel comes from: at step 483 the end block holds (10)^8, and at step 752 the new low digit has fuel 8.
• Drop (steps 908, 2,854): the carry flips a 0-digit that has fuel 1, which spends its last 01. A digit with no 01s is just 10s, so it merges into the 10s on its right, and the counter loses the 1 it just wrote. At step 752 it reads 01; adding 1 should give 10, but at step 908 it reads 0. In the same way 011 (step 2,546) plus 1 reads 00 (step 2,854), not 100.

So #11 is not a plain binary counter: its digits come and go. Its rules fail only if a carry reaches a 0-digit with no fuel at all, and its proof is an invariant showing that never happens (module 5).

#11 in the explorer (right-record rows)

4Where "Skelet 1-like" comes from

The holdout list files #11, #3 and W4-3 under the class "Skelet 1-like Class 2". The name comes from Skelet #1, the BB(5) machine 1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC, which busycoq proves never halts in Skelet1.v, following sligocki's 2023 post.

What they share: the post shows that Skelet #1 spends almost all its time counting up a base-4 counter whose digits (C0 to C3 in Skelet1.v) are short blocks of cells, with filler between them. Its digits are blocks of cells, not single cells, and so are the digits of #11 (two runs), #3 (pairs of blocks) and W4-3 (a chain of digit blocks).

W4-3's counter counts in base 3 and lives in its defects (module 2 shows them). Its proof is a 2,583-line Coq file, so this guide stops at the name.

W4-3's defects in module 2W4-3 with the background removed, in the explorer