# Proving BB(5) in Coq

I’m working on proving correctness of deciders in Coq.
Now only some simple deciders are proved, and there are 82 holdouts (58 of them write 1 at the first step).
Used deciders:

1. translated cycle
2. n-gram-CPS with local update history
3. CTL limited to fixed word length and no “|”
See readme code for more details.
2 Likes

Wow, this looks like a very fresh approach to piecing together BB(5) from available techniques. You’ve got my interest.
If I may ask, have you been active here for a while? I’m not aware of Nathan’s nice CPS variant being well advertised outside of Discord?
Also, would you mind sharing a holdout list (with the caveat that more compute might change things)? Are they likely TNF leaves or interior nodes corresponding to many individual TMs?

Here is the holdout list, they are all TNF leaves.
holdouts.txt (3.3 KB)

[upd 2024.4.30]:
23 TMs are solved by a FAR verifier
17 TMs are solved by a Weighted Automata verifier
347505 is solved by limited CTL
5877285,6244297,7174252,7174254 are solved by n-gram-CPS

[upd 2024.5.10]:
The proof is finished.

2 Likes

I found this website two weeks ago, and read n-gram-CPS from https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/2.
Since n-gram-CPS seems easy to implement, I reimplement the version described in readme and found that it fails on many trivial cases (e.g. cannot distinguish the length of 1111…1 mod 2).
Add more history information to the tape helps a lot in many cases.
For example, if 1111…11 is generated by a translated cycle of shift 2, and the transition of last update of each position is recorded on the tape, it may look like (1,(A,0))(1,(B,1))(1,(A,0))(1,(B,1))…(1,(A,0))(1,(B,1)).
However, fixed length historical information is not enough, as nested loops may overwrite all useful historical information. LRU cache is a solution (but not perfect) for this: we can record the order of the last occurrence of all 10 possible transitions in each position.

2 Likes

