Pri dôkaze oboch inklúzií vychádzame z definície nového dvojsmerného automatu. Ukážeme, že ekvivalentne existujú akceptačné výpočty v oboch automatoch.

L’ Í L(A’)

V tomto smere sa snažíme dokázať, že ak existuje akceptačný výpočet v automate A (čo nám zaručuje to, že ten jazyk je regulárny) potom dá sa nájsť akceptačný výpočet aj v našom automate A´.

" z=uv $ acc. s automatom A pre nejaké wÎ S*.

(q0,uvw) |--|uv| (qa,w) |-- (q1,w2w3...wk) |-- (q2,w3...wk) |-- … |--(qk,e ) & qk Î F

poďla def. $ acc. s automatom A’

(q0,¢#uv$) |--|uv| (qa,¢uv#$) |-- (qa’,¢uv1v2…#vk$) |-- (qaL’,¢uv1v2…#vk-1vk$) |-- (q1’, ¢uv1v2…#vk-2vk-1vk$) |-- (q1L’,¢uv1v2…#vk-3vk-2vk-1vk$) |--
(q2’, ¢uv1v2…#vk-4vk-3vk-2vk-1vk$) |-- (q2L’,¢uv1v2…#vk-5vk-4vk-3vk-2vk-1vk$) |-- … |--
(qk-1’,¢u1#u2u3…v$) |-- (qk-1L’,¢#u1u2u3…v$) |-- (qk,#¢uv$) |--|uv| (qk,¢uv#$)

Rozpoznávanie slova z určuje akúsi postupnosť stavov, cez ktorých automat A prechádza. Navyše podľa dĺžky vstupného slova môžeme presne určiť hranicu slov v a w. Automat A v tomto stave je po |uv| krokoch. Z konštrukcie automatu A´ priamo vyplýva, že túto fázu rozpoznávania urobí identicky ako automat A. V tom okamihu má na vstupe $, a teda prejde do fázy q s čiarou, a nedeterministicky uhádne takú postupnosť stavov, aby sa mohol skončit v akceptačnom po zpätnom preberaní vstupu. Túto postupnosť stavov si určíme podľa tej postupnosti, čo vytvoril automat A pri preskúmaní podslova w. Opäť podľa definície, ak sme na začiatku slova a v akceptačnom stave, mechanicky prejdeme na koniec vstupu bez ohľadu na to, čo vidí čitacia hlava. A preto existuje akceptačný výpočet aj v A´, teda slovo z patrí do L(A´).

 

L’ Ę L(A’)

V tomto smere máme za predpoklad, že náš automat A´ akceptuje dané slovo, a máme dokázať, že to slovo patrí do jazyka L´. Na to, aby to platilo, musíme nájsť akceptačný výpočet v automate A a súčasne musí platiť rovnosť o dĺžke tých podslov.
Akceptačný výpočet si nájdeme identicky, takisto ako pri predchádzajúcej inklúzií dôkaz sa vo veľkej miere opiera definíciu nášho automatu, ale teraz využijeme opačný smer ekvivalencie. Pri rozpoznávaní prefixu uv nemáme žiadny problém, lebo (ako už bolo povedané) prvá fáza rozpoznávacieho procesu v A´ je identická s rozpoznávaním v starom automate. Otázka postfixu je vyriešená s tým, že zoberieme si postupnosť stavov fázy dva, vynecháme pomocné stavy (stavy s L-kom). A teraz na vstup pôvodného automatu dávame také symboly, aby počas rozpoznávania vytvorili tú istú postupnosť ekvivalentných stavov. Takým postupom aj pôvodný automat sa dostane do akceptačného stavu.

z=uv $ acc. s automatom A’ pre nejaké wÎ S*.
a) (q0,¢#uv$) |--|uv| (qa,¢uv#$)
viď: D(qa,x) = {(qb,1)} Ű d(qa) = qb & xÎ S'
b) (qa,¢uv#$) |--|uv| (qFINAL,#¢uv$)
viď: D(qaL',x) = {(qb',-1)} Ű d(qa,y) = qb "yÎ S' & xÎ S'
c) (qFINAL, ¢#uv$) |--|uv| (qFINAL,¢uv#$)

Otázka dĺžky slov: predstavme si, že náš automat dostane na vstup slovo nepárnej dĺžky. Potom by sa ale vyskytli problémy pri spätnej ceste. Čitacia hlava by sa dostala na cent v tzv. pomocnom stave (v stave s L-kom). Pre taký prípad ale delta-funkcia nie je kondiciovaná, tj. to by nebol akceptačný výpočet.