theory UTM

imports Recursive Abacus UF GCD Turing_Hoare

begin

section {* Wang coding of input arguments *}

text {*

\newlength{\basewidth}

\settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx}

\newlength{\baseheight}

\settoheight{\baseheight}{$B:R$}

\newcommand{\vsep}{5\baseheight}

The TM used to generate the Wang's code of input arguments is divided into three TMs

 executed sequentially, namely $prepare$, $mainwork$ and $adjust$\<exclamdown>\<pounds>According to the

 convention, start state of ever TM is fixed to state $1$ while the final state is

 fixed to $0$.

The input and output of $prepare$ are illustrated respectively by Figure

\ref{prepare_input} and \ref{prepare_output}.

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  [tbox/.style = {draw, thick, inner sep = 5pt}]

  \node (0) {};

  \node (1) [tbox, text height = 3.5pt, right = -0.9pt of 0] {\wuhao $m$};

  \node (2) [tbox, right = -0.9pt of 1] {\wuhao $0$};

  \node (3) [tbox, right = -0.9pt of 2] {\wuhao $a_1$};

  \node (4) [tbox, right = -0.9pt of 3] {\wuhao $0$};

  \node (5) [tbox, right = -0.9pt of 4] {\wuhao $a_2$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [tbox, right = -0.9pt of 6] {\wuhao $a_n$};

  \draw [->, >=latex, thick] (1)+(0, -4\baseheight) -- (1);

\end{tikzpicture}}

\caption{The input of TM $prepare$} \label{prepare_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.5pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_n$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $0$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $1$};

  \draw [->, >=latex, thick] (10)+(0, -4\baseheight) -- (10);

\end{tikzpicture}}

\caption{The output of TM $prepare$} \label{prepare_output}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{0.9}{

\begin{tikzpicture}

     \node[circle,draw] (1) {$1$};

     \node[circle,draw] (2) at ($(1)+(0.3\basewidth, 0)$) {$2$};

     \node[circle,draw] (3) at ($(2)+(0.3\basewidth, 0)$) {$3$};

     \node[circle,draw] (4) at ($(3)+(0.3\basewidth, 0)$) {$4$};

     \node[circle,draw] (5) at ($(4)+(0.3\basewidth, 0)$) {$5$};

     \node[circle,draw] (6) at ($(5)+(0.3\basewidth, 0)$) {$6$};

     \node[circle,draw] (7) at ($(6)+(0.3\basewidth, 0)$) {$7$};

     \node[circle,draw] (8) at ($(7)+(0.3\basewidth, 0)$) {$0$};

     \draw [->, >=latex] (1) edge [loop above] node[above] {$S_1:L$} (1)

     ;

     \draw [->, >=latex] (1) -- node[above] {$S_0:S_1$} (2)

     ;

     \draw [->, >=latex] (2) edge [loop above] node[above] {$S_1:R$} (2)

     ;

     \draw [->, >=latex] (2) -- node[above] {$S_0:L$} (3)

     ;

     \draw [->, >=latex] (3) edge[loop above] node[above] {$S_1:S_0$} (3)

     ;

     \draw [->, >=latex] (3) -- node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) edge[loop above] node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) -- node[above] {$S_0:R$} (5)

     ;

     \draw [->, >=latex] (5) edge[loop above] node[above] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (5) -- node[above] {$S_0:R$} (6)

     ;

     \draw [->, >=latex] (6) edge[bend left = 50] node[below] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (6) -- node[above] {$S_0:R$} (7)

     ;

     \draw [->, >=latex] (7) edge[loop above] node[above] {$S_0:S_1$} (7)

     ;

     \draw [->, >=latex] (7) -- node[above] {$S_1:L$} (8)

     ;

 \end{tikzpicture}}

\caption{The diagram of TM $prepare$} \label{prepare_diag}

\end{figure}

The purpose of TM $mainwork$ is to compute the Wang's encoding of $a_1, \ldots, a_n$. Every bit of $a_1, \ldots, a_n$, including the separating bits, is processed from left to right.

In order to detect the termination condition when the left most bit of $a_1$ is reached,

TM $mainwork$ needs to look ahead and consider three different situations at the start of

every iteration:

