{{Template:TIN064 Skripta}}
{{TODO|tohle je jen opravdu hruby nastrel}}
*ČRF => TS (každá ČRF je turingovsky vyčíslitelná)
důkaz indukcí podle konstrukce ČRF
základní fce jsou tur.vyčíslitelné
substituce (vyčíslím podfce g - m-pásek, a dám to dohromady)
primitivní rekurze, minimalizace (asi easy!?)
*TS => ČRF
jeden krok TS je PR-záležitost
TS pracuje dokud neskončí (while cyklus)
TS pracuje s konfiguracemi + okraje (zarážky) - to jsou tzv. Postova slova UqsV (kóduji je do přirozených čísel)
fce step(kód(K_i)) = kód(K_i+1) je PRF (K_i je konfigurace)
comp(x,s) = kód výsledku po s krocích práce - for-cyklus => comp(x,s) je PRF
\ný_s(comp(x,s) & za s kroků skončím) - while cyklus (operátor minimalizace)