I’ve translated your list to terms more familiar to us, below.
Let me reiterate how impressive these results are. A limitation is that machines not marked as “Regular” below cannot be solved by the techniques you’ve described (we think). However, we know how to solve them between individual proofs in @meithecatte’s BusyCoq repo and a weighted automata technique in @Iijil’s MITMWFAR repo. [EDIT: except Skelet #17, whose BusyCoq proof is under construction. Proof write-ups have been posted to our Discord.]

The “Regular” ones are solvable with CTL/FAR techniques, perhaps including your own with more compute. Let me know if you’d like me to dig up more info about the proofs we know about for these ones.

Holdout BBChallenge Text BBChallenge ID Type
BR0 AL0 CR1 HR1 DR0 EL1 ER1 DR1 AL1 CL1 `1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE` 572659 Shift Recursive
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 DL1 `1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD` 3841643 Regular
BR1 CL1 AL1 BR1 DL1 AL0 ER1 DR0 HR1 BR0 `1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB` 12554268 Regular (Sk. 9)
BR0 BL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 `1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA` 8210684 Shift Recursive
BR0 EL0 CL1 BR1 BR1 DL1 HR1 AL0 AR0 EL1 `1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE` 11218583 Regular
BR1 HR1 CR0 BR0 CL1 DL0 AR1 EL0 AL0 EL0 `1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE` 14536286 Regular (Sk. 19)
BR1 HR1 CR0 BL1 DR1 CR1 EL1 DL1 AR0 EL0 `1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE` 472097 Shift Recursive
BR0 AL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 `1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE` 8210685 Shift Recursive
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AL1 HR1 `1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA` 10818510 Shift Recursive
BR1 DL0 CR1 BL0 DR0 HR1 ER1 BL0 AL1 AR0 `1RB0LD_1RC0LB_0RD---_1RE0LB_1LA0RA` 7174254 Regular
BR0 CL0 CR1 BR1 DL1 EL0 HR1 EL1 AR1 AL1 `1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB` 8176549 Regular
BR1 CR0 CL1 EL0 DL0 BL0 AR1 HR1 BL1 DR0 `1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD` 4817065 3N (“Helix”)
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 ER1 `1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE` 11896833 Shift-Overflow
BR1 BL0 CL1 ER0 DL1 CR0 EL0 HR1 AL1 AL0 `1RB0LB_1LC0RE_1LD0RC_0LE---_1LA0LA` 6244297 Regular
BR1 BL1 CR0 DL0 DR1 CR1 EL1 AL0 HR1 AL1 `1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA` 11414657 Regular
BR1 AL1 CR1 DR1 AL0 ER0 HR1 CR0 CL0 ER1 `1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE` 11143983 Regular
BR0 AL0 CR1 HR1 DR0 DL1 ER1 DR1 AL1 EL1 `1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE` 523280 Shift Recursive
BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 `1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE` 347505 Regular (Sk. 20)
BR1 AR1 CL1 CL0 EL0 DR0 AR0 BL1 DL1 HR1 `1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD---` 60658955 Regular (Sk. 24)
BR1 AL1 CL0 ER0 HR1 DL1 AR1 CL0 AR1 ER1 `1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE` 11017998 N_2N (“Finned”)
BR1 DL0 CR1 AR0 DR0 BR0 EL1 HR1 BL1 CL0 `1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC` 7138511 3N (“Helix”)
BR0 AR0 CL1 HR1 DL0 CL0 ER0 BR1 ER1 AR1 `1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE` 35346 Regular
BR0 DL0 CR1 ER1 AL1 CR1 CL1 DL1 HR1 BR0 `1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA` 10756090 N_2N (“Finned”)
BR1 AR1 CR1 BL1 DL0 AR0 AR1 EL1 HR1 DL0 `1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD` 8120967 N_2N (“Finned”)
BR1 DR0 CR1 HR1 DL1 EL1 ER1 DL1 AR1 CL0 `1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC` 5057577 Regular
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 `1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA` 3841642 Regular
BR1 AR0 CL0 AR1 ER1 DL1 CL1 DL0 HR1 BR0 `1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB` 3810716 Skelet #10
BR0 CL0 CR1 HR1 DL0 ER1 EL1 DL1 AR1 AR0 `1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB` 20569060 Regular (Sk. 16)
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AR1 `1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA` 11896832 Shift-Overflow
BR1 HR1 CR1 BL1 DL1 ER1 BL1 DL0 AR1 CR0 `1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC` 2204428 Shift-Overflow
BR1 BR0 CR0 DL0 DR1 HR1 EL0 AR1 AL1 EL1 `1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE` 35771936 Regular (Sk. 38)
BR0 AL0 CR1 HR1 DR0 DR1 ER1 DR1 AL1 EL1 `1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE` 321080 Shift Recursive
BR1 HR1 CL0 CL1 DL1 BL1 ER1 DR1 AL0 ER0 `1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE` 1465912 Shift Recursive
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 CR1 `1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC` 36287 Regular
BR1 CR1 CL1 BR1 DL1 AR0 EL1 BL0 AL1 HR1 `1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA---` 9393627 Regular
BR1 EL0 CR1 BR1 DR1 CL1 EL0 BR0 HR1 AL1 `1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA` 7763480 N_2N (“Finned”)
BR1 AR1 CL1 BL1 DR0 CL0 ER1 HR1 AR0 AR1 `1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA` 8210683 Shift Recursive
BR1 DL1 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 `1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA` 13357563 Regular
BR0 AR1 CR1 DL1 DL1 BR1 EL0 AL0 HR1 DL0 `1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC` 12781955 Shift Recursive
BR1 AL1 CR1 EL0 DR1 AR0 ER1 HR1 AL1 BL1 `1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB` 11128264 Regular
BR1 HR1 CL0 ER1 DL0 CL1 AR1 BL1 BR0 AR0 `1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA` 1365166 Skelet #17
BR1 DL0 CR1 BL0 DR0 HR1 ER1 ER0 AL1 AR0 `1RB0LD_1RC0LB_0RD---_1RE0RE_1LA0RA` 7174252 Regular
BR0 AR1 CR1 DL1 CL1 BR1 EL0 AL0 HR1 DL0 `1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC` 12699987 Shift Recursive
BR1 AR1 CL1 EL1 DR0 CL0 ER1 HR1 AR0 BL1 `1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB` 8226493 Shift Recursive
BR1 DR1 CL1 CR0 AR1 DL1 ER0 BL0 HR1 CR1 `1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC` 68329601 Skelet # 1
BR1 HR1 CR0 CR1 DR1 BR1 EL1 DL1 AR0 EL0 `1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE` 320969 Shift Recursive
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 EL0 `1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE` 36285 Regular
BR1 ER0 CR0 AR0 DL1 HR1 AL1 BL0 AR1 CL0 `1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC` 5377178 3N (“Helix”)
BR1 AL0 CR0 HR1 DR1 DR0 EL1 ER0 AR1 CL0 `1RB0LA_0RC---_1RD0RD_1LE0RE_1RA0LC` 5877285 Regular
BR1 EL0 CR1 HR1 DR0 CR0 DL1 AL0 BL0 EL0 `1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE` 57874080 Regular (Sk. 42)
BR1 AR0 CL1 HR1 CL0 DL0 ER1 BR0 ER0 AR1 `1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA` 3841616 Regular (Sk. 40)
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AL0 `1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA` 11896831 Shift-Overflow
BR1 HR1 CL1 DL1 DR1 CL1 ER1 BL0 AR1 CR0 `1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC` 3656280 Regular
BR1 DL1 CR1 BR0 AL1 CR1 EL1 AL0 CL1 HR1 `1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---` 13134219 Shift-Overflow
BR1 HR1 CR0 BR0 DL0 EL1 DL1 CR1 AL1 EL0 `1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE` 36299 Regular
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AR1 HR1 `1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA` 10818491 Shift Recursive
BR1 DL0 CR1 ER0 DR1 HR1 EL1 AL1 AR1 EL1 `1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE` 7161825 Regular
BR1 AL1 CL0 ER0 HR1 DL1 AL1 CL0 AR1 ER1 `1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE` 11018487 N_2N (“Finned”)
3 Likes

Here’s the info about known proofs of the above holdouts.

This subset is solved by individual proofs alone (sometimes with common techniques/lemmas). We’re confident these aren’t regular, except technically Skelet 1 (becomes a translated cycler at ludicrous scales).

Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 ER1 `1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE` 11896833 Shift-Overflow Skelet33.v
BR1 AL1 CL0 ER0 HR1 DL1 AR1 CL0 AR1 ER1 `1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE` 11017998 N_2N (“Finned”) Finned4.v
BR0 DL0 CR1 ER1 AL1 CR1 CL1 DL1 HR1 BR0 `1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA` 10756090 N_2N (“Finned”) Finned3.v
BR1 AR1 CR1 BL1 DL0 AR0 AR1 EL1 HR1 DL0 `1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD` 8120967 N_2N (“Finned”) Finned2.v
BR1 AR0 CL0 AR1 ER1 DL1 CL1 DL0 HR1 BR0 `1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB` 3810716 Skelet #10 Skelet10.v
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AR1 `1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA` 11896832 Shift-Overflow Skelet34.v
BR1 HR1 CR1 BL1 DL1 ER1 BL1 DL0 AR1 CR0 `1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC` 2204428 Shift-Overflow Skelet15.v
BR1 EL0 CR1 BR1 DR1 CL1 EL0 BR0 HR1 AL1 `1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA` 7763480 N_2N (“Finned”) Finned1.v
BR1 HR1 CL0 ER1 DL0 CL1 AR1 BL1 BR0 AR0 `1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA` 1365166 Skelet #17 WIP / Discord
BR1 DR1 CL1 CR0 AR1 DL1 ER0 BL0 HR1 CR1 `1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC` 68329601 Skelet # 1 Skelet1.v
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AL0 `1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA` 11896831 Shift-Overflow Skelet35.v
BR1 DL1 CR1 BR0 AL1 CR1 EL1 AL0 CL1 HR1 `1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---` 13134219 Shift-Overflow Skelet26.v
BR1 AL1 CL0 ER0 HR1 DL1 AL1 CL0 AR1 ER1 `1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE` 11018487 N_2N (“Finned”) Finned5.v

This subset is solved by weighted automata, and listed (by bbchallenge text) in the cert files of MITMWFAR.
We’re confident these aren’t regular. The solution is CTL flavored, but the language class allows counting. The program can solve the 11 “shift recursive” ones by search. The 3N/helix ones, I solved by hand and translated.

Holdout BBChallenge Text BBChallenge ID Type Proof
BR0 AL0 CR1 HR1 DR0 EL1 ER1 DR1 AL1 CL1 `1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE` 572659 Shift Recursive Weighted Automata
BR0 BL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 `1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA` 8210684 Shift Recursive Weighted Automata
BR1 HR1 CR0 BL1 DR1 CR1 EL1 DL1 AR0 EL0 `1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE` 472097 Shift Recursive Weighted Automata
BR0 AL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 `1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE` 8210685 Shift Recursive Weighted Automata
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AL1 HR1 `1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA` 10818510 Shift Recursive Weighted Automata
BR1 CR0 CL1 EL0 DL0 BL0 AR1 HR1 BL1 DR0 `1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD` 4817065 3N (“Helix”) Weighted Automata
BR0 AL0 CR1 HR1 DR0 DL1 ER1 DR1 AL1 EL1 `1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE` 523280 Shift Recursive Weighted Automata
BR1 DL0 CR1 AR0 DR0 BR0 EL1 HR1 BL1 CL0 `1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC` 7138511 3N (“Helix”) Weighted Automata
BR0 AL0 CR1 HR1 DR0 DR1 ER1 DR1 AL1 EL1 `1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE` 321080 Shift Recursive Weighted Automata
BR1 HR1 CL0 CL1 DL1 BL1 ER1 DR1 AL0 ER0 `1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE` 1465912 Shift Recursive Weighted Automata
BR1 AR1 CL1 BL1 DR0 CL0 ER1 HR1 AR0 AR1 `1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA` 8210683 Shift Recursive Weighted Automata
BR0 AR1 CR1 DL1 DL1 BR1 EL0 AL0 HR1 DL0 `1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC` 12781955 Shift Recursive Weighted Automata
BR0 AR1 CR1 DL1 CL1 BR1 EL0 AL0 HR1 DL0 `1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC` 12699987 Shift Recursive Weighted Automata
BR1 AR1 CL1 EL1 DR0 CL0 ER1 HR1 AR0 BL1 `1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB` 8226493 Shift Recursive Weighted Automata
BR1 HR1 CR0 CR1 DR1 BR1 EL1 DL1 AR0 EL0 `1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE` 320969 Shift Recursive Weighted Automata
BR1 ER0 CR0 AR0 DL1 HR1 AL1 BL0 AR1 CL0 `1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC` 5377178 3N (“Helix”) Weighted Automata
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AR1 HR1 `1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA` 10818491 Shift Recursive Weighted Automata

This holdout, Skelet 20, is both an extreme bouncer and an extreme CPS-solvable TM.

``````dir=L,
n0=55144,
n1=41010,
split=[(80, 80), (6, 10), (75, 70)],
shifts=[(0, 144), (2, 20), (1, 34), (1, 28), (5, 392), (1, 196), (3, 34), (13, 816), (2, 144), (2, 22), (5, 392), (2, 196), (9, 102), (13, 816), (0, 144), (0, 16), (5, 392), (1, 196), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (1, 196), (5, 392), (2, 196), (12, 102), (13, 816), (0, 144), (0, 20), (5, 392), (1, 196), (1, 34), (2, 28), (3, 34), (13, 816), (2, 144), (0, 22), (5, 392), (2, 196), (5, 392), (1, 196), (9, 102), (13, 816), (0, 144), (0, 16), (5, 392), (0, 196), (5, 392), (1, 196), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (3, 196), (12, 102), (13, 816), (0, 144), (0, 20), (5, 392), (2, 196), (1, 34), (0, 28), (5, 392), (1, 196), (3, 34), (13, 816), (2, 144), (0, 22), (5, 392), (2, 196), (9, 102), (13, 816), (0, 144), (0, 16), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (1, 196), (12, 102), (13, 816), (0, 144), (2, 20), (1, 34), (1, 28), (3, 34), (13, 816), (2, 144), (0, 22), (9, 102), (13, 816), (0, 144), (0, 16), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (2, 196), (12, 102), (13, 816)]
``````
Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 `1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE` 347505 Regular (Sk. 20) Bouncers

This subset is solved by CPS, with the given left/center/right segment sizes. (More info here.) I re-list Sk. 20.

Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 DL0 CR1 BL0 DR0 HR1 ER1 BL0 AL1 AR0 `1RB0LD_1RC0LB_0RD---_1RE0LB_1LA0RA` 7174254 Regular CPS3(12-12-11)
BR1 BL0 CL1 ER0 DL1 CR0 EL0 HR1 AL1 AL0 `1RB0LB_1LC0RE_1LD0RC_0LE---_1LA0LA` 6244297 Regular CPS3(12-12-11)
BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 `1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE` 347505 Regular (Sk. 20) CPS3(8-24-7)
BR1 DL0 CR1 BL0 DR0 HR1 ER1 ER0 AL1 AR0 `1RB0LD_1RC0LB_0RD---_1RE0RE_1LA0RA` 7174252 Regular CPS3(12-12-11)
BR1 AL0 CR0 HR1 DR1 DR0 EL1 ER0 AR1 CL0 `1RB0LA_0RC---_1RD0RD_1LE0RE_1RA0LC` 5877285 Regular CPS3(12-12-11)

The rest are solved by FAR. In this table I give minimal left/right DFA sizes.
Where I show ‘??’ on the right, only FAR-direct realistically gets it (using an NFA on the right). A DFA size in the 80s is possible…

Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 DL1 `1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD` 3841643 Regular FAR: 3x4
BR1 CL1 AL1 BR1 DL1 AL0 ER1 DR0 HR1 BR0 `1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB` 12554268 Regular (Sk. 9) FAR: 13x16
BR0 EL0 CL1 BR1 BR1 DL1 HR1 AL0 AR0 EL1 `1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE` 11218583 Regular FAR: 4x4
BR1 HR1 CR0 BR0 CL1 DL0 AR1 EL0 AL0 EL0 `1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE` 14536286 Regular (Sk. 19) FAR: 11x11
BR0 CL0 CR1 BR1 DL1 EL0 HR1 EL1 AR1 AL1 `1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB` 8176549 Regular FAR: 10x??
BR1 BL1 CR0 DL0 DR1 CR1 EL1 AL0 HR1 AL1 `1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA` 11414657 Regular FAR: 10x??
BR1 AL1 CR1 DR1 AL0 ER0 HR1 CR0 CL0 ER1 `1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE` 11143983 Regular FAR: 4x4
BR1 AR1 CL1 CL0 EL0 DR0 AR0 BL1 DL1 HR1 `1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD---` 60658955 Regular (Sk. 24) FAR: 11x11
BR0 AR0 CL1 HR1 DL0 CL0 ER0 BR1 ER1 AR1 `1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE` 35346 Regular FAR: 4x3
BR1 DR0 CR1 HR1 DL1 EL1 ER1 DL1 AR1 CL0 `1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC` 5057577 Regular FAR: 11x9
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 `1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA` 3841642 Regular FAR: 3x4
BR0 CL0 CR1 HR1 DL0 ER1 EL1 DL1 AR1 AR0 `1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB` 20569060 Regular (Sk. 16) FAR: 12x11
BR1 BR0 CR0 DL0 DR1 HR1 EL0 AR1 AL1 EL1 `1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE` 35771936 Regular (Sk. 38) FAR: 11x11
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 CR1 `1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC` 36287 Regular FAR: 4x4
BR1 CR1 CL1 BR1 DL1 AR0 EL1 BL0 AL1 HR1 `1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA---` 9393627 Regular FAR: 9x11
BR1 DL1 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 `1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA` 13357563 Regular FAR: 3x4
BR1 AL1 CR1 EL0 DR1 AR0 ER1 HR1 AL1 BL1 `1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB` 11128264 Regular FAR: 11x9
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 EL0 `1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE` 36285 Regular FAR: 4x4
BR1 EL0 CR1 HR1 DR0 CR0 DL1 AL0 BL0 EL0 `1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE` 57874080 Regular (Sk. 42) FAR: 10x11
BR1 AR0 CL1 HR1 CL0 DL0 ER1 BR0 ER0 AR1 `1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA` 3841616 Regular (Sk. 40) FAR: 4x4
BR1 HR1 CL1 DL1 DR1 CL1 ER1 BL0 AR1 CR0 `1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC` 3656280 Regular FAR: 11x9
BR1 HR1 CR0 BR0 DL0 EL1 DL1 CR1 AL1 EL0 `1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE` 36299 Regular FAR: 4x4
BR1 DL0 CR1 ER0 DR1 HR1 EL1 AL1 AR1 EL1 `1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE` 7161825 Regular FAR: 11x9

Here are the DFA tables for those:

``````1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB [[0, 1], [2, 3], [4, 5], [4, 6], [4, 4], [4, 7], [4, 8], [4, 9], [4, 10], [4, 11], [4, 3], [4, 12], [4, 7]], [[0, 1], [2, 3], [4, 5], [6, 7], [4, 4], [0, 1], [4, 8], [9, 5], [10, 11], [4, 12], [4, 13], [4, 14], [3, 15], [6, 2], [3, 6], [4, 8]]
1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE [[0, 1], [2, 3], [2, 2], [0, 1]], [[0, 1], [2, 3], [2, 2], [0, 1]]
1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE [[0, 1], [2, 3], [4, 4], [5, 6], [4, 4], [7, 4], [8, 4], [9, 10], [4, 4], [5, 6], [4, 3]], [[0, 1], [2, 1], [3, 4], [5, 6], [6, 7], [6, 6], [6, 6], [8, 9], [10, 6], [10, 4], [3, 4]]
1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB [[0, 1], [2, 3], [4, 5], [6, 0], [4, 4], [4, 7], [4, 8], [4, 2], [4, 9], [4, 6]], ??
1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA [[0, 1], [2, 3], [4, 5], [6, 0], [4, 4], [4, 7], [4, 8], [4, 2], [4, 9], [4, 6]], ??
1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE [[0, 1], [2, 3], [2, 2], [0, 1]], [[0, 1], [2, 3], [2, 2], [2, 1]]
1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD--- [[0, 1], [2, 3], [4, 5], [5, 5], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]], [[0, 1], [2, 1], [3, 4], [5, 6], [5, 7], [5, 5], [5, 7], [8, 9], [3, 5], [10, 6], [5, 4]]
1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [2, 0], [2, 2]]
1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC [[0, 1], [2, 3], [4, 5], [2, 3], [6, 7], [8, 8], [9, 6], [9, 6], [4, 10], [9, 9], [8, 8]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB [[0, 1], [2, 3], [4, 5], [2, 3], [6, 7], [6, 8], [6, 6], [6, 8], [9, 10], [4, 6], [11, 7], [6, 5]], [[0, 1], [2, 3], [4, 5], [5, 5], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]]
1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE [[0, 1], [2, 1], [3, 4], [5, 6], [5, 7], [5, 5], [5, 7], [8, 9], [3, 5], [10, 6], [5, 4]], [[0, 1], [2, 3], [4, 5], [5, 6], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]]
1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA--- [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]], [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]]
1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE [[0, 1], [2, 3], [4, 4], [5, 6], [4, 4], [7, 4], [2, 4], [8, 9], [5, 6], [4, 3]], [[0, 1], [2, 1], [3, 4], [5, 6], [6, 7], [6, 6], [6, 6], [8, 9], [10, 6], [10, 4], [3, 4]]
1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA [[0, 1], [2, 3], [1, 0], [3, 3]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC [[0, 1], [2, 3], [4, 5], [2, 3], [6, 4], [6, 7], [6, 6], [8, 9], [6, 10], [7, 7], [6, 4]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
``````
2 Likes