\begin{enumerate}

    \item The TM configuration for the first situation is shown in Figure \ref{mainwork_case_one_input},

        where the accumulator is stored in $r$, both of the next two bits

        to be encoded are $1$. The configuration at the end of the iteration

        is shown in Figure \ref{mainwork_case_one_output}, where the first 1-bit has been

        encoded and cleared. Notice that the accumulator has been changed to

        $(r+1) \times 2$ to reflect the encoded bit.

    \item The TM configuration for the second situation is shown in Figure

        \ref{mainwork_case_two_input},

        where the accumulator is stored in $r$, the next two bits

        to be encoded are $1$ and $0$. After the first

        $1$-bit was encoded and cleared, the second $0$-bit is difficult to detect

        and process. To solve this problem, these two consecutive bits are

        encoded in one iteration.  In this situation, only the first $1$-bit needs

        to be cleared since the second one is cleared by definition.

        The configuration at the end of the iteration

        is shown in Figure \ref{mainwork_case_two_output}.

        Notice that the accumulator has been changed to

        $(r+1) \times 4$ to reflect the two encoded bits.

    \item The third situation corresponds to the case when the last bit of $a_1$ is reached.

        The TM configurations at the start and end of the iteration are shown in

        Figure \ref{mainwork_case_three_input} and \ref{mainwork_case_three_output}

        respectively. For this situation, only the read write head needs to be moved to

        the left to prepare a initial configuration for TM $adjust$ to start with.

\end{enumerate}

The diagram of $mainwork$ is given in Figure \ref{mainwork_diag}. The two rectangular nodes

labeled with $2 \times x$ and $4 \times x$ are two TMs compiling from recursive functions

so that we do not have to design and verify two quite complicated TMs.

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $1$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $0$};

  \node (12) [right = -0.9pt of 11] {\ldots \ldots};

  \node (13) [draw, right = -0.9pt of 12, thick, inner sep = 5pt] {\wuhao $0$};

  \node (14) [draw, text height = 3.9pt, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (13)+(0, -4\baseheight) -- (13);

\end{tikzpicture}}

\caption{The first situation for TM $mainwork$ to consider} \label{mainwork_case_one_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $0$};

  \node (12) [right = -0.9pt of 11] {\ldots \ldots};

  \node (13) [draw, right = -0.9pt of 12, thick, inner sep = 5pt] {\wuhao $0$};

  \node (14) [draw, text height = 2.7pt, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $(r+1) \times 2$};

  \draw [->, >=latex, thick] (13)+(0, -4\baseheight) -- (13);

\end{tikzpicture}}

\caption{The output for the first case of TM $mainwork$'s processing}

\label{mainwork_case_one_output}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $1$};

  \node (12) [draw, right = -0.9pt of 11, thick, inner sep = 5pt] {\wuhao $0$};

  \node (13) [right = -0.9pt of 12] {\ldots \ldots};

  \node (14) [draw, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $0$};

  \node (15) [draw, text height = 3.9pt, right = -0.9pt of 14, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (14)+(0, -4\baseheight) -- (14);

\end{tikzpicture}}

\caption{The second situation for TM $mainwork$ to consider} \label{mainwork_case_two_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $0$};

  \node (12) [draw, right = -0.9pt of 11, thick, inner sep = 5pt] {\wuhao $0$};

  \node (13) [right = -0.9pt of 12] {\ldots \ldots};

  \node (14) [draw, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $0$};

  \node (15) [draw, text height = 2.7pt, right = -0.9pt of 14, thick, inner sep = 5pt] {\wuhao $(r+1) \times 4$};

  \draw [->, >=latex, thick] (14)+(0, -4\baseheight) -- (14);

\end{tikzpicture}}

