\documentclass[a4paper,polish]{article}
\usepackage{amsmath,amsthm,amsfonts}
\usepackage[T1]{fontenc}
\usepackage[latin2]{inputenc}
\usepackage{babel}

\numberwithin{equation}{section}

\newtheorem{thm}{Twierdzenie}
\newtheorem{lem}{Lemat}
\newtheorem{concl}{Wniosek}

\theoremstyle{definition}
\newtheorem{defn}{Definicja}

\newcommand{\N}{\mathbb{N}}
\newcommand{\relref}[2]{\overset{\eqref{#1}}{#2}}
\newcommand{\relrefand}[3]{\overset{\eqref{#1}\text{ i }\eqref{#2}}{#3}}

\markright{Dowód, że funkcja Ackermana nie jest pierwotnie rekurencyjna}
\pagestyle{myheadings}

\begin{document}
  \title{Dowód, że funkcja Ackermana nie jest pierwotnie rekurencyjna}
  \author{Jakub Pawlewicz}
  \date{26 marzec 2001}
  \maketitle
  


  W całym dokumencie dziedziną zmiennych są liczby naturalne ($\N)$, a
  wszystkie funkcje są postaci $\N^k \rightarrow \N$.
  
  Wszędzie, gdzie będzie podana jakaś tożsamość zależna od zmiennej wolnej
  np. $x$, to zakłada się, że tożsamość ta spełniona jest dla wszystkich
  $x\in\N$, chyba, że ponadto podane zostaną ograniczenia na tą zmienną, np.
  $x\geq 1$, wtedy oznacza to, że tożsamość jest spełniona dla wszystkich
  $x\in\N$ i $x\geq 1$.



  \section{Funkcja Ackermana}
  \begin{defn}
    Funkcja Ackermana $A : \N^3 \rightarrow \N$, określona jest równaniami
    rekurencyjnymi:
    \begin{align}
      A(0,0,x)     &= x			\tag{A1}\label{eq:ack00x} \\
      A(0,y+1,x)   &= A(0,y,x)+1	\tag{A2}\label{eq:ack0yx} \\
      A(1,0,x)     &= 0			\tag{A3}\label{eq:ack10x} \\
      A(z+2,0,x)   &= 1			\tag{A4}\label{eq:ackz0x} \\
      A(z+1,y+1,x) &= A(z,A(z+1,y,x),x)	\tag{A5}\label{eq:ackzyx}
    \end{align}
  \end{defn}
  
  \begin{thm}[Własności funkcji Akcermana]
    Zachodzi:
    \begin{align}
      A(0,y,x) &= x+y	\label{eq:ack_z0} \\
      A(1,y,x) &= xy	\label{eq:ack_z1} \\
      A(2,y,x) &= x^y	\label{eq:ack_z2} \\
      A(z+2,1,x) &= x	\label{eq:ack_y1}
    \end{align}
  \end{thm}
  
  \begin{proof}
    Własności \eqref{eq:ack_z0}, \eqref{eq:ack_z1}, \eqref{eq:ack_z2}
    dowodzimy indukcją po $y$, a własność \eqref{eq:ack_y1} indukcją po $z$.
    \begin{itemize}
      \item \eqref{eq:ack_z0}. $y=0$ to własność \eqref{eq:ack00x}.
        $A(0,y+1,x) \relref{eq:ack0yx}{=} A(0,y,x)+1 = x+y+1$.
      \item \eqref{eq:ack_z1}. $y=0$ to własność \eqref{eq:ack10x}.
        $A(1,y+1,x) \relref{eq:ackzyx}{=} A(0,A(1,y,x),x) = A(0,xy,x)
        \relref{eq:ack_z0}{=} x(y+1)$.
      \item \eqref{eq:ack_z2}. $y=0$ to własność \eqref{eq:ackz0x}.
        $A(2,y+1,x) \relref{eq:ackzyx}{=} A(1,A(2,y,x),x) = A(1,x^y,x)
        \relref{eq:ack_z1}{=} x^{y+1}$.
      \item \eqref{eq:ack_y1}. Dla $z=0$ wynika to z \eqref{eq:ack_z2}.
        $A(z+3,1,x) \relref{eq:ackzyx}{=} A(z+2,A(z+3,0,x),x)
	\relref{eq:ackz0x}{=} A(z+2,1,x) = x$.
    \end{itemize}
  \end{proof}



  \section{Parę nierówności}
  \begin{lem}
    \begin{equation}
      2x\geq x+1\qquad\text{dla }x\geq 1.\label{eq:2x_geq_x1}
    \end{equation}
  \end{lem}
  
  \begin{lem}
    \begin{equation}
      x^y\geq xy \qquad \text{dla } x\geq 2.\label{eq:xtoy_geq_xy}
    \end{equation}
  \end{lem}
  \begin{proof}
    Indukcja po $y$. Dla $y=0$, prawa strona \eqref{eq:xtoy_geq_xy} wynosi 0.
    Dla $y=1$ \eqref{eq:xtoy_geq_xy} ma postać $x\geq x$. Niech $y\geq 1$.
    Wtedy $x^{y+1}=x^yx\geq (xy)x\geq (2y)x
    \relref{eq:2x_geq_x1}{\geq} x(y+1)$.
  \end{proof}

  \begin{concl}
    \begin{equation}
      x^y\geq y+1 \qquad \text{dla } x\geq 2.\label{eq:xtoy_geq_y1}
    \end{equation}
  \end{concl}
  \begin{proof}
    Dla $y=0$ \eqref{eq:xtoy_geq_y1} to $1\geq1$. Dla $y\geq 1$ mamy
    $x^y\relref{eq:xtoy_geq_xy}{\geq}xy\geq 2y
    \relref{eq:2x_geq_x1}{\geq}y+1$.
  \end{proof}
  
  \begin{concl}
    \begin{equation}
      2^x>x.\label{eq:2tox_gt_x}
    \end{equation}
  \end{concl}
  \begin{proof}
    Dla $x=0$ i $x=1$ jest to oczywiste. Niech $x\geq 2$.
    Mamy $2^x\relref{eq:xtoy_geq_y1}{\geq}x+1>x$.
  \end{proof}

  \begin{lem}
    \begin{equation}
      x^y\geq x(y+1) \qquad \text{dla } x\geq 2\text{ i }y\geq 3.
      \label{eq:xtoy_geq_xy1}
    \end{equation}
  \end{lem}
  \begin{proof}
    Indukcja po $y$. Dla $y=3$ mamy $x^y=x^3=(x^2)x\geq 4x=x(y+1)$.
    Następnie $x^{y+1}=x^yx\geq x(y+1)x\geq 2(y+1)x
    \relref{eq:2x_geq_x1}{\geq}x(y+2)$.
  \end{proof}
  
  \begin{concl}
    \begin{equation}
      x^y\geq y+2 \qquad \text{dla } x\geq 2\text{ i }y\geq 2.
      \label{eq:xtoy_geq_y2}
    \end{equation}
  \end{concl}
  \begin{proof}
    Dla $y=2$ mamy $x^2\geq 4=y+2$. Niech $y\geq 3$. Wtedy
    $x^y\relref{eq:xtoy_geq_xy1}{\geq}x(y+1)\geq 2(y+1)
    \relref{eq:2x_geq_x1}{\geq}y+2$.
  \end{proof}
  
  \begin{concl}
    \begin{equation}
      2^x>x+1 \qquad \text{dla } x\geq 2.\label{eq:2tox_gt_x1}
    \end{equation}
  \end{concl}
  \begin{proof}
    $2^x\relref{eq:xtoy_geq_y2}{\geq}x+2>x+1$.
  \end{proof}
  
  \begin{lem}
    \begin{equation}
      x^y\geq2xy\qquad\text{dla }y\geq 4,x\geq 2.
      \label{eq:xtoy_geq_2xy}
    \end{equation}
  \end{lem}
  \begin{proof}
    Indukcja po $y$. Dla $y=4$ mamy $x^4=(x^3)x\geq 8x=2yx$. Następnie
    $x^{y+1}=x^yx\geq 2xyx\geq 2x(2y)\relref{eq:2x_geq_x1}{\geq}2x(y+1)$.
  \end{proof}
  
  \begin{concl}
    \begin{equation}
      x^y\geq 2y+2\qquad\text{dla }y\geq 3,x\geq 2.
      \label{eq:xtoy_geq_2y2}
    \end{equation}
  \end{concl}
  \begin{proof}
    Dla $y=3$ mamy $x^3=8=2y+2$. Niech $y\geq 4$. Wtedy
    $x^y\relref{eq:xtoy_geq_2xy}{\geq}
    2xy\geq 4y=2(2y)\relref{eq:2x_geq_x1}{\geq}2(y+1)$.
  \end{proof}



  \section{Nierówności dla funkcji Ackermana}
  \begin{thm}
    Funkcja Ackermana jest niemalejąca po $y$, dla $x\geq 1$.
    \begin{equation}
      A(z,y',x)\geq A(z,y,x) \text{ dla wszystkich } y'\geq y.
      \label{eq:ack_yup}
    \end{equation}
  \end{thm}
  \begin{proof}
    Wystarczy udowodnić, że
    \begin{equation}
      A(z,y+1,x)\geq A(z,y,x).\label{eq:ack_y1up}
    \end{equation}
    Indukcja po $z$.
    \begin{enumerate}
      \item Dla $z=0$ \eqref{eq:ack_y1up} na mocy
        \eqref{eq:ack_z0} sprowadza się do $x+y+1\geq x+y$.
	Dla $z=1$ \eqref{eq:ack_y1up} na mocy
        \eqref{eq:ack_z1} sprowadza się do $x(y+1)\geq xy$.
      \item Zakładamy, że $z\geq 2$ oraz, że $A(z-1,y+1,x)\geq A(z-1,y,x)$,
	czyli w ogólności
        \begin{equation}
          A(z-1,y',x)\geq A(z-1,y,x)\text{ dla wszystkich } y'\geq y.
	  \label{eq:ack_yup:ind_z}
	\end{equation}
	Teraz stosujemy indukcje po $y$.
	\begin{enumerate}
	  \item $y=0$. Wtedy $A(z,1,x)\relref{eq:ack_y1}{=}x\geq 1
	    \relref{eq:ackz0x}{=}A(z,0,x)$.
	  \item $y\geq 1$ oraz $A(z,y,x)\geq A(z,y-1,x)$. Wtedy 
	    $A(z,y+1,x)\relref{eq:ackzyx}=A(z-1,A(z,y,x),x)
	    \relref{eq:ack_yup:ind_z}{\geq}A(z-1,A(z,y-1,x),x)
	    \relref{eq:ackzyx}{=}A(z,y,x).$
	\end{enumerate}
    \end{enumerate}
  \end{proof}

  \begin{lem}
    \begin{equation}
      A(z,y,x)\geq y+1\qquad\text{dla }z\geq 2,x\geq 2.
      \label{eq:ack_geq_y1}
    \end{equation}
  \end{lem}
  \begin{proof}
    Indukcja po $z$.
    \begin{enumerate}
      \item $z=2$. Wtedy $A(2,y,x)\relref{eq:ack_z2}{=}x^y
        \relref{eq:xtoy_geq_y1}{\geq}y+1$.
      \item Zakładamy, że
        \begin{equation}
	  A(z-1,y,x)\geq y+1\text{ oraz }z\geq 3.
	  \label{eq:ack_geq_y1:ind_z}
        \end{equation}
	Teraz stosujemy indukcje po $y$.
	\begin{enumerate}
	  \item $y=0$. Wtedy $A(z,0,x)\relref{eq:ackz0x}{=}1=y+1$.
	  \item Niech $y\geq 1$ i $A(z,y-1,x)\geq y$. Mamy $A(z,y,x)
	    \relref{eq:ackzyx}{=}A(z-1,A(z,y-1,x),x)\relref{eq:ack_yup}{\geq}
	    A(z-1,y,x)\relref{eq:ack_geq_y1:ind_z}{\geq}y+1$.
	\end{enumerate}
    \end{enumerate}
  \end{proof}
  
  \begin{thm}
    Funkcja Ackermana jest niemalejąca po $z$, dla $x\geq 2$ i $z\geq 1$.
    \begin{equation}
      A(z',y,x)\geq A(z,y,x) \text{ dla wszystkich } z'\geq z.
      \label{eq:ack_zup}
    \end{equation}
  \end{thm}
  \begin{proof}
    Wystarczy udowodnić, że $A(z+1,y,x)\geq A(z,y,x)$.
    
    Dla $z=1$ mamy $A(2,y,x)\relref{eq:ack_z2}{=}x^y
    \relref{eq:xtoy_geq_xy}{\geq}xy\relref{eq:ack_z1}{=}A(1,y,x)$.
    Niech $z\geq2$.
    Dla $y=0$ mamy $A(z+1,0,x)\relref{eq:ackz0x}{=}1
    \relref{eq:ackz0x}{=}A(z,0,x)$.
    Niech $y\geq 1$.
    Mamy $A(z+1,y,x)\relref{eq:ackzyx}{=}A(z,A(z+1,y-1,x),x)$.
    Z \eqref{eq:ack_geq_y1} mamy $A(z+1,y-1,x)\geq y$, więc
    $A(z,A(z+1,y-1,x),x)\relref{eq:ack_yup}{\geq}A(z,y,x)$.
  \end{proof}
  
  \begin{lem}
    \begin{equation}
      A(z,y,x)\geq y+2\qquad\text{dla }z\geq 2, y\geq 2, x\geq 2.
      \label{eq:ack_geq_y2}
    \end{equation}
  \end{lem}
  \begin{proof}
    Indukcja po $z$.
    \begin{enumerate}
      \item $z=2$. Wtedy $A(2,y,x)\relref{eq:ack_z2}{=}x^y
        \relref{eq:xtoy_geq_y2}{\geq}y+2$.
      \item Zakładamy, że 
        \begin{equation}
          A(z-1,y,x)\geq y+2\text{ oraz }z\geq 3.
	  \label{eq:ack_geq_y2:ind_z}
	\end{equation}
        Wtedy mamy
        $A(z,y,x)\relref{eq:ackzyx}{=}A(z-1,A(z,y-1,x),x)$. Z
	\eqref{eq:ack_geq_y1} mamy $A(z,y-1,x)\geq y$, skąd
	$A(z-1,A(z,y-1,x),x)\relref{eq:ack_yup}{\geq}A(z-1,y,x)
	\relref{eq:ack_geq_y2:ind_z}{\geq}y+2$.
    \end{enumerate}
  \end{proof}

  \begin{thm}
    Funkcja Ackermana szybciej rośnie po $z$ niż po $y$.
    \begin{equation}
      A(z+1,y,x)\geq A(z,y+1,x)\qquad\text{dla }z\geq 1,y\geq 3,x\geq 2.
      \label{eq:ack_zdown_yup}
    \end{equation}
  \end{thm}
  \begin{proof}
    Dla $z=1$ mamy $A(2,y,x)\relref{eq:ack_z2}{=}x^y
    \relref{eq:xtoy_geq_xy1}{\geq}x(y+1)\relref{eq:ack_z1}{=}A(1,y+1,x)$.
    Niech $z\geq 2$. Mamy $A(z+1,y,x)\relref{eq:ackzyx}{=}A(z,A(z+1,y-1,x),x)$.
    Z \eqref{eq:ack_geq_y2} mamy $A(z+1,y-1,x)\geq y+1$, skąd
    $A(z,A(z+1,y-1,x),x)\relref{eq:ack_yup}{\geq}A(z,y+1,x)$.
  \end{proof}

  \begin{concl}
    \begin{equation}
      A(z+n,y,x)\geq A(z,y+n,x)\qquad\text{dla }z\geq 1,y\geq 3,x\geq 2.
      \label{eq:ack_n_zdown_yup}
    \end{equation}
  \end{concl}

  \begin{concl}
    \begin{equation}
      A(z+n,y,x) > y+n\qquad\text{dla }z\geq 2,y\geq 3,x\geq 2.
      \label{eq:ack_znup_gt_yn}
    \end{equation}
  \end{concl}
  \begin{proof}
    $A(z+n,y,x)\relref{eq:ack_n_zdown_yup}{\geq}A(z,y+n,x)
    \relref{eq:ack_geq_y1}{\geq}y+n+1>y+n$.
  \end{proof}

  \begin{lem}
    \begin{equation}
      A(z,y,x)\geq 2y+2\qquad\text{dla }z\geq 2, y\geq 3, x\geq 2.
      \label{eq:ack_geq_2y2}
    \end{equation}
  \end{lem}
  \begin{proof}
    Indukcja po $z$.
    \begin{enumerate}
      \item $z=2$. Wtedy $A(2,y,x)\relref{eq:ack_z2}{=}x^y
        \relref{eq:xtoy_geq_2y2}{\geq}2y+2$.
      \item Zakładamy, że 
        \begin{equation}
          A(z-1,y,x)\geq 2y+2\text{ oraz }z\geq 3.
	  \label{eq:ack_geq_2y2:ind_z}
	\end{equation}
        Wtedy mamy
        $A(z,y,x)\relref{eq:ackzyx}{=}A(z-1,A(z,y-1,x),x)$. Z
	\eqref{eq:ack_geq_y1} mamy $A(z,y-1,x)\geq y$, skąd
	$A(z-1,A(z,y-1,x),x)\relref{eq:ack_yup}{\geq}A(z-1,y,x)
	\relref{eq:ack_geq_2y2:ind_z}{\geq}2y+2$.
    \end{enumerate}
  \end{proof}
  
  \begin{thm}
    Funkcja Ackermana szybciej rośnie po $z$ niż wykładniczo po $y$.
    \begin{equation}
      A(z+1,y,x)\geq A(z,2y,x)\qquad\text{dla }z\geq 1,y\geq 4,x\geq 2.
      \label{eq:ack_zdown_2y}
    \end{equation}
  \end{thm}
  \begin{proof}
    Dla $z=1$ mamy $A(2,y,z)\relref{eq:ack_z2}{=}x^y
    \relref{eq:xtoy_geq_2xy}{\geq}2xy\relref{eq:ack_z1}{=}A(1,2y,x)$.
    Niech $z\geq 2$. Mamy $A(z+1,y,x)\relref{eq:ackzyx}{=}A(z,A(z+1,y-1,x),x)$.
    Z \eqref{eq:ack_geq_2y2} $A(z+1,y-1,x)\geq 2(y-1)+2=2y$, skąd
    $A(z,A(z+1,y-1,x),x)\relref{eq:ack_yup}{\geq}A(z,2y,x)$.
  \end{proof}



  \section{Funkcje pierwotnie rekurencyjne}
  \begin{defn}
    Klasę funkcji {\em pierwotnie rekurencyjnych} określamy jako najmniej\-szy
    zbiór $PR$ funkcji $\N^k \rightarrow \N$ zawierający funkcje:
    \begin{align}
      f(x) &= x+1 \tag{PR1}\label{PRinc}\\
      f(x_1,\dots,x_n) &= 0
      \tag{PR2}\label{PRzero}\\
      f(x_1,\dots,x_n) &= x_i \qquad \text{gdzie } 1 \leq i \leq n
      \tag{PR3}\label{PRproj}\\
      \intertext{oraz zamknięty na operację złożenia:}
      \begin{split}
        f(x_1,\dots,x_n) &=
	h\bigl(g_1(x_1,\dots,x_n),\dots,g_k(x_1,\dots,x_n)\bigr) \\
        \text{gdzie }h,g_1,\dots,g_k \in PR \text{ i } &
	h:\N^k\rightarrow\N, g_1,\dots,g_k:\N^n\rightarrow\N
      \end{split}\tag{PR4}\label{PRconcat}
      \intertext{i operację pierwotnej rekursji:}
      \begin{split}
        f(0,x_1,\dots,x_k) &= g(x_1,\dots,x_k)\\
	f(n+1,x_1,\dots,x_k) &= h(n,f(n,x_1,\dots,x_k),x_1,\dots,x_k)\\
	\text{gdzie } g,h\in PR \text{ i } &
	g:\N^k \rightarrow \N, h:\N^{k+2}\rightarrow\N
      \end{split}\tag{PR5}\label{PRinduct}
    \end{align}
  \end{defn}

  \begin{lem}\label{PR_const_lem}
    Funkcja stała $f_N(x)=N$ jest pierwotnie rekurencyjna.
  \end{lem}
  \begin{proof}
    Indukcja po $N$. Dla $N=0$ to własność (PR2).
    Niech $g(x)=x+1$. $g\in PR$ z własności (PR1).
    Następnie definiujemy $f_{N+1}$ używając własności (PR4).
    $f_{N+1}=g(f_N(x))=g(N)=N+1$.
  \end{proof}
  
  \begin{defn}
    {\em Ciągiem definicji funkcji} pierwotnie rekurencyjnych nazywamy
    ciąg funkcji $f_1,\dots,f_n$ o własnościach:
    \begin{itemize}
      \item
        $f_1,\dots,f_{n-1}$ jest ciągiem definicji funkcji,
      \item
        definicja $f_n$ jest postaci (PR1)-(PR5),
      \item
        definicja $f_n$ zależy tylko od funkcji $f_1,\dots,f_{n-1}$, tzn.
	jeśli $f_n$ jest określona przez (PR4), to
	$h,g_1,\dots,g_k\in\{f_1,\dots,f_{n-1}\}$, jeśli jest określona
	przez (PR5), to $h,g\in\{f_1,\dots,f_{n-1}\}$.
    \end{itemize}
  \end{defn}
  
  \begin{defn}
    {\em Definicją funkcji $f$} nazywamy ciąg definicji funkcji
    $f_1,\dots,f_n$ taki, że $f_n = f$. {\em Długością definicji funkcji $f$}
    jest liczba funkcji w ciągu definicji funkcji, czyli tutaj $n$.
  \end{defn}
  


  \section{Dowód, że funkcja Ackermana nie jest pierwotnie rekurencyjna}
  \begin{lem}\label{ack_lem_const}
    Dla dowolnego $N$ istnieje stała $z_N\geq 2$ taka, że
    \begin{equation}
      N < A(z_N,y,2)\qquad\text{dla }y\geq 3.\label{eq:ack_lem_const}
    \end{equation}
  \end{lem}
  \begin{proof}
    Wystarczy przyjąć $z_N=2 + \max(N-3,0)$. Wtedy $A(z_N,y,2)
    \relref{eq:ack_yup}{\geq}A(z_N,3,2)=A(2+\max(N-3,0),3,2)
    \relref{eq:ack_znup_gt_yn}{>}\max(N-3,0)+3=\max(N,3)\geq N$.
  \end{proof}
  
  \begin{lem}\label{PR4_fup_lem}
    Niech $h:\N^k\rightarrow\N$ oraz $g_i:\N^n\rightarrow\N$ dla
    $1\leq i \leq k$. Niech $z_h,z_{g_1},\dots,z_{g_k}\geq 2$
    takie, że zachodzi
    \begin{align}
      \begin{split}
	h(x_1,\dots,x_k)&<A(z_h,\max(x_1,\dots,x_k),2) \\
	&\text{dla }\max(x_1,\dots,x_k)\geq 4,
      \end{split}\label{eq:PR4_h}\\
      \begin{split}
	g_i(x_1,\dots,x_n)&<A(z_{g_i},\max(x_1,\dots,x_n),2) \\
	&\text{dla }\max(x_1,\dots,x_n)\geq 4
	\text{ i }1\leq i\leq k.
      \end{split}\label{eq:PR4_g}
    \end{align}
    Wtedy dla $f:\N^n\rightarrow\N$ danej wzorem:
    \begin{equation*}
      f(x_1,\dots,x_n)=h\bigl(g_1(x_1,\dots,x_n),\dots,g_k(x_1,\dots,x_n)\bigr)
    \end{equation*}
    istnieje stała $z_f\geq 2$ taka, że
    \begin{equation}
      \begin{split}
	f(x_1,\dots,x_n)&<A(z_f,\max(x_1,\dots,x_n),2) \\
	&\text{dla }\max(x_1,\dots,x_n)\geq 4.
      \end{split}
    \end{equation}
  \end{lem}
  \begin{proof}
    Niech
    \begin{equation}
      N_h=\max_{x_1,\dots,x_k<4}h(x_1,\dots,x_k).\label{eq:PR4_N_h_def}
    \end{equation}
    Z lematu \ref{ack_lem_const} mamy, że istnieje stała $z_{N_h}\geq 2$, że
    \begin{equation}
      N_h < A(z_{N_h},y,2)\qquad\text{dla }y\geq 3.\label{eq:PR4_N_h_up}
    \end{equation}
    Wystarczy przyjąć:
    \begin{equation}
      z_f = \max(z_{N_h},z_h,z_{g_1},\dots,z_{g_k})+1.\label{eq:PR4_z_f}
    \end{equation}
    Oznaczmy $X=\max(x_1,\dots,x_n)$. Zakładamy, że $X \geq 4$.
    Należy wykazać, że $f(x_1,\dots,x_n)<A(z_f,X,2)$.
    
    Rozpatrzmy dwa przypadki.
    \begin{enumerate}
      \item
	$\max\bigl(g_1(x_1,\dots,x_n),\dots,g_k(x_1,\dots,x_n)\bigr) < 4$.
        Wtedy
	\begin{multline*}
	  h\bigl(g_1(x_1,\dots,x_n),\dots,g_k(x_1,\dots,x_n)\bigr)
	  \relref{eq:PR4_N_h_def}{\leq} N_h\\
	  \relref{eq:PR4_N_h_up}{<}A(z_{N_h},X,2)
	  \relrefand{eq:ack_zup}{eq:PR4_z_f}\leq A(z_f,X,2).
	\end{multline*}
      \item
	$\max\bigl(g_1(x_1,\dots,x_n),\dots,g_k(x_1,\dots,x_n)\bigr) \geq 4$.
	Wtedy mamy:
	\begin{align*}
	  &h\bigl(g_1(x_1,\dots,x_n),\dots,g_k(x_1,\dots,x_n)\bigr)\\
	  \relref{eq:PR4_h}{<}
	  &A\bigl(z_h,\max\bigl(g_1(x_1,\dots,x_n),\dots,
	  g_k(x_1,\dots,x_n)\bigr),2\bigr)\\
	  \relrefand{eq:ack_yup}{eq:PR4_g}{\leq}
	  &A\bigl(z_h,\max\bigl(A(z_{g_1},X,2),\dots,
	  A(z_{g_k},X,2)\bigr),2\bigr)=(*)
	\end{align*}
	Z \eqref{eq:ack_zup} i \eqref{eq:PR4_z_f} mamy, że
	$A(z_{g_i},X,2)\leq A(z_f-1,X,2)$ dla $1\leq i \leq k$, więc
	$\max\bigl(A(z_{g_1},X,2),\dots,A(z_{g_k},X,2)\bigr)
	\leq A(z_f-1,X,2)$, skąd
	\begin{align*}
	  (*)&\relref{eq:ack_yup}{\leq}
	  A(z_h,A(z_f-1,X,2),2)\\
	  &\relrefand{eq:ack_yup}{eq:ack_zdown_yup}{\leq}
	  A(z_h,A(z_f,X-1,2),2)\\
	  &\relrefand{eq:ack_zup}{eq:PR4_z_f}{\leq}
	  A(z_f-1,A(z_f,X-1,2),2)\relref{eq:ackzyx}{=}A(z_f,X,2).
	\end{align*}
    \end{enumerate}
    W obu przypadkach otrzymaliśmy:
    \begin{equation*}
      f(x_1,\dots,x_n)=h\bigl(g_1(x_1,\dots,x_n),\dots,g_k(x_1,\dots,x_n)\bigr)
      \leq A(z_f,X,2).
    \end{equation*}
  \end{proof}
  
  \begin{lem}\label{PR5_fup_lem}
    Niech $g:\N^k\rightarrow\N,h:\N^{k+2}\rightarrow\N$. Niech
    $z_h,g_h\geq 2$ takie, że
    \begin{align}
      \begin{split}
        h(x_1,\dots,x_{k+2})&<A(z_h,\max(x_1,\dots,x_{k+2}),2) \\
        &\text{dla }\max(x_1,\dots,x_{k+2})\geq 4,
      \end{split}\label{eq:PR5_h} \\
      \begin{split}
        g(x_1,\dots,x_k)&<A(z_g,\max(x_1,\dots,x_k),2) \\
        &\text{dla }\max(x_1,\dots,x_k)\geq 4.
      \end{split}\label{eq:PR5_g}
    \end{align}
    Wtedy dla $f:\N^{k+1}\rightarrow\N$ danej wzorami:
    \begin{align*}
      f(0,x_1,\dots,x_k)&=g(x_1,\dots,x_k)\\
      f(n+1,x_1,\dots,x_k)&=h(n,f(n,x_1,\dots,x_k),x_1,\dots,x_k)
    \end{align*}
    istnieje stała $z_f\geq 2$ taka, że
    \begin{equation}
      \begin{split}
	f(n,x_1,\dots,x_k)&<A(z_f,\max(x_1,\dots,x_k)+n,2) \\
	&\text{dla }\max(n,x_1,\dots,x_k)\geq 4.
      \end{split}\label{eq:PR5_fup_lem}
    \end{equation}
  \end{lem}
  \begin{proof}
    Niech
    \begin{align}
      N_h&=\max_{x_1,\dots,x_{k+2}<4}h(x_1,\dots,x_{k+2}),
      \label{eq:PR5_N_h_def}\\
      N_f&=\max_{n,x_1,\dots,x_k<4}f(n,x_1,\dots,x_k).
      \label{eq:PR5_N_f_def}
    \end{align}
    Z lematu \ref{ack_lem_const} mamy, że istnieją stałe
    $z_{N_h},z_{N_f}\geq 2$, że dla $y\geq 3$ zachodzi:
    \begin{align}
      N_h < A(z_{N_h},y,2),\label{eq:PR5_N_h_up}\\
      N_f < A(z_{N_f},y,2).\label{eq:PR5_N_f_up}
    \end{align}
    Wystarczy przyjąć:
    \begin{equation}
      z_f = \max(z_g, z_h, z_{N_h}, z_{N_f}) + 1.
      \label{eq:PR5_def_z_f}
    \end{equation}
    Oznaczmy $X=\max(x_1,\dots,x_k)$. Wtedy $\max(n,x_1,\dots,x_k)=\max(n,X)$.
    
    Indukcja po $n$.
    \begin{enumerate}
      \item $n=0$. Mamy $\max(0,X)=X\geq 4$, więc
        \begin{equation*}
	  g(x_1,\dots,x_n)\relref{eq:PR5_g}{<}
	  A(z_g,X,2)\relrefand{eq:ack_zup}{eq:PR5_def_z_f}{\leq}A(z_f,X,2).
	\end{equation*}
      \item $n\geq 1$. Zakładamy, że $\max(n,X)\geq 4$. Założenie
	indukcyjne to
        \begin{equation}
	  \begin{split}
	    f(n-1,x_1,\dots,x_k)&<A(z_f,X+n-1,2)\\
	    &\text{dla }\max(n-1,X)\geq 4.\label{eq:PR5_ind_n}
	  \end{split}
	\end{equation}
	Oznaczmy $X'=\max(n-1,X,f(n-1,x_1,\dots,x_k))$. Rozważmy dwa przypadki.
	\begin{enumerate}
	  \item\label{case:Xprim_lt_4}
	    $X'<4$. Oczywiście jest $4\leq\max(n,X)\leq X+n$. Mamy
	    \begin{multline*}
	      f(n,x_1,\dots,x_k) =
	      h(n-1,f(n-1,x_1,\dots,x_k),x_1,\dots,x_k)\\
	      \relref{eq:PR5_N_h_def}{\leq}N_h\relref{eq:PR5_N_h_up}{<}
	      A(z_{N_h},X+n,2)
	      \relrefand{eq:ack_zup}{eq:PR5_def_z_f}{\leq}
	      A(z_f, X+n, 2).
	    \end{multline*}
	  \item\label{case:Xprim_geq_4}
	    $X'\geq 4$. Rozpatrzmy dwa przypadki.
	    \begin{enumerate}
	      \item\label{case:max_n1_X_lt_4}
		$\max(n-1,X)<4$. Ponieważ $\max(n,X)\geq 4$, więc
	        $\max(n-1,X)=3$.
	        Wtedy $X'=f(n-1,x_1,\dots,x_k)
		\relref{eq:PR5_N_f_def}{\leq}N_f\relref{eq:PR5_N_f_up}{<}
		A(z_{N_f},X+n-1,2)\relrefand{eq:ack_zup}{eq:PR5_def_z_f}{\leq}
		A(z_f, X+n, 2)$.
	      \item\label{case:max_n1_X_geq_4}
		$\max(n-1,X)\geq 4$. Wtedy oczywiście $\max(n-1,X)\geq X+n-1$
		i zachodzi:
		\begin{align*}
		  \max(n-1,X)\relref{eq:ack_geq_y1}{<}&A(z_f,\max(n-1,X),2)\\
		  \relref{eq:ack_yup}{\leq}&A(z_f,X+n-1,2),\\
		  f(n-1,x_1,\dots,x_k)\relref{eq:PR5_ind_n}{<}&
		  A(z_f,X+n-1,2),
		\end{align*}
		skąd $X'\leq A(z_f,X+n-1,2)$.
	    \end{enumerate}
	    W obu przypadkach \ref{case:max_n1_X_lt_4} oraz
	    \ref{case:max_n1_X_geq_4} otrzymaliśmy, że
	    \begin{equation}
	      X'<A(z_f,X+n-1,2).\label{eq:PR5_Xprim_up}
	    \end{equation}
	    Teraz mamy:
	    \begin{multline*}
	      f(n,x_1,\dots,x_k) =
	      h(n-1,f(n-1,x_1,\dots,x_k),x_1,\dots,x_k)\\
	      \begin{split}
		\relref{eq:PR5_h}{<}&A(z_h,X',2)
		\relrefand{eq:ack_zup}{eq:PR5_def_z_f}{\leq}A(z_f-1,X',2)\\
		\relrefand{eq:ack_yup}{eq:PR5_Xprim_up}{\leq}
		&A(z_f-1,A(z_f,X+n-1,2),2)\relref{eq:ackzyx}{=}A(z_f,X+n,2).
	      \end{split}
	    \end{multline*}
	\end{enumerate}
	W obu przypadkach \ref{case:Xprim_lt_4} oraz
	\ref{case:Xprim_geq_4} otrzymaliśmy $f(n,x_1,\dots,x_k)<A(z_f,X+n,2)$,
	co kończy krok indukcyjny.
    \end{enumerate}
  \end{proof}
  
  \begin{lem}\label{fup_lem}
    Jeśli $f:\N^k\rightarrow\N$ jest pierwotnie rekurencyjna, to istnieje
    stała $z_f \geq 2$ taka, że dla wszystkich $x_1,\dots,x_k$, że
    $\max(x_1,\dots,x_k)\geq 4$, zachodzi:
    \begin{equation}
      f(x_1,\dots,x_k) < A(z_f, \max(x_1,\dots,x_k), 2).
      \label{eq:fup_lem}
    \end{equation}
  \end{lem}
  \begin{proof}
    Indukcja względem długości definicji funkcji $f$.
    \begin{enumerate}
      \item\label{ack_main_ind1}
        Długość definicji jest równa 1. Wtedy definicja jest postaci
	(PR1)-(PR3).
	\begin{itemize}
	  \item (PR1). Wystarczy przyjąć $z_f=2$. Wtedy dla $x\geq 2$ mamy
	    $f(x)=x+1\relref{eq:2tox_gt_x1}{<}2^x\relref{eq:ack_z2}{=}A(2,x,2)$.
	  \item (PR2). Wystarczy przyjąć $z_f=2$. Wtedy
	    $f(x_1,\dots,x_n)=0<2^0\relref{eq:ack_z2}{=}A(2,0,2)
	    \relref{eq:ack_yup}{\leq} A(2,\max(x_1,\dots,x_n),2)$.
	  \item (PR3). Wystarczy przyjąć $z_f=2$. Wtedy
	    $f(x_1,\dots,x_n)=x_i\relref{eq:2tox_gt_x}{<}2^{x_i}
	    \relref{eq:ack_z2}{=}A(2,x_i,2)
	    \relref{eq:ack_yup}{\leq}A(2,\max(x_1,\dots,x_n),2)$.
	\end{itemize}
      \item
        W przypadku, gdy definicja $f$ jest postaci (PR1)-(PR3) to postępujemy
	jak w punkcie \ref{ack_main_ind1}. Rozpatrzmy pozostałe dwa przypadki.
	\begin{itemize}
	  \item (PR4). Zakładamy, że funkcje $h,g_1,\dots,g_k$ spełniają
	    własność \eqref{eq:fup_lem}. Wtedy teza wynika bezpośrednio z
	    lematu \ref{PR4_fup_lem}.
	  \item (PR5). Zakładamy, że funkcje $g,h$ spełniają własność
	    \eqref{eq:fup_lem}. Z lematu \ref{PR5_fup_lem} mamy, że istnieje
	    stała $z'_f$ taka, że
	    \begin{equation}
	      \begin{split}
		f(n,x_1,\dots,x_k)&<A(z'_f,\max(x_1,\dots,x_k)+n,2) \\
		&\text{dla }\max(n,x_1,\dots,x_k)\geq 4.
	      \end{split}\label{eq:PR5_fup_sum}
	    \end{equation}
	    Wystarczy przyjąć $z_f=z'_f+1$.
	    Wobec oczywistej nierówności
	    $$\max(x_1,\dots,x_k)+n\leq 2\max(n,x_1,\dots,x_k)$$
	    mamy
	    \begin{align*}
	      f(n,x_1,\dots,x_k)&<A(z'_f,\max(x_1,\dots,x_k)+n,2) \\
	      &\relref{eq:ack_yup}{\leq}A(z'_f,2\max(n,x_1,\dots,x_k),2) \\
	      &\relref{eq:ack_zdown_2y}{\leq}A(z_f,\max(n,x_1,\dots,x_k),2),
	    \end{align*}
	    a to jest teza.
	\end{itemize}
    \end{enumerate}
  \end{proof}

  \begin{thm}
    Funkcja Ackermana nie jest pierwotnie rekurencyjna.
  \end{thm}
  \begin{proof}
    Załóżmy, że $A\in PR$. Niech $g_1(x)=g_2(x)=x$ i $g_3(x)=2$.
    $g_1,g_2\in PR$ z własności (PR3), a $g_3\in PR$ z lematu
    \ref{PR_const_lem}. Definiujemy funkcję:
    \begin{equation}
      f(x)=A(g_1(x),g_2(x),g_3(x))=A(x,x,2).\label{eq:f_ack}
    \end{equation}
    Z własności (PR4) mamy $f\in PR$, więc na mocy lematu \ref{fup_lem}
    istnieje stała $z_f\geq 2$, że dla $x \geq 4$ zachodzi $f(x) < A(z_f,x,2)$.
    Dla $x \geq z_f$ mamy
    \begin{equation*}
      f(x) < A(z_f,x,2)\relref{eq:ack_zup}{\leq}A(x,x,2),
    \end{equation*}
    co jest sprzeczne z \eqref{eq:f_ack}.
  \end{proof}

\end{document}
