BB5's "finned" machines (summary)

This post summarizes a family of 5 decider holdouts (proved infinite by hand).
They are:

Years ago, Skelet noticed them and wrote: " N_2N and 3N machines are 3-linear sequences, but with little complex behavior than the machines, proved by methods TryL1Cnt and TryModFin. They are easy provable by hand." (“N_2N” corresponds to these five; “3N” corresponds to a holdout family I’ve called “helix”.)

I called them “finned” cubic machines when I noticed them as CTL holdouts.
They are provably CTL holdouts, as illustrated by @Iijil: 10756090 is irregular.
Analysis has shown they’ll likely remain holdouts for any Weighted Finite Automata decider (using a single integer weight): a closed language of configs can be described in this way (and the linked proofs effectively do that), but the transitions do not vary the weights smoothly.
However, @mxdys has reported being able to extend a Repeated-Word List CTL decider in a way that allows linear equalities between repeater counts, and it was effective at solving these machines.
@meithecatte has also at least started to explore automatic deciders that could cover this class
Therefore, these machines may soon lose their status as special cases.

1 Like