\caption{The output for the second case of TM $mainwork$'s processing}

\label{mainwork_case_two_output}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [draw, right = -0.9pt of 6, thick, inner sep = 5pt] {\wuhao $0$};

  \node (8) [draw, text height = 3.9pt, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (7)+(0, -4\baseheight) -- (7);

\end{tikzpicture}}

\caption{The third situation for TM $mainwork$ to consider} \label{mainwork_case_three_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [draw, right = -0.9pt of 6, thick, inner sep = 5pt] {\wuhao $0$};

  \node (8) [draw, text height = 3.9pt, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (3)+(0, -4\baseheight) -- (3);

\end{tikzpicture}}

\caption{The output for the third case of TM $mainwork$'s processing}

\label{mainwork_case_three_output}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{0.9}{

\begin{tikzpicture}

     \node[circle,draw] (1) {$1$};

     \node[circle,draw] (2) at ($(1)+(0.3\basewidth, 0)$) {$2$};

     \node[circle,draw] (3) at ($(2)+(0.3\basewidth, 0)$) {$3$};

     \node[circle,draw] (4) at ($(3)+(0.3\basewidth, 0)$) {$4$};

     \node[circle,draw] (5) at ($(4)+(0.3\basewidth, 0)$) {$5$};

     \node[circle,draw] (6) at ($(5)+(0.3\basewidth, 0)$) {$6$};

     \node[circle,draw] (7) at ($(2)+(0, -7\baseheight)$) {$7$};

     \node[circle,draw] (8) at ($(7)+(0, -7\baseheight)$) {$8$};

     \node[circle,draw] (9) at ($(8)+(0.3\basewidth, 0)$) {$9$};

     \node[circle,draw] (10) at ($(9)+(0.3\basewidth, 0)$) {$10$};

     \node[circle,draw] (11) at ($(10)+(0.3\basewidth, 0)$) {$11$};

     \node[circle,draw] (12) at ($(11)+(0.3\basewidth, 0)$) {$12$};

     \node[draw] (13) at ($(6)+(0.3\basewidth, 0)$) {$2 \times x$};

     \node[circle,draw] (14) at ($(13)+(0.3\basewidth, 0)$) {$j_1$};

     \node[draw] (15) at ($(12)+(0.3\basewidth, 0)$) {$4 \times x$};

     \node[draw] (16) at ($(15)+(0.3\basewidth, 0)$) {$j_2$};

     \node[draw] (17) at ($(7)+(0.3\basewidth, 0)$) {$0$};

     \draw [->, >=latex] (1) edge[loop left] node[above] {$S_0:L$} (1)

     ;

     \draw [->, >=latex] (1) -- node[above] {$S_1:L$} (2)

     ;

     \draw [->, >=latex] (2) -- node[above] {$S_1:R$} (3)

     ;

     \draw [->, >=latex] (2) -- node[left] {$S_1:L$} (7)

     ;

     \draw [->, >=latex] (3) edge[loop above] node[above] {$S_1:S_0$} (3)

     ;

     \draw [->, >=latex] (3) -- node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) edge[loop above] node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) -- node[above] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (5) edge[loop above] node[above] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (5) -- node[above] {$S_0:S_1$} (6)

     ;

     \draw [->, >=latex] (6) edge[loop above] node[above] {$S_1:L$} (6)

     ;

     \draw [->, >=latex] (6) -- node[above] {$S_0:R$} (13)

     ;

     \draw [->, >=latex] (13) -- (14)

     ;

     \draw (14) -- ($(14)+(0, 6\baseheight)$) -- ($(1) + (0, 6\baseheight)$) node [above,midway] {$S_1:L$}

     ;

     \draw [->, >=latex] ($(1) + (0, 6\baseheight)$) -- (1)

     ;

     \draw [->, >=latex] (7) -- node[above] {$S_0:R$} (17)

     ;

     \draw [->, >=latex] (7) -- node[left] {$S_1:R$} (8)

     ;

     \draw [->, >=latex] (8) -- node[above] {$S_0:R$} (9)

     ;

     \draw [->, >=latex] (9) -- node[above] {$S_0:R$} (10)

     ;

     \draw [->, >=latex] (10) -- node[above] {$S_1:R$} (11)

     ;

     \draw [->, >=latex] (10) edge[loop above] node[above] {$S_0:R$} (10)

     ;

     \draw [->, >=latex] (11) edge[loop above] node[above] {$S_1:R$} (11)

     ;

     \draw [->, >=latex] (11) -- node[above] {$S_0:S_1$} (12)

     ;

     \draw [->, >=latex] (12) -- node[above] {$S_0:R$} (15)

     ;

     \draw [->, >=latex] (12) edge[loop above] node[above] {$S_1:L$} (12)

     ;

     \draw [->, >=latex] (15) -- (16)

     ;

     \draw (16) -- ($(16)+(0, -4\baseheight)$) -- ($(1) + (0, -18\baseheight)$) node [below,midway] {$S_1:L$}

     ;

     \draw [->, >=latex] ($(1) + (0, -18\baseheight)$) -- (1)

     ;

 \end{tikzpicture}}

\caption{The diagram of TM $mainwork$} \label{mainwork_diag}

\end{figure}

The purpose of TM $adjust$ is to encode the last bit of $a_1$. The initial and final configuration

of this TM are shown in Figure \ref{adjust_initial} and \ref{adjust_final} respectively.

The diagram of TM $adjust$ is shown in Figure \ref{adjust_diag}.

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [draw, right = -0.9pt of 6, thick, inner sep = 5pt] {\wuhao $0$};

  \node (8) [draw, text height = 3.9pt, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (3)+(0, -4\baseheight) -- (3);

\end{tikzpicture}}

\caption{Initial configuration of TM $adjust$} \label{adjust_initial}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, text height = 2.9pt, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $r+1$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $0$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \draw [->, >=latex, thick] (1)+(0, -4\baseheight) -- (1);

\end{tikzpicture}}

