1 theory UTM

     2 imports Main uncomputable recursive abacus UF GCD 

     3 begin

     4 

     5 section {* Wang coding of input arguments *}

     6 

     7 text {*

     8   The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2,

     9   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. 

    10   (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may

    11   very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential 

    12   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 

    13   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

    14   argument. 

    15 

    16   However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive 

    17   function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into 

    18   Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions.

    19 

    20 \newlength{\basewidth}

    21 \settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx}

    22 \newlength{\baseheight}

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

    24 \newcommand{\vsep}{5\baseheight}

    25 

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

    27  executed sequentially, namely $prepare$, $mainwork$ and $adjust$¡£According to the

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

    29  fixed to $0$.

    30 

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

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

    33 

    34 

    35 \begin{figure}[h!]

    36 \centering

    37 \scalebox{1.2}{

    38 \begin{tikzpicture}

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

    40   \node (0) {};

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

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

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

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

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

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

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

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

    49 \end{tikzpicture}}

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

    51 \end{figure}

    52 

    53 \begin{figure}[h!]

    54 \centering

    55 \scalebox{1.2}{

    56 \begin{tikzpicture}

    57   \node (0) {};

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

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

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

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

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

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

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

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

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

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

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

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

    70 \end{tikzpicture}}

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

    72 \end{figure}

    73 

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

    75 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},

    76 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,

    77 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}.

    78 

    79 

    80 \begin{figure}[h!]

    81 \centering

    82 \scalebox{0.9}{

    83 \begin{tikzpicture}

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

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

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

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

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

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

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

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

    92 

    93 

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

    95      ;

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

    97      ;

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

    99      ;

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

   101      ;

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

   103      ;

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

   105      ;

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

   107      ;

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

   109      ;

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

   111      ;

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

   113      ;

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

   115      ;

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

   117      ;

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

   119      ;

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

   121      ;

   122  \end{tikzpicture}}

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

   124 \end{figure}

   125 

   126 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.

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

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

   129 every iteration:

   130 \begin{enumerate}

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

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

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

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

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

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

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

   138         \ref{mainwork_case_two_input},

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

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

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

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

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

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

   145         The configuration at the end of the iteration

   146         is shown in Figure \ref{mainwork_case_two_output}.

   147         Notice that the accumulator has been changed to

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

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

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

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

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

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

   154 \end{enumerate}

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

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

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

   158 

   159 

   160 \begin{figure}[h!]

   161 \centering

   162 \scalebox{1.2}{

   163 \begin{tikzpicture}

   164   \node (0) {};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   180 \end{tikzpicture}}

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

   182 \end{figure}

   183 

   184 

   185 \begin{figure}[h!]

   186 \centering

   187 \scalebox{1.2}{

   188 \begin{tikzpicture}

   189   \node (0) {};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   205 \end{tikzpicture}}

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

   207 \label{mainwork_case_one_output}

   208 \end{figure}

   209 

   210 \begin{figure}[h!]

   211 \centering

   212 \scalebox{1.2}{

   213 \begin{tikzpicture}

   214   \node (0) {};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   231 \end{tikzpicture}}

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

   233 \end{figure}

   234 

   235 \begin{figure}[h!]

   236 \centering

   237 \scalebox{1.2}{

   238 \begin{tikzpicture}

   239   \node (0) {};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   256 \end{tikzpicture}}

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

   258 \label{mainwork_case_two_output}

   259 \end{figure}

   260 

   261 \begin{figure}[h!]

   262 \centering

   263 \scalebox{1.2}{

   264 \begin{tikzpicture}

   265   \node (0) {};

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

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

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

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

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

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

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

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

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

   275 \end{tikzpicture}}

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

   277 \end{figure}

   278 

   279 \begin{figure}[h!]

   280 \centering

   281 \scalebox{1.2}{

   282 \begin{tikzpicture}

   283   \node (0) {};

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

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

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

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

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

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

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

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

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

   293 \end{tikzpicture}}

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

   295 \label{mainwork_case_three_output}

   296 \end{figure}

   297 

   298 \begin{figure}[h!]

   299 \centering

   300 \scalebox{0.9}{

   301 \begin{tikzpicture}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   319 

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

   321      ;

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

   323      ;

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

   325      ;

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

   327      ;

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

   329      ;

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

   331      ;

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

   333      ;

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

   335      ;

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

   337      ;

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

   339      ;

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

   341      ;

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

   343      ;

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

   345      ;

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

   347      ;

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

   349      ;

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

   351      ;

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

   353      ;

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

   355      ;

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

   357      ;

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

   359      ;

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

   361      ;

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

   363      ;

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

   365      ;

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

   367      ;

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

   369      ;

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

   371      ;

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

   373      ;

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

   375      ;

   376  \end{tikzpicture}}

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

   378 \end{figure}

   379 

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

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

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

   383 

   384 

   385 \begin{figure}[h!]

   386 \centering

   387 \scalebox{1.2}{

   388 \begin{tikzpicture}

   389   \node (0) {};

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

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

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

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

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

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

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

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

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

   399 \end{tikzpicture}}

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

   401 \end{figure}

   402 

   403 \begin{figure}[h!]

   404 \centering

   405 \scalebox{1.2}{

   406 \begin{tikzpicture}

   407   \node (0) {};

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

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

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

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

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

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

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

   415 \end{tikzpicture}}

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

   417 \end{figure}

   418 

   419 

   420 \begin{figure}[h!]

   421 \centering

   422 \scalebox{0.9}{

   423 \begin{tikzpicture}

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

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

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

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

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

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

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

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

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

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

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

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

   436 

   437 

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

   439      ;

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

   441      ;

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

   443      ;

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

   445      ;

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

   447      ;

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

   449      ;

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

   451      ;

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

   453      ;

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

   455      ;

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

   457      ;

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

   459      ;

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

   461      ;

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

   463      ;

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

   465      ;

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

   467      ;

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

   469      ;

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

   471      ;

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

   473      ;

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

   475      ;

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

   477      ;

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

   479      ;

   480  \end{tikzpicture}}

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

   482 \end{figure}

   483 *}

   484 

   485 

   486 definition rec_twice :: "recf"

   487   where

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

   489 

   490 definition rec_fourtimes  :: "recf"

   491   where

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

   493 

   494 definition abc_twice :: "abc_prog"

   495   where

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

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

   498 

   499 definition abc_fourtimes :: "abc_prog"

   500   where

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

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

   503 

   504 definition twice_ly :: "nat list"

   505   where

   506   "twice_ly = layout_of abc_twice"

   507 

   508 definition fourtimes_ly :: "nat list"

   509   where

   510   "fourtimes_ly = layout_of abc_fourtimes"

   511 

   512 definition t_twice :: "tprog"

   513   where

   514   "t_twice = change_termi_state (tm_of (abc_twice) @ (tMp 1 (start_of twice_ly (length abc_twice) - Suc 0)))"

   515 

   516 definition t_fourtimes :: "tprog"

   517   where

   518   "t_fourtimes = change_termi_state (tm_of (abc_fourtimes) @ 

   519              (tMp 1 (start_of fourtimes_ly (length abc_fourtimes) - Suc 0)))"

   520 

   521 

   522 definition t_twice_len :: "nat"

   523   where

   524   "t_twice_len = length t_twice div 2"

   525 

   526 definition t_wcode_main_first_part:: "tprog"

   527   where

   528   "t_wcode_main_first_part \<equiv> 

   529                    [(L, 1), (L, 2), (L, 7), (R, 3),

   530                     (R, 4), (W0, 3), (R, 4), (R, 5),

   531                     (W1, 6), (R, 5), (R, 13), (L, 6),

   532                     (R, 0), (R, 8), (R, 9), (Nop, 8),

   533                     (R, 10), (W0, 9), (R, 10), (R, 11), 

   534                     (W1, 12), (R, 11), (R, t_twice_len + 14), (L, 12)]"

   535 

   536 definition t_wcode_main :: "tprog"

   537   where

   538   "t_wcode_main = (t_wcode_main_first_part @ tshift t_twice 12 @ [(L, 1), (L, 1)]

   539                     @ tshift t_fourtimes (t_twice_len + 13) @ [(L, 1), (L, 1)])"

   540 

   541 fun bl_bin :: "block list \<Rightarrow> nat"

   542   where

   543   "bl_bin [] = 0" 

   544 | "bl_bin (Bk # xs) = 2 * bl_bin xs"

   545 | "bl_bin (Oc # xs) = Suc (2 * bl_bin xs)"

   546 

   547 declare bl_bin.simps[simp del]

   548 

   549 type_synonym bin_inv_t = "block list \<Rightarrow> nat \<Rightarrow> tape \<Rightarrow> bool"

   550 

   551 fun wcode_before_double :: "bin_inv_t"

   552   where

   553   "wcode_before_double ires rs (l, r) =

   554      (\<exists> ln rn. l = Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

   555                r = Oc\<^bsup>(Suc (Suc rs))\<^esup> @ Bk\<^bsup>rn \<^esup>)"

   556 

   557 declare wcode_before_double.simps[simp del]

   558 

   559 fun wcode_after_double :: "bin_inv_t"

   560   where

   561   "wcode_after_double ires rs (l, r) = 

   562      (\<exists> ln rn. l = Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>

   563          r = Oc\<^bsup>Suc (Suc (Suc 2*rs))\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   564 

   565 declare wcode_after_double.simps[simp del]

   566 

   567 fun wcode_on_left_moving_1_B :: "bin_inv_t"

   568   where

   569   "wcode_on_left_moving_1_B ires rs (l, r) = 

   570      (\<exists> ml mr rn. l = Bk\<^bsup>ml\<^esup> @ Oc # Oc # ires \<and> 

   571                r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   572                ml + mr > Suc 0 \<and> mr > 0)"

   573 

   574 declare wcode_on_left_moving_1_B.simps[simp del]

   575 

   576 fun wcode_on_left_moving_1_O :: "bin_inv_t"

   577   where

   578   "wcode_on_left_moving_1_O ires rs (l, r) = 

   579      (\<exists> ln rn.

   580                l = Oc # ires \<and> 

   581                r = Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   582 

   583 declare wcode_on_left_moving_1_O.simps[simp del]

   584 

   585 fun wcode_on_left_moving_1 :: "bin_inv_t"

   586   where

   587   "wcode_on_left_moving_1 ires rs (l, r) = 

   588           (wcode_on_left_moving_1_B ires rs (l, r) \<or> wcode_on_left_moving_1_O ires rs (l, r))"

   589 

   590 declare wcode_on_left_moving_1.simps[simp del]

   591 

   592 fun wcode_on_checking_1 :: "bin_inv_t"

   593   where

   594    "wcode_on_checking_1 ires rs (l, r) = 

   595     (\<exists> ln rn. l = ires \<and>

   596               r = Oc # Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   597 

   598 fun wcode_erase1 :: "bin_inv_t"

   599   where

   600 "wcode_erase1 ires rs (l, r) = 

   601        (\<exists> ln rn. l = Oc # ires \<and> 

   602                  tl r = Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   603 

   604 declare wcode_erase1.simps [simp del]

   605 

   606 fun wcode_on_right_moving_1 :: "bin_inv_t"

   607   where

   608   "wcode_on_right_moving_1 ires rs (l, r) = 

   609        (\<exists> ml mr rn.        

   610              l = Bk\<^bsup>ml\<^esup> @ Oc # ires \<and> 

   611              r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   612              ml + mr > Suc 0)"

   613 

   614 declare wcode_on_right_moving_1.simps [simp del] 

   615 

   616 declare wcode_on_right_moving_1.simps[simp del]

   617 

   618 fun wcode_goon_right_moving_1 :: "bin_inv_t"

   619   where

   620   "wcode_goon_right_moving_1 ires rs (l, r) = 

   621       (\<exists> ml mr ln rn. 

   622             l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

   623             r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   624             ml + mr = Suc rs)"

   625 

   626 declare wcode_goon_right_moving_1.simps[simp del]

   627 

   628 fun wcode_backto_standard_pos_B :: "bin_inv_t"

   629   where

   630   "wcode_backto_standard_pos_B ires rs (l, r) = 

   631           (\<exists> ln rn. l =  Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

   632                r =  Bk # Oc\<^bsup>(Suc (Suc rs))\<^esup> @ Bk\<^bsup>rn \<^esup>)"

   633 

   634 declare wcode_backto_standard_pos_B.simps[simp del]

   635 

   636 fun wcode_backto_standard_pos_O :: "bin_inv_t"

   637   where

   638    "wcode_backto_standard_pos_O ires rs (l, r) = 

   639         (\<exists> ml mr ln rn. 

   640             l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>

   641             r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   642             ml + mr = Suc (Suc rs) \<and> mr > 0)"

   643 

   644 declare wcode_backto_standard_pos_O.simps[simp del]

   645 

   646 fun wcode_backto_standard_pos :: "bin_inv_t"

   647   where

   648   "wcode_backto_standard_pos ires rs (l, r) = (wcode_backto_standard_pos_B ires rs (l, r) \<or>

   649                                             wcode_backto_standard_pos_O ires rs (l, r))"

   650 

   651 declare wcode_backto_standard_pos.simps[simp del]

   652 

   653 lemma [simp]: "<0::nat> = [Oc]"

   654 apply(simp add: tape_of_nat_abv exponent_def tape_of_nat_list.simps)

   655 done

   656 

   657 lemma tape_of_Suc_nat: "<Suc (a ::nat)> = replicate a Oc @ [Oc, Oc]"

   658 apply(simp add: tape_of_nat_abv exp_ind tape_of_nat_list.simps)

   659 apply(simp only: exp_ind_def[THEN sym])

   660 apply(simp only: exp_ind, simp, simp add: exponent_def)

   661 done

   662 

   663 lemma [simp]: "length (<a::nat>) = Suc a"

   664 apply(simp add: tape_of_nat_abv tape_of_nat_list.simps)

   665 done

   666 

   667 lemma [simp]: "<[a::nat]> = <a>"

   668 apply(simp add: tape_of_nat_abv tape_of_nl_abv exponent_def

   669                 tape_of_nat_list.simps)

   670 done

   671 

   672 lemma bin_wc_eq: "bl_bin xs = bl2wc xs"

   673 proof(induct xs)

   674   show " bl_bin [] = bl2wc []" 

   675     apply(simp add: bl_bin.simps)

   676     done

   677 next

   678   fix a xs

   679   assume "bl_bin xs = bl2wc xs"

   680   thus " bl_bin (a # xs) = bl2wc (a # xs)"

   681     apply(case_tac a, simp_all add: bl_bin.simps bl2wc.simps)

   682     apply(simp_all add: bl2nat.simps bl2nat_double)

   683     done

   684 qed

   685 

   686 declare exp_def[simp del]

   687 

   688 lemma bl_bin_nat_Suc:  

   689   "bl_bin (<Suc a>) = bl_bin (<a>) + 2^(Suc a)"

   690 apply(simp add: tape_of_nat_abv bin_wc_eq)

   691 apply(simp add: bl2wc.simps)

   692 done

   693 lemma [simp]: " rev (a\<^bsup>aa\<^esup>) = a\<^bsup>aa\<^esup>"

   694 apply(simp add: exponent_def)

   695 done

   696  

   697 declare tape_of_nl_abv_cons[simp del]

   698 

   699 lemma tape_of_nl_rev: "rev (<lm::nat list>) = (<rev lm>)"

   700 apply(induct lm rule: list_tl_induct, simp)

   701 apply(case_tac "list = []", simp add: tape_of_nl_abv tape_of_nat_list.simps)

   702 apply(simp add: tape_of_nat_list_butlast_last tape_of_nl_abv_cons)

   703 done

   704 lemma [simp]: "a\<^bsup>Suc 0\<^esup> = [a]" 

   705 by(simp add: exp_def)

   706 lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<^bsup>Suc a\<^esup> @ Bk # (<xs@ [b]>))"

   707 apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps)

   708 apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps)

   709 done

   710 

   711 lemma bl_bin_bk_oc[simp]:

   712   "bl_bin (xs @ [Bk, Oc]) = 

   713   bl_bin xs + 2*2^(length xs)"

   714 apply(simp add: bin_wc_eq)

   715 using bl2nat_cons_oc[of "xs @ [Bk]"]

   716 apply(simp add: bl2nat_cons_bk bl2wc.simps)

   717 done

   718 

   719 lemma tape_of_nat[simp]: "(<a::nat>) = Oc\<^bsup>Suc a\<^esup>"

   720 apply(simp add: tape_of_nat_abv)

   721 done

   722 lemma tape_of_nl_cons_app2: "(<c # xs @ [b]>) = (<c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>)"

   723 proof(induct "length xs" arbitrary: xs c,

   724   simp add: tape_of_nl_abv  tape_of_nat_list.simps)

   725   fix x xs c

   726   assume ind: "\<And>xs c. x = length xs \<Longrightarrow> <c # xs @ [b]> = 

   727     <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   728     and h: "Suc x = length (xs::nat list)" 

   729   show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   730   proof(case_tac xs, simp add: tape_of_nl_abv  tape_of_nat_list.simps)

   731     fix a list

   732     assume g: "xs = a # list"

   733     hence k: "<a # list @ [b]> =  <a # list> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   734       apply(rule_tac ind)

   735       using h

   736       apply(simp)

   737       done

   738     from g and k show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   739       apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

   740       done

   741   qed

   742 qed

   743 

   744 lemma [simp]: "length (<aa # a # list>) = Suc (Suc aa) + length (<a # list>)"

   745 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

   746 done

   747 

   748 lemma [simp]: "bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) =

   749               bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)) + 

   750               2* 2^(length (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)))"

   751 using bl_bin_bk_oc[of "Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)"]

   752 apply(simp)

   753 done

   754 

   755 lemma [simp]: 

   756   "bl_bin (<aa # list>) + (4 * rs + 4) * 2 ^ (length (<aa # list>) - Suc 0)

   757   = bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # <list @ [0]>) + rs * (2 * 2 ^ (aa + length (<list @ [0]>)))"

   758 apply(case_tac "list", simp add: add_mult_distrib, simp)

   759 apply(simp add: tape_of_nl_cons_app2 add_mult_distrib)

   760 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

   761 done

   762   

   763 lemma tape_of_nl_app_Suc: "((<list @ [Suc ab]>)) = (<list @ [ab]>) @ [Oc]"

   764 apply(induct list)

   765 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps exp_ind)

   766 apply(case_tac list)

   767 apply(simp_all add:tape_of_nl_abv tape_of_nat_list.simps exp_ind)

   768 done

   769 

   770 lemma [simp]: "bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]> @ [Oc])

   771               = bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>) +

   772               2^(length (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>))"

   773 apply(simp add: bin_wc_eq)

   774 apply(simp add: bl2nat_cons_oc bl2wc.simps)

   775 using bl2nat_cons_oc[of "Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>"]

   776 apply(simp)

   777 done

   778 lemma [simp]: "bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>) + (4 * 2 ^ (aa + length (<list @ [ab]>)) +

   779          4 * (rs * 2 ^ (aa + length (<list @ [ab]>)))) =

   780        bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [Suc ab]>) +

   781          rs * (2 * 2 ^ (aa + length (<list @ [Suc ab]>)))"

   782 apply(simp add: tape_of_nl_app_Suc)

   783 done

   784 

   785 declare tape_of_nat[simp del]

   786 

   787 fun wcode_double_case_inv :: "nat \<Rightarrow> bin_inv_t"

   788   where

   789   "wcode_double_case_inv st ires rs (l, r) = 

   790           (if st = Suc 0 then wcode_on_left_moving_1 ires rs (l, r)

   791           else if st = Suc (Suc 0) then wcode_on_checking_1 ires rs (l, r)

   792           else if st = 3 then wcode_erase1 ires rs (l, r)

   793           else if st = 4 then wcode_on_right_moving_1 ires rs (l, r)

   794           else if st = 5 then wcode_goon_right_moving_1 ires rs (l, r)

   795           else if st = 6 then wcode_backto_standard_pos ires rs (l, r)

   796           else if st = 13 then wcode_before_double ires rs (l, r)

   797           else False)"

   798 

   799 declare wcode_double_case_inv.simps[simp del]

   800 

   801 fun wcode_double_case_state :: "t_conf \<Rightarrow> nat"

   802   where

   803   "wcode_double_case_state (st, l, r) = 

   804    13 - st"

   805 

   806 fun wcode_double_case_step :: "t_conf \<Rightarrow> nat"

   807   where

   808   "wcode_double_case_step (st, l, r) = 

   809       (if st = Suc 0 then (length l)

   810       else if st = Suc (Suc 0) then (length r)

   811       else if st = 3 then 

   812                  if hd r = Oc then 1 else 0

   813       else if st = 4 then (length r)

   814       else if st = 5 then (length r)

   815       else if st = 6 then (length l)

   816       else 0)"

   817 

   818 fun wcode_double_case_measure :: "t_conf \<Rightarrow> nat \<times> nat"

   819   where

   820   "wcode_double_case_measure (st, l, r) = 

   821      (wcode_double_case_state (st, l, r), 

   822       wcode_double_case_step (st, l, r))"

   823 

   824 definition wcode_double_case_le :: "(t_conf \<times> t_conf) set"

   825   where "wcode_double_case_le \<equiv> (inv_image lex_pair wcode_double_case_measure)"

   826 

   827 lemma [intro]: "wf lex_pair"

   828 by(auto intro:wf_lex_prod simp:lex_pair_def)

   829 

   830 lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"

   831 by(auto intro:wf_inv_image simp: wcode_double_case_le_def )

   832 term fetch

   833 

   834 lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"

   835 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   836                 fetch.simps nth_of.simps)

   837 done

   838 

   839 lemma [simp]: "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))"

   840 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   841                 fetch.simps nth_of.simps)

   842 done

   843 

   844 lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)"

   845 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   846                 fetch.simps nth_of.simps)

   847 done

   848 

   849 lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)"

   850 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   851                 fetch.simps nth_of.simps)

   852 done 

   853 

   854 lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)"

   855 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   856                 fetch.simps nth_of.simps)

   857 done

   858 

   859 lemma [simp]: "fetch t_wcode_main 4 Bk = (R, 4)"

   860 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   861                 fetch.simps nth_of.simps)

   862 done

   863 

   864 lemma [simp]: "fetch t_wcode_main 4 Oc = (R, 5)"

   865 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   866                 fetch.simps nth_of.simps)

   867 done

   868 

   869 lemma [simp]: "fetch t_wcode_main 5 Oc = (R, 5)"

   870 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   871                 fetch.simps nth_of.simps)

   872 done

   873 

   874 lemma [simp]: "fetch t_wcode_main 5 Bk = (W1, 6)"

   875 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   876                 fetch.simps nth_of.simps)

   877 done

   878 

   879 lemma [simp]: "fetch t_wcode_main 6 Bk = (R, 13)"

   880 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   881                 fetch.simps nth_of.simps)

   882 done

   883 

   884 lemma [simp]: "fetch t_wcode_main 6 Oc = (L, 6)"

   885 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   886                 fetch.simps nth_of.simps)

   887 done

   888 lemma [elim]: "Bk\<^bsup>mr\<^esup> = [] \<Longrightarrow> mr = 0"

   889 apply(case_tac mr, auto simp: exponent_def)

   890 done

   891 

   892 lemma [simp]: "wcode_on_left_moving_1 ires rs (b, []) = False"

   893 apply(simp add: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps

   894                 wcode_on_left_moving_1_O.simps, auto)

   895 done

   896 

   897 

   898 declare wcode_on_checking_1.simps[simp del]

   899 

   900 lemmas wcode_double_case_inv_simps = 

   901   wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps

   902   wcode_on_left_moving_1_B.simps wcode_on_checking_1.simps

   903   wcode_erase1.simps wcode_on_right_moving_1.simps

   904   wcode_goon_right_moving_1.simps wcode_backto_standard_pos.simps

   905 

   906 

   907 lemma [simp]: "wcode_on_left_moving_1 ires rs (b, r) \<Longrightarrow> b \<noteq> []"

   908 apply(simp add: wcode_double_case_inv_simps, auto)

   909 done

   910 

   911 

   912 lemma [elim]: "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Bk # list);

   913                 tl b = aa \<and> hd b # Bk # list = ba\<rbrakk> \<Longrightarrow> 

   914                wcode_on_left_moving_1 ires rs (aa, ba)"

   915 apply(simp only: wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps

   916                 wcode_on_left_moving_1_B.simps)

   917 apply(erule_tac disjE)

   918 apply(erule_tac exE)+

   919 apply(case_tac ml, simp)

   920 apply(rule_tac x = "mr - Suc (Suc 0)" in exI, rule_tac x = rn in exI)

   921 apply(case_tac mr, simp, case_tac nat, simp, simp add: exp_ind)

   922 apply(rule_tac disjI1)

   923 apply(rule_tac x = nat in exI, rule_tac x = "Suc mr" in exI, rule_tac x = rn in exI, 

   924       simp add: exp_ind_def)

   925 apply(erule_tac exE)+

   926 apply(simp)

   927 done

   928 

   929 

   930 lemma [elim]: 

   931   "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Oc # list); tl b = aa \<and> hd b # Oc # list = ba\<rbrakk> 

   932     \<Longrightarrow> wcode_on_checking_1 ires rs (aa, ba)"

   933 apply(simp only: wcode_double_case_inv_simps)

   934 apply(erule_tac disjE)

   935 apply(erule_tac [!] exE)+

   936 apply(case_tac mr, simp, simp add: exp_ind_def)

   937 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

   938 done

   939 

   940 

   941 lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False" 

   942 apply(auto simp: wcode_double_case_inv_simps)

   943 done         

   944  

   945 lemma [simp]: "wcode_on_checking_1 ires rs (b, Bk # list) = False"

   946 apply(auto simp: wcode_double_case_inv_simps)

   947 done         

   948   

   949 lemma [elim]: "\<lbrakk>wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \<and> list = ba\<rbrakk>

   950   \<Longrightarrow> wcode_erase1 ires rs (aa, ba)"

   951 apply(simp only: wcode_double_case_inv_simps)

   952 apply(erule_tac exE)+

   953 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

   954 done

   955 

   956 

   957 lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False"

   958 apply(simp add: wcode_double_case_inv_simps)

   959 done

   960 

   961 lemma [simp]: "wcode_on_checking_1 ires rs ([], Bk # list) = False"

   962 apply(simp add: wcode_double_case_inv_simps)

   963 done

   964 

   965 lemma [simp]: "wcode_erase1 ires rs (b, []) = False"

   966 apply(simp add: wcode_double_case_inv_simps)

   967 done

   968 

   969 lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"

   970 apply(simp add: wcode_double_case_inv_simps exp_ind_def)

   971 done

   972 

   973 lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"

   974 apply(simp add: wcode_double_case_inv_simps exp_ind_def)

   975 done

   976 

   977 lemma [elim]: "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Bk # ba);  Bk # b = aa \<and> list = b\<rbrakk> \<Longrightarrow> 

   978   wcode_on_right_moving_1 ires rs (aa, ba)"

   979 apply(simp only: wcode_double_case_inv_simps)

   980 apply(erule_tac exE)+

   981 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - Suc 0" in exI,

   982       rule_tac x = rn in exI)

   983 apply(simp add: exp_ind_def)

   984 apply(case_tac mr, simp, simp add: exp_ind_def)

   985 done

   986 

   987 lemma [elim]: 

   988   "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \<and> list = ba\<rbrakk> 

   989   \<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"

   990 apply(simp only: wcode_double_case_inv_simps)

   991 apply(erule_tac exE)+

   992 apply(rule_tac x = "Suc 0" in exI, rule_tac x = "rs" in exI,

   993       rule_tac x = "ml - Suc (Suc 0)" in exI, rule_tac x = rn in exI)

   994 apply(case_tac mr, simp_all add: exp_ind_def)

   995 apply(case_tac ml, simp, case_tac nat, simp, simp)

   996 apply(simp add: exp_ind_def)

   997 done

   998 

   999 lemma [simp]: 

  1000   "wcode_on_right_moving_1 ires rs (b, []) \<Longrightarrow> False"

  1001 apply(simp add: wcode_double_case_inv_simps exponent_def)

  1002 done

  1003 

  1004 lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba; c = Bk # ba\<rbrakk> 

  1005   \<Longrightarrow> wcode_on_right_moving_1 ires rs (aa, ba)"

  1006 apply(simp only: wcode_double_case_inv_simps)

  1007 apply(erule_tac exE)+

  1008 apply(rule_tac x = "Suc 0" in exI, rule_tac x = "Suc (Suc ln)" in exI, 

  1009       rule_tac x = rn in exI, simp add: exp_ind)

  1010 done

  1011 

  1012 lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (aa, Oc # list);  b = aa \<and> Bk # list = ba\<rbrakk> \<Longrightarrow> 

  1013   wcode_erase1 ires rs (aa, ba)"

  1014 apply(simp only: wcode_double_case_inv_simps)

  1015 apply(erule_tac exE)+

  1016 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, auto)

  1017 done

  1018 

  1019 lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, []); b = aa \<and> [Oc] = ba\<rbrakk> 

  1020               \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"

  1021 apply(simp only: wcode_double_case_inv_simps)

  1022 apply(erule_tac exE)+

  1023 apply(rule_tac disjI2)

  1024 apply(simp only:wcode_backto_standard_pos_O.simps)

  1025 apply(rule_tac x = ml in exI, rule_tac x = "Suc 0" in exI, rule_tac x = ln in exI,

  1026       rule_tac x = rn in exI, simp)

  1027 apply(case_tac mr, simp_all add: exponent_def)

  1028 done

  1029 

  1030 lemma [elim]: 

  1031   "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, Bk # list);  b = aa \<and> Oc # list = ba\<rbrakk>

  1032   \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"

  1033 apply(simp only: wcode_double_case_inv_simps)

  1034 apply(erule_tac exE)+

  1035 apply(rule_tac disjI2)

  1036 apply(simp only:wcode_backto_standard_pos_O.simps)

  1037 apply(rule_tac x = ml in exI, rule_tac x = "Suc 0" in exI, rule_tac x = ln in exI,

  1038       rule_tac x = "rn - Suc 0" in exI, simp)

  1039 apply(case_tac mr, simp, case_tac rn, simp, simp_all add: exp_ind_def)

  1040 done

  1041 

  1042 lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (b, Oc # ba);  Oc # b = aa \<and> list = ba\<rbrakk> 

  1043   \<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"

  1044 apply(simp only: wcode_double_case_inv_simps)

  1045 apply(erule_tac exE)+

  1046 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - Suc 0" in exI, 

  1047       rule_tac x = ln in exI, rule_tac x = rn in exI)

  1048 apply(simp add: exp_ind_def)

  1049 apply(case_tac mr, simp, case_tac rn, simp_all add: exp_ind_def)

  1050 done

  1051 

  1052 lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, []);  Bk # b = aa\<rbrakk> \<Longrightarrow> False"

  1053 apply(auto simp: wcode_double_case_inv_simps wcode_backto_standard_pos_O.simps

  1054                  wcode_backto_standard_pos_B.simps)

  1055 apply(case_tac mr, simp_all add: exp_ind_def)

  1056 done

  1057 

  1058 lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba\<rbrakk> 

  1059   \<Longrightarrow> wcode_before_double ires rs (aa, ba)"

  1060 apply(simp only: wcode_double_case_inv_simps wcode_backto_standard_pos_B.simps

  1061                  wcode_backto_standard_pos_O.simps wcode_before_double.simps)

  1062 apply(erule_tac disjE)

  1063 apply(erule_tac exE)+

  1064 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

  1065 apply(auto)

  1066 apply(case_tac [!] mr, simp_all add: exp_ind_def)

  1067 done

  1068 

  1069 lemma [simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False"

  1070 apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps

  1071                  wcode_backto_standard_pos_O.simps)

  1072 done

  1073 

  1074 lemma [simp]: "wcode_backto_standard_pos ires rs (b, []) = False"

  1075 apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps

  1076                  wcode_backto_standard_pos_O.simps)

  1077 apply(case_tac mr, simp, simp add: exp_ind_def)

  1078 done

  1079 

  1080 lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list =  ba\<rbrakk>

  1081        \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"

  1082 apply(simp only:  wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps

  1083                  wcode_backto_standard_pos_O.simps)

  1084 apply(erule_tac disjE)

  1085 apply(simp)

  1086 apply(erule_tac exE)+

  1087 apply(case_tac ml, simp)

  1088 apply(rule_tac disjI1, rule_tac conjI)

  1089 apply(rule_tac x = ln  in exI, simp, rule_tac x = rn in exI, simp)

  1090 apply(rule_tac disjI2)

  1091 apply(rule_tac x = nat in exI, rule_tac x = "Suc mr" in exI, rule_tac x = ln in exI, 

  1092       rule_tac x = rn in exI, simp)

  1093 apply(simp add: exp_ind_def)

  1094 done

  1095 

  1096 declare new_tape.simps[simp del] nth_of.simps[simp del] fetch.simps[simp del]

  1097 lemma wcode_double_case_first_correctness:

  1098   "let P = (\<lambda> (st, l, r). st = 13) in 

  1099        let Q = (\<lambda> (st, l, r). wcode_double_case_inv st ires rs (l, r)) in 

  1100        let f = (\<lambda> stp. steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main stp) in

  1101        \<exists> n .P (f n) \<and> Q (f (n::nat))"

  1102 proof -

  1103   let ?P = "(\<lambda> (st, l, r). st = 13)"

  1104   let ?Q = "(\<lambda> (st, l, r). wcode_double_case_inv st ires rs (l, r))"

  1105   let ?f = "(\<lambda> stp. steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main stp)"

  1106   have "\<exists> n. ?P (?f n) \<and> ?Q (?f (n::nat))"

  1107   proof(rule_tac halt_lemma2)

  1108     show "wf wcode_double_case_le"

  1109       by auto

  1110   next

  1111     show "\<forall> na. \<not> ?P (?f na) \<and> ?Q (?f na) \<longrightarrow>

  1112                    ?Q (?f (Suc na)) \<and> (?f (Suc na), ?f na) \<in> wcode_double_case_le"

  1113     proof(rule_tac allI, case_tac "?f na", simp add: tstep_red)

  1114       fix na a b c

  1115       show "a \<noteq> 13 \<and> wcode_double_case_inv a ires rs (b, c) \<longrightarrow>

  1116                (case tstep (a, b, c) t_wcode_main of (st, x) \<Rightarrow> 

  1117                    wcode_double_case_inv st ires rs x) \<and> 

  1118                 (tstep (a, b, c) t_wcode_main, a, b, c) \<in> wcode_double_case_le"

  1119         apply(rule_tac impI, simp add: wcode_double_case_inv.simps)

  1120         apply(auto split: if_splits simp: tstep.simps, 

  1121               case_tac [!] c, simp_all, case_tac [!] "(c::block list)!0")

  1122         apply(simp_all add: new_tape.simps wcode_double_case_inv.simps wcode_double_case_le_def

  1123                                         lex_pair_def)

  1124         apply(auto split: if_splits)

  1125         done

  1126     qed

  1127   next

  1128     show "?Q (?f 0)"

  1129       apply(simp add: steps.simps wcode_double_case_inv.simps 

  1130                                   wcode_on_left_moving_1.simps

  1131                                   wcode_on_left_moving_1_B.simps)

  1132       apply(rule_tac disjI1)

  1133       apply(rule_tac x = "Suc m" in exI, simp add: exp_ind_def)

  1134       apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def)

  1135       apply(auto)