With the CTL-deciders proving to be very strong there is the question which machines cannot be proven by it. 10756090 is an example of such a machine. We can proof that there is no regular language that includes all configuration the TM reaches, but rejects all configurations that lead to halting:

Write C(n,m) for `(10)^n A0 1^m`

Then the TM follows these rules:

- C(n,m) → halt, if n+m odd
- C(n,m) → C(((n+m)/2)+1,n+1), if n+m even

I’ll leave the proof as an exercise for the reader.

We start in C(0,0) and C(n,n) → C(n+1,n+1) for all n, so the machine is infinite and visits C(n,n) for all n.

To see how it behaves with n != m we consider the difference n-m after applying rule 2:

((n+m)/2)+1-(n+1) = (n+m-2n)/2 = -(n-m)/2

So the TM divides the difference of the exponents by 2 (and flips the sign) until the difference becomes odd. Then it halts. This can only go on forever if the difference is 0 to begin with.

Thus C(n,m) → halt, if n!=m

It is impossible for a regular language to separate {C(n,n) for all n} and {C(n,m) for all n!=m}

To finish it off with an argument by savask:

“If there was a regular language containing all non-halting configs of your machine, then we could intersect it with a language `(10)* A0 1*`

and obtain that `(10)^n A0 1^n`

is regular”