\caption{Final configuration of TM $adjust$} \label{adjust_final}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{0.9}{

\begin{tikzpicture}

     \node[circle,draw] (1) {$1$};

     \node[circle,draw] (2) at ($(1)+(0.3\basewidth, 0)$) {$2$};

     \node[circle,draw] (3) at ($(2)+(0.3\basewidth, 0)$) {$3$};

     \node[circle,draw] (4) at ($(3)+(0.3\basewidth, 0)$) {$4$};

     \node[circle,draw] (5) at ($(4)+(0.3\basewidth, 0)$) {$5$};

     \node[circle,draw] (6) at ($(5)+(0.3\basewidth, 0)$) {$6$};

     \node[circle,draw] (7) at ($(6)+(0.3\basewidth, 0)$) {$7$};

     \node[circle,draw] (8) at ($(4)+(0, -7\baseheight)$) {$8$};

     \node[circle,draw] (9) at ($(8)+(0.3\basewidth, 0)$) {$9$};

     \node[circle,draw] (10) at ($(9)+(0.3\basewidth, 0)$) {$10$};

     \node[circle,draw] (11) at ($(10)+(0.3\basewidth, 0)$) {$11$};

     \node[circle,draw] (12) at ($(11)+(0.3\basewidth, 0)$) {$0$};

     \draw [->, >=latex] (1) -- node[above] {$S_1:R$} (2)

     ;

     \draw [->, >=latex] (1) edge[loop above] node[above] {$S_0:S_1$} (1)

     ;

     \draw [->, >=latex] (2) -- node[above] {$S_1:R$} (3)

     ;

     \draw [->, >=latex] (3) edge[loop above] node[above] {$S_0:R$} (3)

     ;

     \draw [->, >=latex] (3) -- node[above] {$S_1:R$} (4)

     ;

     \draw [->, >=latex] (4) -- node[above] {$S_1:L$} (5)

     ;

     \draw [->, >=latex] (4) -- node[right] {$S_0:L$} (8)

     ;

     \draw [->, >=latex] (5) -- node[above] {$S_0:L$} (6)

     ;

     \draw [->, >=latex] (5) edge[loop above] node[above] {$S_1:S_0$} (5)

     ;

     \draw [->, >=latex] (6) -- node[above] {$S_1:R$} (7)

     ;

     \draw [->, >=latex] (6) edge[loop above] node[above] {$S_0:L$} (6)

     ;

     \draw (7) -- ($(7)+(0, 6\baseheight)$) -- ($(2) + (0, 6\baseheight)$) node [above,midway] {$S_0:S_1$}

     ;

     \draw [->, >=latex] ($(2) + (0, 6\baseheight)$) -- (2)

     ;

     \draw [->, >=latex] (8) edge[loop left] node[left] {$S_1:S_0$} (8)

     ;

     \draw [->, >=latex] (8) -- node[above] {$S_0:L$} (9)

     ;

     \draw [->, >=latex] (9) edge[loop above] node[above] {$S_0:L$} (9)

     ;

     \draw [->, >=latex] (9) -- node[above] {$S_1:L$} (10)

     ;

     \draw [->, >=latex] (10) edge[loop above] node[above] {$S_0:L$} (10)

     ;

     \draw [->, >=latex] (10) -- node[above] {$S_0:L$} (11)

     ;

     \draw [->, >=latex] (11) edge[loop above] node[above] {$S_1:L$} (11)

     ;

     \draw [->, >=latex] (11) -- node[above] {$S_0:R$} (12)

     ;

 \end{tikzpicture}}

\caption{Diagram of TM $adjust$} \label{adjust_diag}

\end{figure}

*}

definition rec_twice :: "recf"

  where

  "rec_twice = Cn 1 rec_mult [id 1 0, constn 2]"

definition rec_fourtimes  :: "recf"

  where

  "rec_fourtimes = Cn 1 rec_mult [id 1 0, constn 4]"

definition abc_twice :: "abc_prog"

  where

  "abc_twice = (let (aprog, ary, fp) = rec_ci rec_twice in 

                       aprog [+] dummy_abc ((Suc 0)))"

definition abc_fourtimes :: "abc_prog"

  where

  "abc_fourtimes = (let (aprog, ary, fp) = rec_ci rec_fourtimes in 

                       aprog [+] dummy_abc ((Suc 0)))"