====== JFiZO - Zadanie 09.125 ======
Definiujemy sobie język L, budując algorytm A, który go rozstrzyga

<code>
wczytaj x;
wczytaj maszynę $M_x$ odpowiadającą x //umawiamy się, że każda maszyna ma nieskończenie wiele poprawnych reprezentacji
utwórz wielomian $p(y)=y^{log(x)} + log(x)$
Zapuść maszynę $M_x(x)$.  Jeśli maszyna się zatrzyma, zużywając co najwyżej $p(|x|)$ pamięci i zaakceptuje, to słowo
$x \not \in L$. W przeciwnym wypadku $x \in L$
</code>
Język L jest rekurencyjny, bo algorytm A zawsze się zatrzyma.
Ten algorytm działa w EXPSPACE, gdyż dla dowolnego x da się ograniczyć $p(|x|)$ przez $O(2^n)$

Załóżmy nie wprost, że istnieje maszyna $M_L$, która rozstrzyga L, zużywając pamięć ograniczoną przez wielomian q.
Znajdźmy $m$ takie, że wielomian $p(y) = y^{log(m)}+log(m)$ jest zawsze większy od $q(y)$. 
Weźmy takie $m_1 \ge m$, że $M_{m1} = M_L$. 

Teraz zapuśćmy $A(m_1)$. Jak się ten program wykona?
Wczytamy $m_1$ jako liczbę. Wczytamy maszynę $M_L$. I stworzymy wielomian p, o którym wiemy, że jest stale większy od q.
Skoro $p(m_1)>q(|m_1|)$, to symulacja maszyny $M_L$ będzie przebiegać aż do jej zakończenia. I co teraz?

$m_1 \in L \iff M_L(m_1)$ powie "tak" ${} \iff A(m_1)$ powie "nie" ${} \iff m_1 \not \in L$

TODO **Poszło zdecydowanie zbyt gładko, będę wdzięczny za szukanie ewentualnych bugów**