This is neat. I wonder whether there is a faster approach using binary decision diagrams or a variant thereof. If the state transition were represented by a binary function, BDDs could allow for counting states without actually enumerating. The question would be, how to actually find all the fixed points of that function.
Neat. Seems a lot harder than the work I did to enumerate towers of Hanoi back in 2004:<p><a href="https://www.cs.carleton.ca/sites/default/files/tr/TR-04-10.pdf" rel="nofollow">https://www.cs.carleton.ca/sites/default/files/tr/TR-04-10.p...</a>