Turing machine simulator

This machine halts if and only if Erdős' conjecture on powers of two is false:

"For all n > 8, there is at least one 2 in the ternary representation of 2^n"

P. Erdős. Some unconventional problems in number theory. Mathematics Magazine, 52(2):67–70, 1979.

The machine has 5 states and 4 symbols
States mul2_F and mul2_G run the FST that computes 2x in base 3 (reverse-ternary).
The other states are responsible for checking the conjecture and keeping track of the 3 known special cases:
1, 4 and 256 which are resepectively 1, 11 and 100111 in base 3.

This machine was proven correct:

Setup

Machine

or 

Turing Machine format described here.

or

Initial configuration

Initial tape content

(put a > in front of initial tape position or leave empty if blank input)

Initial state

Simulation

Tape (blank symbol: #)

Click and drag tape with mouse

Step: 0

States (5)

  mul2_F
> mul2_G
  find_2
  rewind
  check_halt