popsat TS, ktery prijima jazyk \{ 1^{2^x}, x \geq 0\}
odvodit ze x-1 je PRF
pokud mam blackbox ktery resi rozhodovaci SAT (ANO/NE) jak pomoci nej sestrojim algoritmus ktery najde dane ohodnoceni promennych
dokaz ze celociselne programovani je NP-uplne