Prirodzenym cislom kodujeme konfiguraciu turingovho stroja <Q, S, N>,
kde Q je aktualny stav, S je najmensia suvisla cast pasky obsahujuca
vsetky neprazdne symboly a N je pozicia citacej hlavy. Pre jednoduchost
nech paska je nekonecna iba do jedneho smeru. Budeme pracovat v binarnej
sustave, znaky na paske nech su iba 0 a 1 alebo X (prazdny znak).

Pasku zakodujeme ako dvojicu, kde prvy prvok bude pocet nastavenych
znakov a druhy binarne cislo vyjadrujuce stav pasky. Existuje v
aritmetike definovatelna funkcia get_bit(S,n) ktora z pasky S vrati
n-ty znak alebo X ak este nebol nastaveny a set_bit(S,n,b) ktora n-ty
bit nastavi na b.

Prechodova funkcia je konecna, a teda je tiez jednoducho definovatelna,
nech to bude teda
  d(Q,Z,0) vrati novy stav zo stavy Q a znaku Z, alebo 0 ak sme sa dostali do koncoveho stavu,
  d(Q,Z,1) vrati znak ktory sa ma napisat na pasku,
  d(Q,Z,_) vrati 0 alebo 1, podla toho ci sa mame posunut dolava alebo doprava.

Potom vieme definovat funkciu
prechod(O) = N, kde O je stara konfiguracia a N je nova konfiguracia:
prechod(<q,s,n>) = <Q,S,N>  ↔  ( z = get_bit(s, n) ∧
                                 d(q, z, 0) = Q ∧
                                 S = set_bit(s, n, d(q, z, 1)) ∧
                                 ( d(q, z, 2) = 1 → N = n+1 ) ∧
                                 ( d(q, z, 2) != 1 → ( (n = N+1) ∨ (N = 0) ) )
                               )

Ked uz mame definovanu tuto funkciu, mozme vyjadrit konfiguraciu po n krokoch:
( prechod_n_krokmi(K, 0) = K ∧
  prechod_n_krokmi(K, x+1) = prechod_n_krokmi(prechod(K), x)
)

A nakoniec vieme vyjadrit ze turingov stroj sa zastavi:

(∃x) (prechod_n_krokmi(pociatocna_konfiguracia, x) = <0,_,_>)

Ak by sme teda vedeli dokazat alebo vyvratit tuto formulu, vedeli by sme vyriesit halting problem.