(* Title: thys/UTM.thy

   Author: Jian Xu, Xingyuan Zhang, and Christian Urban

*)

chapter {* Construction of a Universal Turing Machine *}

theory UTM

imports Recursive Abacus UF HOL.GCD Turing_Hoare

begin

section {* Wang coding of input arguments *}

text {*

  The direct compilation of the universal function @{text "rec_F"} can

  not give us UTM, because @{text "rec_F"} is of arity 2, where the

  first argument represents the Godel coding of the TM being simulated

  and the second argument represents the right number (in Wang's

  coding) of the TM tape.  (Notice, left number is always @{text "0"}

  at the very beginning). However, UTM needs to simulate the execution

  of any TM which may very well take many input arguments. Therefore,

  a initialization TM needs to run before the TM compiled from @{text

  "rec_F"}, and the sequential composition of these two TMs will give

  rise to the UTM we are seeking. The purpose of this initialization

  TM is to transform the multiple input arguments of the TM being

  simulated into Wang's coding, so that it can be consumed by the TM

  compiled from @{text "rec_F"} as the second argument.

  However, this initialization TM (named @{text "t_wcode"}) can not be

  constructed by compiling from any recursive function, because every

  recursive function takes a fixed number of input arguments, while

  @{text "t_wcode"} needs to take varying number of arguments and

  tranform them into Wang's coding. Therefore, this section give a

  direct construction of @{text "t_wcode"} with just some parts being

  obtained from recursive functions.

\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}

As shown in Figure \ref{prepare_input}, the input of $prepare$ is the

same as the the input of UTM, where $m$ is the Godel coding of the TM

being interpreted and $a_1$ through $a_n$ are the $n$ input arguments

of the TM under interpretation. The purpose of $purpose$ is to

transform this initial tape layout to the one shown in Figure

\ref{prepare_output}, which is convenient for the generation of Wang's

codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$

and ends after $a_1$ is encoded. The coding result is stored in an

accumulator at the end of the tape (initially represented by the $1$

two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure

\ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by

two blanks on both ends with the rest so that movement conditions can

be implemented conveniently in subsequent TMs, because, by convention,

two consecutive blanks are usually used to signal the end or start of

a large chunk of data. The diagram of $prepare$ is given in Figure

\ref{prepare_diag}.

\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)))"