\documentclass[12pt,twoside]{article}
\renewcommand{\baselinestretch}{1}
\setcounter{page}{1}
\setlength{\textheight}{21.6cm}
\setlength{\textwidth}{14cm}
\setlength{\oddsidemargin}{1cm}
\setlength{\evensidemargin}{1cm}
\pagestyle{myheadings}
\thispagestyle{empty}
\markboth{\small{John Nixon}}{\small{Developments in the analysis technique for non-terminating Turing Machines}}
%\date{2017-02-21}
\usepackage{caption}
\usepackage{verbatim} %allows some sections to be temporarily commented out, which was %useful for correcting compilation errors that caused a problem with the long captions in two
%tables (search for 'comment' to find them)
\usepackage{enumitem}
\usepackage{amssymb}
\usepackage{longtable}
\usepackage{float}
\usepackage{subfigure}
\usepackage{multirow}
\usepackage{bigstrut}
\usepackage{bigdelim}
%\usepackage{cmll}
\usepackage{pifont}
\usepackage[utf8]{inputenc}% add accented characters directly
\restylefloat{figure}
\restylefloat{table}
\usepackage{booktabs}
\usepackage{hyperref}%The inclusion of package hyperref converts all the references to equations etc. to internal links
\usepackage{array}
\usepackage{mathtools}% includes amsmath
\usepackage{amscd}
\usepackage{amsthm}
%\usepackage{MnSymbol}
\everymath{\mathtt{\xdef\tmp{\fam\the\fam\relax}\aftergroup\tmp}}
\everydisplay{\mathtt{\xdef\tmp{\fam\the\fam\relax}\aftergroup\tmp}}
\begin{document}
\setbox0\hbox{$x$}
\newcommand{\un}{\underline}
%\centerline{\bf Mathematica Aeterna, Vol. x, 201x, no. xx, xxx - xxx}%uncomment this in published version
Date: 2023-11-30
\centerline{}
\centerline{}
\centerline {\Large{\bf Turing Machines}}
\centerline{}
%\centerline{\bf {John Nixon}}
%\centerline{}
%\centerline{Brook Cottage}
%\centerline{The Forge, Ashburnham}
%\centerline{Battle, East Sussex}
%\centerline{TN33 9PH, U.K.}
%Email: John.h.nixon1@gmail.com
%Date: 2017-01-11
\newtheorem{Theorem}{\quad Theorem}[section]
\newtheorem{Definition}[Theorem]{\quad Definition}
\newtheorem{Corollary}[Theorem]{\quad Corollary}
\newtheorem{Lemma}[Theorem]{\quad Lemma}
\newtheorem{Example}[Theorem]{\quad Example}
\newtheorem{alg}[Theorem]{\quad Algorithm}
\newcounter{Hypothesis}
\newtheorem{hyp}[Hypothesis]{Hypothesis}
\begin{abstract}
Developments are here described in the analysis technique for non-terminating Turing Machines (TM's) that I described earlier. The main idea is the introduction of IRR patterns i.e. constraints satisfied by large sets of IRRs (Irreducible Regular Rules) and the logical relationships between them as a result of the general method for deriving IRR's from others described in my earlier paper. These logical relationships will be referred to as IGR's (IRR Generating Rules). IGR's have been reduced to their minimal form in a way analogous to the way in which regular rules were reduced to IRR's by taking out symbol strings that played no essential role. In the case of IGR's these symbol strings (actually pairs) will be referred to as context pairs. A new version of my computer program extending the previous analysis is described and is freely available that generates these IGR's up to a given length of IRR's that they generate. The results show repetition of the left hand halves (Left IGR's or LIGR's) of IGR's associated with different right hand halves. Because the LIGR's can be derived independently of the right hand halves of IGR's, this should be done separately and can be done using the currently known IRR's as previously described in my earlier papers. The LIGR's can be used to calculate all the IRR's of a TM. A procedure for the generation of all the LIGR's for a TM has been suggested and is expressed here by a detailed analysis of a TM though not yet as computer code.
\end{abstract}
{\bf Mathematics Subject Classification:} 68Q25 \\
{\bf Keywords:} Turing Machine (TM), Irreducible Regular Rule (IRR), IRR Generating Rule (IGR), LIGR (Left IGR).
\section{Introduction}
This document is a work in progress. As such it is incomplete and still has errors and omissions. When brought to a state where I cannot easily find any improvements it will form my next paper on Turing Machine analysis.
Section 2 is a quite dense summary of the previous methods that lays the foundations of the developments to be described in this paper.
Section 3 introduces IRR patterns (IRRP's) as sets of IGR's conforming to the pattern. They have some common symbols in the origin and the RHS of the IRR and allow for any LHS.
Section 4 introduces IGR's in terms of IRRP's and illustrates the fact that IRR's of any length can be derived from sequences of IGR's by a sequence of substitutions.
In Section 5 the detailed description of an IGR is given and proves the generation of IRR's from IGR's. A computer algorithm is described for generating them all for a TM and its results are shown for an example TM.
In Section 6 a necessary condition in the relation ``can be followed by" for IGR's is found. Further results are found for the set of IGR's that can follow a sequence of IGR's following each other (i.e. substituted into each other) hand calculation of which suggests a method for generating all of them for a TM thugh this appears practically impossible for the example TM beause of te large number of cases to be considered. In Section 7 left IGR's or LIGR's are introduced because in section 6 the LHS and RHS of an IGR can be developed independently. An algorithm is illustrated by example for finding all the LIGR's for a TM based on the above ideas and results.
A lot of material has been removed to 2017's
\href{http://www.bluesky-home.co.uk/2017_Turing_notes.pdf}{Notes on Turing Machines}. These notes are now mostly superseded, but there may be a little there that is of use.
Comments are welcome. Please send them to
john.h.nixon1@gmail.com
\begin{comment}
\section{Outline of a possible algorithm for TM analysis}
Looking at the many examples of IGR's here including those in the next section suggests the best practical method to analyse the TM is to repeatedly apply $F$ to results that generate the IRR(3).
A typical instance involves applying $F$ to IRRP X as follows:
\begin{alg}\label{algorithm9.1}[Algorithm for applying $F$ to an IRRP $X$] Repeat while $X$ has not already had $F$ applied to it \{Truncate $X$ by 1 symbol putting the context pair at the end of a sequence or list that starts empty\}. Apply $F$ to $X$ truncated to length 1 as in the examples above or to the last but one result of this loop by applying the last context pair in the list to each member of $X$ that is not extendable as its LHS as described in Table~\ref{Table3} and Section~\ref{section7}. Repeat this recursively, unless already done, for any member of $X$ that is not extendable using the next context pair. Repeat till all the context has been applied. If the result of applying $F$ is no new results, this terminates this branch of the calculation. The procedure branches whenever there is more than one $X$ that is of non-extendable type (case 4). The must be a separate pointer to the list of contexts for each branch.
The intermediate results of this procedure may not be needed in the final analysis. They should be marked as such so that $F$ will not be applied to them at the next stage to generate IGR's for determining the $IRR({\it n})$.
\end{alg}
\begin{Theorem}Algorithm~\ref{algorithm9.1} applied to an IRRP $X$ generates all the IGRs that define all the results of the application of $F$ to $X$ as described in Section~\ref{section4}.
\end{Theorem}
\begin{proof}
(Sketch) This is obvious because truncating $X$ truncates both the forward computation and backward search to that length and these calculations must be included in the full calculation for the original $X$. Therefore adding back the effect of the symbols truncated off systematically so that no options are forgotten must give the same result. This holds separately for each individual backward search path and forward computation possible.
\end{proof}
Note that in this algorithm it is the non-extendable IRRP's on the RHS that can have extra contexts applied to generate new IGR members. If the IRRP's of the right are extendable they can have $F$ applied using a new $\alpha$ to generate new IGR members.
Repeat this starting with each IRRP generated from the TM until $F$ has been applied to every IRRP generated. All the IGR's so obtained must be recorded including those that lead to no new IRRP's.
This may terminate because the final result is the IGR used to extend $X$ which can often be expected to be much shorter than $X$. See the example in Section~\ref{section4}. I will shortly try to construct a computer program to do this and check against the results obtained so far.
A result of the analysis for a TM will be that each IRRP has associated with it a set of pairs of context strings that generate the IRR's it corresponds to.
\end{comment}
\section{\label{sec2}Basic definitions and summary of the existing method to generate the IRR's for a TM}
A configuration set (CS) for a TM is a set of complete configurations (tape symbols with pointer position indicated, and the machine state of the TM) such that the CS is specified by giving a finite set of symbols in a set of contiguous pointer positions together with the machine state and such that the pointer position is where one of the given symbols is given or adjacent to one. In a CS all possible configurations that are consistent with the specified symbols and machine state are included. The notation is the specified symbol string with the pointer indicated by an underscore (it is just off the end of the symbol string) or an underline and the machine state on the left. For example with machine states 1,2,3, etc. and symbols lower case letters the following are CSs: $2a\un{b}ca$, $1\_aabbcac$. The length of the CS is the length of the symbol string which is finite.
A computation rule or rule is a pair of CS's linked by $\to$ indicating the forward direction of the computation. A reducible rule is one that has symbols that play no part in the computation i.e. any extra symbols added on the left or right of the strings at the left and right hand sides of a computation rule. From the definitions of regular rules (RR) and irreducible regular rules (IRR) in \cite{jhn2013},
any computation of the TM that ends with the pointer just off the end (i.e. adjacent to a symbol at the end) of the string of symbols specified at the start can be represented by RR's chained together as a sequence of CS's starting with one of length 1, where for each step in the chain a new symbol is read at a position where no symbol has yet been read at the pointer, thus the length of the string of symbols increases by 1 for each RR unless a stationary cycle occurs that ends such a sequence. All such CS's are by definition reachable. All single TM steps are RR's. If the RR is of type LR or RL as designated earlier (now the position of the pointer in the origin (see below) is included so these are now RLR and LRL respectively) the pointer swaps ends at that step of the chain and these RR's are also irreducible RR's (IRR's) because if the pointer swaps ends there are no redundant symbols i.e. the rule is irreducible. There are also IRR's that that don't swap ends.
If a CS called ``origin" is included with the LHS and RHS of the IRR it can be written in the triplet form as $origin\to LHS\to RHS$ for which the abbeviated form $origin\to\to RHS$ will be used if the LHS is not specified hence the changed designation of the type of an IRR. An origin (there could be many for the same LHS) of an IRR is a CS obtained by running the TM backwards starting from the LHS to a point such that the pointer position is at the opposite end of the string from where it is in the LHS.
If an RR is of type LRR or RLL it is related to an irreducible form (a possibly shorter IRR which only involves the symbols passed by the pointer during its execution) as follows.
Suppose the RR is represented by
$m\to n\to o$ where ${\it m}<{\it n}<{\it o}$ and ${\it n}+{\rm 1}={\it o}$ where italics represent the corresponding pointer positions for the CS's in typewriter font. Then the RR has type LRR because the start and end points of the i.e. the LHS and RHS have the pointer at the right hand end of the string. The rule $n\to o$ can be represented as $n'\to p'\to o'$ without any redundant symbols where ${\it m}\le {\it p}\le{\it n}<{\it o}$ and the primes indicate shortening of the strings by deleting the symbols below position {\it p} i.e. {\it p} is the leftmost pointer position in the computation from $n$ to $o$. ${\it n}={\it p}$ holds if and only if $n'=p'$ and $n'\to o'$ is a single TM step. If ${\it n}\ne {\it p}$ the rule $n'\to p'$ shows that $p'$ is reachable therefore $n'\to p'\to o'$ represents an IRR of type RLR, and of course the mirror image result applies to IRR's of type RLL.
In general let $X$ be a member of IRR({\em n}) i.e. the set of all IRR's with CS's of length ${\it n}$. Then $X$ can be represented as $A\to B\to C$ where the pointer swaps ends between $A$ and $B$ (thus this is either $1\to n$ or $n\to 1$ and is referred to as condition 1) to establish the reachability of $B$ necessary for $X$ to be an IRR. There may be more than one such CS $A$ for a single $B$ and the set of all such $A$ will be denoted by $O_1(B)$ (the same as $S(B)$ in \cite{jhn2017}), the 1 referring to the backward searching algorithm that terminates in condition 1 (see \cite{jhn2017} section 2.2). Likewise if it terminates in condition 2 i.e. the pointer comes back to where it was at the start of the backward search, the set of such endpoints will be denoted as $O_2(B)$, but these do not confer reachability and will not be referred to as origins. If the pointer is at the right in $A$ and at the left in $B$ then at $C$ it can be at the left or right so that $X$ must be represented as either of the triplet forms $n\to 1\to 0$ or $n\to 1\to n+1$ and having types RLL and RLR respectively. Likewise if the pointer is at the left in $A$ (the mirror image forms), $X$ must be represented by either of $1\to n\to n+1$ or $1\to n\to 0$, having types LRR and LRL respectively.
If $B$ is reachable but forward computaton from it leads to a CS that has arisen before in this computation, this is an stationary cycle and the type of the IRR is then of type LC or RC. If the reverse computation path from $B$ leads to a stationary cycle, then this cycle must include $B$ to avoid a branch point in the forward computation that would not then be unique. Thus likewise the IRR is of type LC or RC.
From the definition of RR in the first paragraph of this section, if in the backward search from the LHS of an IRR, the pointer again reaches the same position it had in the LHS (condition 2), however much further back the backward search were to continue, it would not be possible from this alone to show that this LHS is indeed the LHS of an IRR. This is because if the computation is again run forward, this LHS has the pointer at the same point as a previous CS and is therefore not shown to be one of the list of CS's playing the special role in the above definition,
though it could possibly be shown to be one as a result of another backward search path. This is the justification of the terminating condition 2 in the backward search algorithm. See \cite{jhn2017} page 30.
This proves that
\begin{Lemma}\label{lemma1} The triplets $1\to n\to 0$, $1\to n\to n+1$, and $n\to 1\to n+1$, and $n\to 1\to 0$ representing TM computations each form an IRR {\em (}type LRL, LRR, RLR or RLL respectively{\em )} if and only if the origin indicated {\em (}the first member{\em )} is the first CS arrived at with the pointer in that position after tracing the computation back from the LHS {\em (}the middle member{\em )} and the the pointer does not occur again in the position it had in the LHS in the reverse computation path from the LHS i.e there is no other CS $1$ or $n$ between the $1$ and the $n$ in the triplet forms above. Furthermore any IRR of length {\em n} of one of the types RLL, RLR, LRL, LRR has one of these forms.\end{Lemma}
Generating all the IRR's based on Theorem 9.1 of \cite{jhn2013} starts with all single TM steps in the above notation $1\to 0$ (i.e. $\un{x}\to \_x$) or $1\to 2$ (i.e.
$\un{x}\to x\_$) where $x$'s represents an arbitrary symbol that could be different for each use. Every possible single symbol (called $\alpha$) is added at the pointer position in each RHS, and in each case the computaton is taken as far as possible to get the new RHS unless a stationary cycle occurs. The resulting rule $LHS\to RHS$ is an IRR if it irreducible i.e. connot be expressed with shorter strings of symbols. In the first case, adding $\alpha$ on the left and continuing the computation as far as possible gives results either of the form (i) $2\to 1\to 3$ or (ii) $2\to 1\to 0$ i.e. $\alpha\un{x}\to\un{\alpha}x\to xx\_\text{ or }\_xx$ respectively unless a stationary cycle is obtained. The results in case (i) are IRR's by Lemma~\ref{lemma1} because there can be no other CS's between the $2$ and the $1$ which is a single TM step. The results from (ii) are IRR's if and only if the first move beyond the $1$ is to $2$ i.e. the computation has the form $2\to 1\to 2 \to 0$ because this ensures that the rule $1\to 0$ contained in (ii) of length 2 is irreducible. Likewise for the mirror image case starting with a rule of the form $1\to 2$ adding the $\alpha$ on the right and continuing gives results of the form $1\to 2\to 0$ ($\in \text{IRR}(2)$) or of the form $1\to 2\to 3$ ($\in\text{IRR}(2)$ if and only if the first move from the $2$ is to $1$).
Consider extending this to the general case of generating all the IRR $Y$ of length ${\it n}+{\rm 1}$ based on the single IRR $X$ of length ${\it n}\ge {\rm 2}$ and having the form $n\to 1\to n+1$, which can be also be written as $A\to\ B\to C$ for some CS's $A$,$B$, and $C$. First the computation $A\alpha\to B\alpha\to C\alpha$ holds where $\alpha$ is any symbol the TM uses. Clearly by Theorems 5.4 and 9.1 of \cite{jhn2013} every such IRR $Y$ can be obtained starting from the LHS $B\alpha$ if an appropriate $\alpha$ can be found. The symbol $\alpha$ must be chosen so that $B\alpha$ is reachable i.e. $O_1(B\alpha)\ne\emptyset$. These are all the terminal CS's of length ${\it n}+{\rm 1}$ from the backward searching algorithm starting from $B\alpha$ and ending in condition (1). Each of these branches has a point where the pointer first reaches $n$ and this CS is $A\alpha$ because the $\alpha$ has yet played no part, so $O_1(B\alpha)=O_1(A\alpha)$, thus the backward search algorithm is applied to $A\alpha$, and identifying all possible values of $\alpha$ i.e. the values of $\alpha$ for which $O_1(A\alpha)\ne\emptyset$ by generating all its origins for each such $\alpha$. Also the forward computation from $C\alpha$ is continued as far as possible to generate the RHS of $Y$ and hence what its type is (LRR, LRL, RLR, RLL, LRC, or RLC) the last two cases coming from a stationary cycle in the forward computation from $C\alpha$.
If the pointer is at the left in $A$ and $C$ and the right in $B$ (the mirror image case) the added arbitrary symbol $\alpha$ will be on the left. This procedure for generating the all the IRR $Y$ of length {\em n}$+1$ like this from an IRR $X$ of length {\em n}, including the mirror image case where the triplet form of $X$ is $1\to n\to 0$, will denoted by the function $F$. $F$ applied to an IRR of type LC or RC is the empty set. This proves that
\begin{Theorem}\label{irr_ind_thm} Every member of IRR{\em (}${\it n}+{\rm 1}${\em )} can be obtained using $F$ from some $X\in\text{IRR}${\em (}n{\em )} of type RLR or LRL for ${\it n}\ge {\rm 2}$. Also, because forward computation is unique e.g. the RHS of an IRR is uniquely determined by is LHS, but the origins may be more than one, the sets of IRR obtained like this for different $X$ {\em (}different $B${\em )} must be disjoint i.e. $F^{-1}$ applied to a member of IRR{\em (}${\it n}+{\rm 1}${\em )} is a unique member of IRR{\em (}n{\em )}. The first part can be written symbolically as
\begin{equation}\label{irr_ind}\text{IRR}({\it n}+{\rm 1})=\bigcup _{X\in IRR({\it n})}\{ F(X)\}\end{equation}
\end{Theorem}
The following is the general outline showing an IRR triplet of length {\em n} of type RLR (type RLR with origin having the pointer at the right) and the possible types of result (except the cases where a stationary cycle occurs) of this argument for a given symbol $\alpha$ that could include a new IRR triplet of length ${\it n}+{\rm 1}$.
\begin{equation}\label{irr_deriv1}\arraycolsep=5pt
\left.\mkern-30mu\begin{array}{ccc}\left.\begin{array}{c}\text{Cannot be used to}\\\text{ prove reachability of } 1\end{array}\right\}&1&\to\\\text{Proves reachability of }1&n+1&\to\end{array}\right\}n\to 1\to n+1\left\{\begin{array}{ccc}\to &0&\text{type RLL}\\\to &n+2&\text{type RLR}\end{array}\right.
\end{equation}
The 3 central CS's refer to a member of IRR({\em n}), and the leftmost, central, and rightmost CS's refer to the corresponding member of IRR({\em n}$+1$) if reachability of the CS $1$ in the centre of \eqref{irr_deriv1} is found. The corresponding mirror image result for the LRL case is as follows:
\begin{equation}\label{irr_deriv2}\arraycolsep=4pt
\left.\mkern-30mu\begin{array}{ccc}\text{Proves reachability of }n+1&1&\to\\\left.\begin{array}{c}\text{Cannot be used to}\\\text{ prove reachability of }n+1\end{array}\right\}&n+1&\to\end{array}\right\}2\to n+1\to 1\left\{\begin{array}{ccc}\to &0&\text{type LRL}\\\to &n+2&\text{type LRR}\end{array}\right.
\end{equation}
In this case note that because the $\alpha$ is added on the left, all the pointer positions in the IRR of length {\em n} have been increased by 1 when they appear in the embedded IRR of length {\em n}, so originally they would have been $1\to n\to 0$.
The above procedure allows the generation of all the IRR of a TM up to any given length and has been implemented \cite{tie}.
\begin{comment}
While deriving an IRR triplet of the form $n+1\to 1\to n+2$ in the notation of \eqref{irr_deriv1} from one of the form $n\to 1\to n+1$ the pointer moves in the backward search in general thus: $n\leftarrow n-k\leftarrow n+1$ (i.e. equivalent to $k+1\leftarrow 1\leftarrow k+2$ or where $k+2$ is the first CS of the form arrived at.) where the CS $n+1$ is the first arrival at such a CS in the backward search because the $n+1$ would terminate the backward search algorithm. It could not reach point $1$ because that would also terminate the backward search algorithm. Therefore ${\rm 0}\le {\it k}\le {\it n}-{\rm 2}$. It is interesting to note that the backward search in general takes the form of an IRR triplet of length ${\it k}+{\rm 1}$ run in reverse by lemma~\ref{lemma1} where $1\le {\it k}+1\le {\it n}-\rm 1$ but crucially only if the direction of computation could be is reversed so this might have no significance.
\end{comment}
\section{\label{sec3}IRR patterns (IRRP's) and IGR's}
The derivation of IRR's from other ones (length ${\it n}$) following the procedure $F$ described above was found to often take the same form independent of ${\it n}$ provided ${\it n}$ is large enough. Then the obvious step is to describe these general results termed IRR generating rules (IGR's) so that they can be easily applied in any given case. These results have an LHS and an RHS and the existence of a member of IRR({\it n}) matching the LHS implies the existence of a corresponding member of IRR({\it n}+{\rm 1}) matching each of the parts of the RHS. Each of these parts and the LHS take the form of a generalised IRR in which the symbol $\alpha$ appears and two arbitrary strings, $T_1$ in the origin and $T_2$ in the RHS, and the LHS (middle member) is omitted so that any LHS is matched.
These general forms for the IRR's were termed IRR patterns (IRRP's).
The analysis techniques were applied to the following TM \eqref{1} which was generated randomly with 5 states and 5 symbols. This TM, being much larger than any that I have analysed before, has proved to be a much more challenging case.
\begin{equation}\label{1}
\begin{tabular}{lllll}
$1\un{a}\to 2\_d$&$2\un{a}\to 1c\_$&$3\un{a}\to 4c\_$&$4\un{a}\to 3\_b$&$5\un{a}\to 2\_e$\\
$1\un{b}\to 4\_d$&$2\un{b}\to 4\_c$&$3\un{b}\to 4\_c$&$4\un{b}\to 4b\_$&$5\un{b}\to 3\_e$\\
$1\un{c}\to 3\_a$&$2\un{c}\to 1d\_$&$3\un{c}\to 2\_a$&$4\un{c}\to 3c\_$&$5\un{c}\to 3a\_$\\
$1\un{d}\to 2b\_$&$2\un{d}\to 1a\_$&$3\un{d}\to 5\_c$&$4\un{d}\to 5\_c$&$5\un{d}\to 4\_a$\\
$1\un{e}\to 2b\_$&$2\un{e}\to 3\_c$&$3\un{e}\to 3b\_$&$4\un{e}\to 5a\_$&$5\un{e}\to 3a\_$\\
\end{tabular}
\end{equation}
\begin{comment}
IRR patterns (IRRP's) have been found to be very useful because they result in shortening of the lists of cases to be considered because sets of IRR's that match an IRRP often have similar derivations and can be dealt with together. For example in \eqref{irr_deriv1} (and similarly for \eqref{irr_deriv2}) that contains two derivations one of each of the forms $n+1\to n$ and $n+1\to n+2$, often involve one or a small number of TM steps and are indepedent of {\em n}. Also the treatment of IRR's in TM1 in \cite{jhn2017} where sets conforming to the IRRP's could be treated in the same way, allowed a proof of a general method for obtaining all the $IRR({\it n}+1)$ from the $IRR({\it n})$ for all sufficiently large {\em n} for this TM.
An IRRP is represented like an IRR but with $\ldots$ or $T_1$ and $T_2$ representing the arbitrary strings, because there are two of them in each IRRP that can be different but have the same length. The IRRP is the set of all results that would be obtained (they will be IRR's) by keeping the fixed values of the given symbols and making arbitrary substitutions for the arbitrary strings that can be any strings of symbols of arbitrary length including zero.
An IRRP may be regarded as an abbreviation of an IRR (1) to a fixed length {\em k} of the given strings of symbols, where the symbol at the pointer in the origin is at one end and (2) the original LHS (the middle element in the triplet form of an IRR) is removed completely. The abbreviation is indicated by $\ldots$ or $T_1$ and $T_2$ in place of the deleted symbols in the origin and the RHS. This presentation has the property that the pointer position appears separately in the RHS column if and only if the IRR is of extendable type i.e. type LRL or RLR, otherwise it appears as an underscore under the $T_2$ indicating that the pointer should be under the first symbol of $T_2$ i.e. adjacent to one of the given symbols.
Table~\ref{ind1} is presented in doubled two-column format just for convenience, and has logically just two columns, Origin and RHS's. It was obtained by abbreviating all the IRR(3) to length ${\it k}={\rm 2}$. For this purpose, IRR's with many origins have a separate entry for each origin. This allows the origins to be unique for each row in the table but multiple RHS's from different IRRP's often combined into the same row of Table~\ref{ind1}.
An effect of the information loss resulting from representing the IRR's by IRRP's i.e. the truncation of the string of symbols from length {\em n} to length {\em k} that is independent of {\em n}, is that it completely alters the simple description of how to analyse a Turing Machine provided by Theorem~\ref{irr_ind_thm}. This may be thought of as the trade-off for the advantages described above. How this is dealt with is complicated and not easy to describe and is a major theme of this paper.
\begin{longtable}{ll|ll}
\caption{List of patterns for the IRR(3)\label{ind1}}\\
Origin&RHS's&Origin&RHS's\\\hline
$1\un{d}d\ldots$&$4\_cb\ldots$&$5\un{e}e\ldots$&$\{3\_bc\ldots,3ca\ldots\}$\\
$1\un{e}d\ldots$&$4\_cb\ldots$&$3\un{e}e\ldots$&$\{4bc\ldots,4\_ce\ldots\}$\\
$1\un{d}d\ldots$&$4\_ca\ldots$&$4\un{e}c\ldots$&$\{3cb\ldots,1cb\ldots\}$\\
$1\un{e}d\ldots$&$4\_ca\ldots$&$4\un{e}e\ldots$&$\{3cb\ldots,1cb\ldots\}$\\
$1\un{d}a\ldots$&$4\_ca\ldots$&$4\un{c}e\ldots$&$\{1ab\ldots,2\_ae\ldots\}$\\
$1\un{e}a\ldots$&$4\_ca\ldots$&$3\ldots b\un{c}$&$\{4\ldots cc\_,1\ldots bc\_,4\ldots ac\_\}$\\
$1\un{d}c\ldots$&$3\_ec\ldots$&$1\ldots b\un{c}$&$\{4\ldots cc\_,1\ldots bc\_,4\ldots ac\_\}$\\
$1\un{e}c\ldots$&$3\_ec\ldots$&$4\ldots b\un{a}$&$\{2\ldots ab\_,3\ldots bc\_\}$\\
$1\ldots c\un{c}$&$1\ldots bc\_$&$2\ldots b\un{e}$&$\{2\ldots ab\_,1\ldots bd\_,2\ldots db\_\}$\\
$4\ldots c\un{a}$&$3\ldots bc\_$&$1\ldots b\un{a}$&$\{2\ldots db\_,1\ldots ba\_,1\ldots bd\_\}$\\
$2\ldots c\un{e}$&$1\ldots bd\_$&$5\ldots b\un{a}$&$\{3\ldots cb\_,3\ldots cc,3\ldots ab\_\}$\\
$5\ldots c\un{b}$&$\{5\ldots cc,3\ldots cc,1\ldots bd\_\}$&$5\ldots b\un{b}$&$\{3\ldots cb\_,3\ldots cc,3\ldots ab\_\}$\\
$3\ldots a\un{d}$&$1\ldots bd\_$&$4\un{b}b\ldots$&$\{2ba\ldots,4\_ce\ldots\}$\\
$4\ldots a\un{d}$&$1\ldots bd\_$&$3\un{a}b\ldots$&$\{3ab\ldots,2\_ae\ldots\}$\\
$2\un{d}d\ldots$&$3\_bc\ldots$&$5\un{c}a\ldots$&$3db\ldots$\\
$2\un{d}e\ldots$&$3\_bc\ldots$&$5\un{e}a\ldots$&$3db\ldots$\\
$2\un{a}d\ldots$&$1ab\ldots$&$3\un{e}a\ldots$&$4\_ca\ldots $\\
$2\un{a}e\ldots$&$1ab\ldots$&$4\un{c}a\ldots$&$3ab\ldots$\\
$2\un{c}d\ldots$&$5\_cc\ldots$&$1\ldots d\un{c}$&$1\ldots bc\_$\\
$2\un{c}e\ldots$&$5\_cc\ldots$&$4\ldots d\un{a}$&$3\ldots bc\_$\\
$5\ldots a\un{d}$&$\{3\ldots bc\_,4\ldots cc\_\}$&$2\ldots d\un{e}$&$1\ldots bd\_$\\
$2\ldots a\un{b}$&$\{3\ldots bc\_,2\ldots ab\_\}$&$5\ldots d\un{b}$&$5\ldots cc$\\
$3\ldots a\un{b}$&$\{3\ldots bc\_,2\ldots ab\_\}$&$5\ldots d\un{d}$&$1\ldots bc\_$\\
$1\ldots a\un{b}$&$\{2\ldots ec,2\ldots db\_\}$&$2\ldots d\un{b}$&$1\ldots bd\_$\\
$3\ldots e\un{c}$&$4\ldots cc\_$&$3\ldots d\un{b}$&$1\ldots bd\_$\\
$1\ldots e\un{a}$&$2\ldots db\_$&$1\ldots d\un{b}$&$1\ldots ba\_$\\
$5\ldots e\un{a}$&$3\ldots cb\_$&$4\un{b}e\ldots$&$4\_cb\ldots$\\
$3\ldots b\un{d}$&$\{3\ldots aa\_,4\ldots cc\_\}$&$3\un{a}e\ldots$&$2\_ab\ldots$\\
$4\ldots b\un{d}$&$\{3\ldots aa\_,4\ldots cc\_\}$&$3\ldots d\un{d}$&$\{3\ldots cc\_,1\ldots bd\_\}$\\
$5\un{c}e\ldots$&$\{3\_bc\ldots,3ca\ldots\}$&$4\ldots d\un{d}$&$\{3\ldots cc\_,1\ldots bd\_\}$\\
\end{longtable}
Treating Table~\ref{ind1} at first as a hypothesis to be proved by induction for IRR of length ${\it n}\ge 3$ suggests (1) following the method in Section~\ref{sec2} to each of the patterns provided they are extendable i.e. of type RLR or LRL, and then (2) truncating the result to two symbols from the pointer at the new origin so generating another result of the same form as those already in Table~\ref{ind1}. This must be repeated as necessary to ensure closure, i.e. every member of IRRP$({\it n}+{\rm 1})$ truncated to length ${\it k}={\rm 2}$ must also appear as a member of IRRP(${\it n}$) also truncated to length ${\it k}={\rm 2}$. This results in Table~\ref{irr_2r}. Thus an infinite number of IRR could be captured by the resulting recursive description. In these tables the lazy abbreviation is used where $\ldots$ represents any string of symbols of length $\ge 1$ that could be different whenever is used, but really it should be done with say $T_1$ and $T_2$ to represent the two arbitrary strings ($S_1$ and $S_2$ are used later so this notation avoids ambiguity).
Thus every application of $F$ as described in Section~\ref{sec2} maps an IRRP in Table~\ref{irr_2r} that has ${\it k}={\rm 2}$ to another IRRP in Table~\ref{irr_2r} unless the backward search procedure to find new origins goes in the unexpected direction i.e. away from the symbol $\alpha$. The analysis for these cases will be taken as far as possible giving results with ${\it k}={\rm 3}$. This issue is taken up again in Section~\ref{sec4}.
\begin{equation}\begin{array}{c}
1\un{a}\to 2b \_\\
1\un{b}\to 3\_b\\
1\un{c}\to 1b\_\\
2\un{a}\to 3b\_\\
2\un{b}\to 2c\_\\
2\un{c}\to 1\_c\\
3\un{a}\to 1\_a\\
3\un{b}\to 1\_a\\
3\un{c}\to 3c\_\\
\end{array}\end{equation}
\end{comment}
For example it is known that at least one IRR for this TM matches \begin{equation}\label{addalpha1}1\un{d}aT_1\to\to4\_caT_2.\end{equation} Using backward TM steps from \eqref{1} gives
\begin{equation}\label{addalpha2}\begin{tabular}{lccc}deriving the origin&old RHS&RHS&$\alpha$\\
$\alpha A$&$\alpha C$&&\\
$1\alpha\un{d}aT_1\left\{\begin{array}{l}
\stackrel{\alpha=a}{\leftarrow}2\un{d}daT_1\\
\stackrel{\alpha=c}{\leftarrow}2\un{a}daT_1\\
\stackrel{\alpha=d}{\leftarrow}2\un{c}daT_1\\
\end{array}\right.$&
$\begin{array}{l}4\un{a}caT_2\\4\un{c}caT_2\\4\un{d}caT_2\\\end{array}$&
$\begin{array}{l}3\_bcaT_2\\1abc\un{T_2}\\5\_ccaT_2\end{array}$&$\begin{array}{l}a\\c\\d\end{array}$
\end{tabular}\end{equation}
of which the result for $\alpha=c$ has an RHS given where the pointer is at the first symbol of $T_2$. The results of $F$ are written as follows
\begin{equation}\label{addalpha3}\begin{array}{l}2\un{d}daT_1\to\to 3\_bcaT_2\\
2\un{a}daT_1\to\to1abc\un{T_2}\\
2\un{c}daT_1\to\to 5\_ccaT_2\end{array}\end{equation} for $\alpha= a,c,d$ respectively, and the complete IGR can be written as
\begin{equation}1\un{d}aT_1\to\to 4\_caT_2\left\{\begin{array}{l}\stackrel{a}{\Rightarrow}2\un{d}daT_1\to\to 3\_bcaT_2\\
\stackrel{c}{\Rightarrow}2\un{a}daT_1\to\to1abc\un{T_2}\\
\stackrel{d}{\Rightarrow}2\un{c}daT_1\to\to 5\_ccaT_2\end{array}\right.\end{equation}
Note that in this argument, adding the arbitrary symbol $\alpha$ on the left (because the pointer in the origin is on the left) maintains the pointer being on the right hand end of the string of symbols in the LHS (not shown), and this property is implicit in an IRRP with the pointer at the left of the origin CS.
The result of this argument is that if an IRR of length ${\it n}$ conforms to \eqref{addalpha1}, then there are 3 more IRR's of length ${\it n}+{\rm 1}$ corresponding to \eqref{addalpha3} for $\alpha\in\{a,c,d\}$ respectively.
The second of these results in \eqref{addalpha3} has the pointer in the RHS on the right, so this IRR has type LRR and cannot be used to derive other IRR's. These are examples of rules that generate IRR's of length ${\it n}+{\rm 1}$ from other IRR's of length ${\it n}$. An IGR is defined as a logical implication having an IRRP on the left and sets of IRRP's on the right, one set for each value of $\alpha$ and the logical deduction follows the general procedure outlined in Theorem~\ref{irr_ind_thm}. Thus the strings with given symbols on the right of the implications are one symbol longer than those on the left.
\begin{comment}
\fontsize{10}{10}\selectfont
\begin{longtable}{c|l@{\hspace{0.5em}}l|c|l@{\hspace{0.5em}}l}
\caption{IRRP's of length {\it n} and their derived IRRP's of length ${\it n}+{\rm 1}$, with the unknown symbols on the right.\label{irr_2r}}\\
set&\multicolumn{2}{c|}{IRRP(${\it n}$)}&$\alpha$&\multicolumn{2}{c}{IRRP(${\it n}+1$)}\\
number&Origin&RHS&&Origin&RHS\\
\hline
$1$&$1\un{d}a\ldots$&$4\_ca\ldots$&$a$&$2\un{d}d\ldots$&$3\_bc\ldots$\\
&&&$c$&$2\un{a}d\ldots$&$1ab\ldots$\\
&&&$d$&$2\un{c}d\ldots$&$5\_cc\ldots$\\\hline
$2$&$1\un{d}c\ldots$&$3\_ec\ldots$&$a$&$2\un{d}d\ldots$&$3ca\ldots$\\
&&&$c$&$2\un{a}d\ldots$&$2\_ae\ldots$\\
&&&$d$&$2\un{c}d\ldots$&$5\_ce\ldots$\\\hline
$3$&$1\un{d}d\ldots$&$4\_ca\ldots$&$a$&$2\un{d}d\ldots$&$3\_bc\ldots$\\
&&&$c$&$2\un{a}d\ldots$&$1ab\ldots$\\
&&&$d$&$2\un{c}d\ldots$&$5\_cc\ldots$\\\hline
$4$&$1\un{d}d\ldots$&$4\_cb\ldots$&$a$&$2\un{d}d\ldots$&$3\_bc\ldots$\\
&&&$c$&$2\un{a}d\ldots$&$3ab\ldots$\\
&&&$d$&$2\un{c}d\ldots$&$5\_cc\ldots$\\\hline
$5$&$1\un{e}a\ldots$&$4\_ca\ldots$&$a$&$2\un{d}e\ldots$&$3\_bc\ldots$\\
&&&$c$&$2\un{a}e\ldots$&$1ab\ldots$\\
&&&$d$&$2\un{c}e\ldots$&$5\_cc\ldots$\\\hline
$6$&$1\un{e}c\ldots$&$3\_ec\ldots$&$a$&$2\un{d}e\ldots$&$3ca\ldots$\\
&&&$c$&$2\un{a}e\ldots$&$2\_ae\ldots$\\
&&&$d$&$2\un{c}e\ldots$&$5\_ce\ldots$\\\hline
$7$&$1\un{e}d\ldots$&$4\_ca\ldots$&$a$&$2\un{d}e\ldots$&$3\_bc\ldots$\\
&&&$c$&$2\un{a}e\ldots$&$1ab\ldots$\\
&&&$d$&$2\un{c}e\ldots$&$5\_cc\ldots$\\\hline
$8$&$1\un{e}d\ldots$&$4\_cb\ldots$&$a$&$2\un{d}e\ldots$&$3\_bc\ldots$\\
&&&$c$&$2\un{a}e\ldots$&$3ab\ldots$\\
&&&$d$&$2\un{c}e\ldots$&$5\_cc\ldots$\\\hline
$9$&$2\un{a}d\ldots$&$2\_ae\ldots$&$b$&$1\un{d}a\ldots$&$4\_ca\ldots$\\
&&&$b$&$1\un{e}a\ldots$&$4\_ca\ldots$\\
&&&$\alpha$&$1\alpha a\un{a}\ldots$&$RHS$\\ \hline
$10$&$2\un{a}d\ldots$&$1ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$11$&$2\un{a}d\ldots$&$3ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$12$&$2\un{a}e\ldots$&$2\_ae\ldots$&$b$&$1\un{d}a\ldots$&$4\_ca\ldots$\\
&&&$b$&$1\un{e}a\ldots$&$4\_ca\ldots$\\
&&&$\alpha$&$5\alpha a \un{a}\ldots$&$RHS$\\\hline
$13$&$2\un{a}e\ldots$&$1ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$14$&$2\un{a}e\ldots$&$3ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$15$&$2\un{c}d\ldots$&$5\_cc\ldots$&$b$&$1\un{d}c\ldots$&$3\_ec\ldots$\\
&&&$b$&$1\un{e}c\ldots$&$3\_ec\ldots$\\
&&&$\alpha$&$1\alpha c\un{a}\ldots$&$RHS$\\\hline
$16$&$2\un{c}d\ldots$&$5\_ce\ldots$&$b$&$1\un{d}c\ldots$&$3\_ec\ldots$\\
&&&$b$&$1\un{e}c\ldots$&$3\_ec\ldots$\\
&&&$\alpha$&$1\alpha c\un{a}\ldots$&$RHS$\\\hline
$17$&$2\un{c}e\ldots$&$5\_cc\ldots$&$b$&$1\un{d}c\ldots$&$3\_ec\ldots$\\
&&&$b$&$1\un{e}c\ldots$&$3\_ec\ldots$\\
&&&$\alpha$&$5\alpha c\un{a}\ldots$&$RHS$\\\hline
$18$&$2\un{c}e\ldots$&$5\_ce\ldots$&$b$&$1\un{d}c\ldots$&$3\_ec\ldots$\\
&&&$b$&$1\un{e}c\ldots$&$3\_ec\ldots$\\
&&&$\alpha$&$5\alpha c\un{a}\ldots$&$RHS$\\\hline
$19$&$2\un{d}d\ldots$&$3\_bc\ldots$&$b$&$1\un{d}d\ldots$&$4\_cb\ldots$\\
&&&$b$&$1\un{e}d\ldots$&$4\_cb\ldots$\\
&&&$\alpha$&$1\alpha d\un{a}\ldots$&$RHS$\\\hline
$20$&$2\un{d}d\ldots$&$3ca\ldots$&$\emptyset$&$\emptyset$\\\hline
$21$&$2\un{d}e\ldots$&$3\_bc\ldots$&$b$&$1\un{d}d\ldots$&$4\_cb\ldots$\\
&&&$b$&$1\un{e}d\ldots$&$4\_cb\ldots$\\
&&&$\alpha$&$5\alpha d\un{a}\ldots$&$RHS$\\\hline
$22$&$2\un{d}e\ldots$&$3ca\ldots$&$\emptyset$&$\emptyset$\\\hline
$23$&$3\un{a}b\ldots$&$2\_ae\ldots$&$a$&$5\un{c}a\ldots$&$5\_cc\ldots$\\
&&&$a$&$5\un{e}a\ldots$&$5\_cc\ldots$\\
&&&$b$&$3\un{e}a\ldots$&$4\_ca\ldots$\\
&&&$c$&$4\un{c}a\ldots$&$3\_bc\ldots$\\
&&&$\alpha$&$4\alpha a\un{a}\ldots$&$RHS$\\\hline
$24$&$3\un{a}b\ldots$&$3\_bc\ldots$&$a$&$5\un{c}a\ldots$&$3cb\ldots$\\
&&&$a$&$5\un{e}a\ldots$&$3cb\ldots$\\
&&&$b$&$3\un{e}a\ldots$&$4\_cb\ldots$\\
&&&$c$&$4\un{c}a\ldots$&$2\_ab\ldots$\\
&&&$\alpha$&$4\alpha a\un{a}\ldots$&$RHS$\\\hline
$25$&$3\un{a}b\ldots$&$1ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$26$&$3\un{a}b\ldots$&$3ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$27$&$3\un{a}c\ldots$&$2\_ab\ldots$&$a$&$5\un{c}a\ldots$&$3db\ldots$\\
&&&$a$&$5\un{e}a\ldots$&$3db\ldots$\\
&&&$b$&$3\un{e}a\ldots$&$4\_ca\ldots$\\
&&&$c$&$4\un{c}a\ldots$&$3ab\ldots$\\
&&&$\alpha$&$2\alpha a\un{e}\ldots$&$RHS$\\\hline
$28$&$3\un{a}c\ldots$&$3\_bc\ldots$&$a$&$5\un{c}a\ldots$&$3cb\ldots$\\
&&&$a$&$5\un{e}a\ldots$&$3cb\ldots$\\
&&&$b$&$3\un{e}a\ldots$&$4\_cb\ldots$\\
&&&$c$&$4\un{c}a\ldots$&$2\_ab\ldots$\\
&&&$\alpha$&$2\alpha a\un{e}\ldots$&$RHS$\\\hline
$29$&$3\un{a}c\ldots$&$3ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$30$&$3\un{a}e\ldots$&$2\_ab\ldots$&$a$&$5\un{c}a\ldots$&$3db\ldots$\\
&&&$a$&$5\un{e}a\ldots$&$3db\ldots$\\
&&&$b$&$3\un{e}a\ldots$&$4\_ca\ldots$\\
&&&$c$&$4\un{c}a\ldots$&$3ab\ldots$\\
&&&$\alpha$&$5\alpha a\un{b}\ldots$&$RHS$\\\hline
$31$&$3\un{a}e\ldots$&$1db\ldots$&$\emptyset$&$\emptyset$\\
\hline
$32$&$3\un{e}a\ldots$&$4\_ca\ldots$&$a$&$5\un{c}e\ldots$&$3\_bc\ldots$\\
&&&$a$&$5\un{e}e\ldots$&$3\_bc\ldots$\\
&&&$b$&$3\un{e}e\ldots$&$4bc\ldots$\\
&&&$c$&$4\un{c}e\ldots$&$1ab\ldots$\\
&&&$\alpha$&$1\alpha e\un{c}\ldots$&$RHS$\\\hline
$33$&$3\un{e}a\ldots$&$4\_cb\ldots$&$a$&$5\un{c}e\ldots$&$3\_bc\ldots$\\
&&&$a$&$5\un{e}e\ldots$&$3\_bc\ldots$\\
&&&$b$&$3\un{e}e\ldots$&$2ba\ldots$\\
&&&$c$&$4\un{c}e\ldots$&$3ab\ldots$\\
&&&$\alpha$&$1\alpha e\un{c}\ldots$&$RHS$\\\hline
$34$&$3\un{e}e\ldots$&$4\_ce\ldots$&$a$&$5\un{c}e\ldots$&$3\_bc\ldots$\\
&&&$a$&$5\un{e}e\ldots$&$3\_bc\ldots$\\
&&&$b$&$3\un{e}e\ldots$&$3bc\ldots$\\
&&&$c$&$4\un{c}e\ldots$&$3\_bc\ldots$\\
&&&$\alpha$&$5\alpha e\un{b}\ldots$&$RHS$\\\hline
$35$&$3\un{e}e\ldots$&$2ba\ldots$&$\emptyset$&$\emptyset$\\\hline
$36$&$3\un{e}e\ldots$&$3bc\ldots$&$\emptyset$&$\emptyset$\\\hline
$37$&$3\un{e}e\ldots$&$4bc\ldots$&$\emptyset$&$\emptyset$\\\hline
$38$&$4\un{b}b\ldots$&$4\_ce\ldots$&$b$&$4\un{b}b\ldots$&$3bc\ldots$\\
&&&$c$&$3\un{a}b\ldots$&$3\_bc\ldots$\\\hline
$39$&$4\un{b}b\ldots$&$2ba\ldots$&$\emptyset$&$\emptyset$\\\hline
$40$&$4\un{b}b\ldots$&$3bc\ldots$&$\emptyset$&$\emptyset$\\\hline
$41$&$4\un{b}b\ldots$&$4bc\ldots$&$\emptyset$&$\emptyset$\\\hline
$42$&$4\un{b}c\ldots$&$4\_ca\ldots$&$b$&$4\un{b}b\ldots$&$4bc\ldots$\\
&&&$c$&$3\un{a}b\ldots$&$1ab\ldots$\\
&&&$\alpha$&$2\alpha b\un{b}\ldots$&$RHS$\\
&&&$\alpha$&$3\alpha b\un{b}\ldots$&$RHS$\\\hline
$43$&$4\un{b}c\ldots$&$4\_cb\ldots$&$b$&$4\un{b}b\ldots$&$2ba\ldots$\\
&&&$c$&$3\un{a}b\ldots$&$3ab\ldots$\\
&&&$\alpha$&$2\alpha b\un{b}\ldots$&$RHS$\\
&&&$\alpha$&$3\alpha b\un{b}\ldots$&$RHS$\\\hline
$44$&$4\un{b}e\ldots$&$4\_cb\ldots$&$b$&$4\un{b}b\ldots$&$2ba\ldots$\\
&&&$c$&$3\un{a}b\ldots$&$3ab\ldots$\\\hline
$45$&$4\un{b}e\ldots$&$4\_ce\ldots$&$b$&$4\un{b}b\ldots$&$3bc\ldots$\\
&&&$c$&$3\un{a}b\ldots$&$3\_bc\ldots$\\\hline
$46$&$4\un{c}a\ldots$&$2\_ab\ldots$&$b$&$4\un{b}c\ldots$&$4\_ca\ldots$\\
&&&$c$&$3\un{a}c\ldots$&$3ab\ldots$\\
&&&$\alpha$&$5\alpha c\un{d}\ldots$&$RHS$\\\hline
$47$&$4\un{c}a\ldots$&$3\_bc\ldots$&$b$&$4\un{b}c\ldots$&$4\_cb\ldots$\\
&&&$c$&$3\un{a}c\ldots$&$2\_ab\ldots$\\
&&&$\alpha$&$5\alpha c\un{d}\ldots$&$RHS$\\\hline
$48$&$4\un{c}a\ldots$&$3ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$49$&$4\un{c}e\ldots$&$2\_ae\ldots$&$b$&$4\un{b}c\ldots$&$4\_ca\ldots$\\
&&&$c$&$3\un{a}c\ldots$&$3\_bc\ldots$\\\hline
$50$&$4\un{c}e\ldots$&$3\_bc\ldots$&$b$&$4\un{b}c\ldots$&$4\_cb\ldots$\\
&&&$c$&$3\un{a}c\ldots$&$2\_ab\ldots$\\\hline
$51$&$4\un{c}e\ldots$&$1ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$52$&$4\un{c}e\ldots$&$3ab\ldots$&$\emptyset$&$\emptyset$\\\hline
$53$&$4\un{e}c\ldots$&$2\_ec\ldots$&$b$&$4\un{b}e\ldots$&$4\_ce\ldots$\\
&&&$c$&$3\un{a}e\ldots$&$1db\ldots$\\
&&&$\alpha$&$2\alpha e\un{b}\ldots$&$RHS$\\
&&&$\alpha$&$3\alpha e\un{b}\ldots$&$RHS$\\\hline
$54$&$4\un{e}c\ldots$&$1cb\ldots$&$\emptyset$&$\emptyset$\\\hline
$55$&$4\un{e}c\ldots$&$3cb\ldots$&$\emptyset$&$\emptyset$\\\hline
$56$&$4\un{e}e\ldots$&$2\_ec\ldots$&$b$&$4\un{b}e\ldots$&$4\_ce\ldots$\\
&&&$c$&$3\un{a}e\ldots$&$1db\ldots$\\\hline
$57$&$4\un{e}e\ldots$&$1cb\ldots$&$\emptyset$&$\emptyset$\\\hline
$58$&$4\un{e}e\ldots$&$3cb\ldots$&$\emptyset$&$\emptyset$\\\hline
$59$&$5\un{c}a\ldots$&$5\_cc\ldots$&$a$&$4\un{e}c\ldots$&$2\_ec\ldots$\\\hline
$60$&$5\un{c}a\ldots$&$3cb\ldots$&$\emptyset$&$\emptyset$\\\hline
$61$&$5\un{c}a\ldots$&$3db\ldots$&$\emptyset$&$\emptyset$\\\hline
$62$&$5\un{c}e\ldots$&$3\_bc\ldots$&$a$&$4\un{e}c\ldots$&$3cb\ldots$\\\hline
$63$&$5\un{c}e\ldots$&$3ca\ldots$&$\emptyset$&$\emptyset$\\\hline
$64$&$5\un{e}a\ldots$&$5\_cc\ldots$&$a$&$4\un{e}e\ldots$&$2\_ec\ldots$\\\hline
$65$&$5\un{e}a\ldots$&$3cb\ldots$&$\emptyset$&$\emptyset$\\\hline
$66$&$5\un{e}a\ldots$&$3db\ldots$&$\emptyset$&$\emptyset$\\\hline
$67$&$5\un{e}e\ldots$&$3\_bc\ldots$&$a$&$4\un{e}e\ldots$&$3cb\ldots$\\\hline
$68$&$5\un{e}e\ldots$&$3ca\ldots$&$\emptyset$&$\emptyset$\\\hline
\end{longtable}
\fontsize{12}{14}\selectfont
\end{comment}
To illustrate how an IRR can be derived from a member of IRR$({\rm 2})$ and a sequence of IGR's,
consider the following IRR of length 6 that was chosen from the computer program output and represented in $\text{Origin}\to\text{LHS}\to\text{RHS}$ format as follows:
\begin{equation}\label{eq130}3\un{a}ecccb\to1cadbd\un{b}\to 2dbdbdb\_.\end{equation}
The derivation of the first rule of \eqref{eq130} in single TM steps is
\begin{equation}\label{eq131}\begin{array}{l}3\un{a}ecccb\\4c\un{e}cccb\\5ca\un{c}ccb\\3caa\un{c}cb\\2ca\un{a}acb\\1cac\un{a}cb\\
2ca\un{c}dcb\\1cad\un{d}cb\\2cadb\un{c}b\\1cadbd\un{b}\end{array}.\end{equation}
Each time the pointer moves to where it has not been before while going backwards from the LHS, the derivation \eqref{eq131} generates IRR's as follows, followed by \eqref{eq130} in triplet and the abbreviated notation:
\begin{equation}\label{irr_array}\begin{array}{cc}\begin{array}{l}
2\un{c}b\to1d\un{b}\to5\_cd\in IRR(2)\\
1\un{d}cb\to 1bd\un{b}\to 3\_ecd\in IRR(3)\\
2\un{c}dcb\to 1dbd\un{b}\to 5\_cecd\in IRR(4)\\
4\un{e}cccb\to 1adbd\un{b}\to 2\_ececd\in IRR(5)\\\end{array}&
\begin{array}{l}2\un{c}b\to\to5\_cd\\1\un{d}cb\to\to3\_ecd\\2\un{c}dcb\to\to 5\_cecd\\4\un{e}cccb\to\to2\_ececd\end{array}\end{array}.
\end{equation}
This splitting up of the derivation of \eqref{eq130} results from the repeated application of $F$ to \eqref{irr_array}.1.
The abbreviated forms in \eqref{irr_array} can be obtained by applying in order the following results to the first of these IRR's $2\un{c}b\to\to5\_cd$.
\begin{equation}\label{f2_array}\begin{array}{l}2\un{T}_1\to\to 5\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{d}T_{\rm 1}\\1\un{e}T_{\rm 1}\end{array}\right\}\to\to 3\_eT_{\rm 2}\\[15pt]
1\un{T}_1\to\to 3\_T_{\rm 2}\left\{\begin{array}{l}\stackrel{a}{\Rightarrow} 2\un{d}T_{\rm 1}\to\to 4c\un{T}_{\rm 2}\\\stackrel{c}{\Rightarrow} 2\un{a}T_{\rm 1}\to\to 2\_aT_{\rm 2}\\\stackrel{d}{\Rightarrow}2\un{c}T_{\rm 1}\to\to 5\_cT_{\rm 2}\end{array}\right.\\[23pt]
2\un{c}dT_{\rm 1}\to\to 5\_T_{\rm 2}\stackrel{a}{\Rightarrow}\left.\begin{array}{l}4\un{e}ccT_{\rm 1}\\4\un{e}ecT_{\rm 1}\\5\un{c}adT_{\rm 1}\\5\un{e}adT_{\rm 1}\end{array}\right\}\to\to2\_eT_{\rm 2}\\[30pt]
4\un{T}_{\rm 1}\to\to2\_eT_{\rm 2}\stackrel{c}{\Rightarrow} \left.\begin{array}{l}3\un{a}T_{\rm 1}\\4\un{b}T_{\rm 1}\end{array}\right\}\to\to2db\un{T}_{\rm 2}\end{array}.\end{equation}
For the initial steps in the derivation of \eqref{eq130}, the following subcases of successive members of \eqref{f2_array} need to be applied in this order: 1, 3, 1, 1.
Equation \eqref{f2_array} contains examples of IGR's which allow one IRR to be derived from another by substituting for the $T_{\rm 1}$ and $T_{\rm 2}$ as the example shows, and express the application of the function $F$ in Theorem~\ref{irr_ind_thm} in a simpler form. The IGR's have two lengths, one associated with $T_{\rm 1}$ and one associated with $T_{\rm 2}$ and these are defined as the lengths of the corresponding strings on the RHS of the IGR thus for example the lengths of the IGR's in \eqref{f2_array} will be donoted by ${\rm (1,1), (1,1), (3,1), (1,2)}$ respectively.
The equations \eqref{f2_array} are in the shortest forms possible as can be verified from their derivations.
The symbols above the implication signs are the symbol added next to the pointer in the origin ($\alpha$) in the derivation of the IRR's from other ones as described in Section~\ref{sec2}, and are the first 4 symbols of the LHS of IRR \eqref{eq130} taken in reverse order. The results on the right in \eqref{f2_array} are all the results that can be derived from their LHS for that value of $\alpha$ and that length, though the third example is quite complicated and has other values of $\alpha$ ie. $b$ and $c$ with different lengths of results.
The IRRP on the RHS of the last member of \eqref{f2_array} is of type LRR and can be seen to not generate a new IRR directly. Applying the last member of \eqref{f2_array} to the last IRR of \eqref{irr_array} gives the initial result \begin{equation}3\un{a}ecccb\to1cadbd\un{b}\to2db\un{c}ecd\end{equation} which is not an IRR. Taking this computation as far a possible has to be an IRR (in this case having non-extendable type LRR) which is
\begin{equation}\label{final}3\un{a}ecccb\to\to 2dbdbdb\_\end{equation} and has $\alpha =c$ and is in agreement with \eqref{eq130}.
The derivations of \eqref{irr_array} and \eqref{final} illustrate the general procedure for deriving any IRR by repeated applications of $F$ i.e. applying a sequence of IGR's starting from a member of IRR(2).
This example suggests that if all the IGR's needed to generate the IRR$({\it n}+{\rm 1})$ from IRR$({\it n})$ were obtained, these could have lengths much less than ${\it n}+{\rm 1}$ and be fewer in number than the IRR$({\it n}+{\rm 1})$, and this might give a more compact way to represent the action of the TM. This will be followed up later, but many details need to be given first.
\section{General Definition of IGR's}
The general form of the derivation of an IRR from an existing one ($F$) can be expressed in detail as follows. Start with the IRR pattern (IRRP) of type LRL\begin{equation}\label{igr0}t_{\rm 1}\un{y_{\rm 1}}\ldots y_{{\it n}}T_{\rm 1}\to\to t_{\rm 2}\_z_{\rm 1}\ldots z_{{\it n}}T_{\rm 2}\end{equation} in which $T_{\rm 1}$ and $T_{\rm 2}$ have been omitted for brevity in much of this section. Here ${\it n}\ge {\rm 2}$ and the $t$'s are machine states and $y$'s and $z$'s are symbols.
Then proceed with $F$ i.e. add the symbol $\alpha$ to both sides where the pointer is in the RHS then the backward search gives the following types of results (excluding the stationary cycles)
which can be classified according to the rightmost position ${\it j}_{\rm 1}$ of the pointer relative to the symbol $y_{\rm 1}$
\begin{equation}\label{igr1}t_{\rm 1}\alpha \un{y_{\rm 1}}\ldots y_{\it n}\leftarrow \left\{\begin{array}{l}
t'_{\rm 1}\un{\alpha'}y_{\rm 1}\ldots y_{\it n}\text{ for }{\it j}_{\rm 1} = {\rm 0}\vspace{0.5em}\\
t'_{\rm 1}\un{\alpha'}y'_{\rm 1}\ldots y'_{{\it j}_{\rm 1}+{\rm 1}}y_{{\it j}_{\rm 1}+{\rm 2}}\ldots y_{\it n}\text{ for }{\rm 1}\le {\it j}_{\rm 1}\le {\it n-{\rm 2}}\vspace{0.5em}\\
t'_{\rm 1}\alpha y'_{\rm 1}\ldots y'_{{\it n}-{\rm 1}}\un{y'_{\it n}}\text{ for }{\it j}_{\rm 1}={\it n - {\rm 1}}\end{array}\right.\end{equation} where the primes indicate a possible change in the symbol or state by the TM.
For the case ${\it n}={\rm 1}$, ${\it j}_{\rm 1}$ must be 0. Note that the form $t'_{\rm 1}\un{\alpha'}y'_{\rm 1}y_{\rm 2}\ldots y_{\it n}$ cannot arise because a single backward step to the right followed by two backward steps to the left could possibly alter $y_{\rm 1}$ and $y_{\rm 2}$ whereas a single backward step to the left has ${\it j}_{\rm 1}{\rm =0}$ as above.
The point of the classification is to enumerate all the different types of case that can arise after all the symbols that are not altered in the derivation are abstracted out. They are not mentioned explicitly and they form part of an arbitrary string (in this case $T_{\rm 1}$). The last reverse computation step in the last case giving ${\it j}_{\rm 1}={\it n} - {\rm 1}$ cannot not lead to a new IRR because this path and the CS reached does not imply the reachability of the LHS and so does not generate an IRR. If the LHS is reachable it must be because there is another origin with ${\it j}_{\rm 1} < {\it n} - {\rm 1}$. Therefore this case must be omitted for the purpose of generating IGR's, so ${\it j}_1$ can be restricted to the range ${\rm 0}\le {\it j}_{\rm 1}\le{\it n-{\rm 2}}$.
Similarly, for the computation of the new RHS, the results can be classified (again excluding stationary cycles) by the rightmost position ${\it j}_{\rm 2}$ of the pointer. So that this parameter also starts at 0, the pointer starts at position 0 at $\alpha$ and ends at position -${\rm 1}$ if it goes left and ends at position ${\it n}+{\rm 1}$ if it goes right giving the possibilities
\begin{equation}\label{igr2}t_{\rm 2}\un{\alpha}z_{\rm 1}\ldots z_{\it n}\to \left\{\begin{array}{l}t'_{\rm 2}\_\alpha' z'_{\rm 1}\ldots z'_{{\it j}_{\rm 2}}z_{{\it j}_{\rm 2}+{\rm 1}}\ldots z_{\it n}\text{ where }{\rm 0}\le {\it j}_{\rm 2}\le {\it n}\text{ or }\vspace{0.5em}\\ t'_{\rm 2}\alpha'z'_{\rm 1}\ldots z'_{\it n}\_\text{ if }{\it j}_{\rm 2}={\it n}+{\rm 1}\end{array}\right..\end{equation}
This works whenever ${\it n}\ge{\rm 1}$.
If a stationary cycle occurred in \eqref{igr1} it would be noted, but it would have no effect on the general form of the possible results except that none of the forms of endpoint in \eqref{igr1} might result, because a stationary cycle would result in a closed circuit in the reverse search path from which paths ending in a type of endpoint in \eqref{igr1} or none could diverge. As noted earlier this would imply $t_1\alpha\un{y_1}\ldots y_{\it n}$ is in the closed circuit (to avoid a branch point in the forward computation implying it is not unique) so the derived IRR would have type RC. This implies a stationary cycle in the result of \eqref{igr2}.
The minimum number of symbols needed for the representation of \eqref{igr1} is easily seen to be
\begin{equation}\label{r1}{\it r}_{\rm 1}=\left\{\begin{array}{ll}{\rm 1}&\text{ for } {\it j}_{\rm 1}={\rm 0}\\
{\it j}_{\rm 1}+{\rm 2}&\text{ otherwise}\end{array}\right.\end{equation} provided ${\rm 0}\le {\it j}_{\rm 1}\le{\it n-{\rm 2}}$.
Similarly, the minimum number of symbols needed for the representation of the result of \eqref{igr2} is
\begin{equation}\label{r2}{\it r}_{\rm 2}=\text{min}({\it j}_{\rm 2}+{\rm 1},{\it n}+{\rm 1}).\end{equation}
The length of an IGR consists of the pair $({\it r}_{\rm 1},{\it r}_{\rm 2})$.
From \eqref{igr1} and \eqref{igr2} the remaining four combinations can be summarised as
\begin{equation}\label{igr_types}\begin{array}{l}
\left\{\begin{array}{c}t_{\rm 1}\un{T_{\rm 1}}\\
t_{\rm 1}\un{y}_{\rm 1}\ldots y_{{\it j}_{\rm 1}+1}T_{\rm 1}\end{array}\right\}\to\to \left\{\begin{array}{c}
t_{\rm 2}\_z_{\rm 1}\ldots z_{{\it j}_{\rm 2}}T_{\rm 2}\\
t_{\rm 2}\_z_{\rm 1}\ldots z_{\it n}T_{\rm 2}\end{array}\right\}
\stackrel{\alpha}{\Rightarrow}\vspace{0.5em}\\
\left\{\begin{array}{c}t'_{\rm 1}\un{\alpha'}T_{\rm 1}\\
t'_{\rm 1}\un{\alpha'}y'_{\rm 1}\ldots y'_{{\it j}_{\rm 1}+1}T_{\rm 1}\end{array}\right\}\to\to
\left\{\begin{array}{c}t'_{\rm 2}\_\alpha'z'_{\rm 1}\ldots z'_{{\it j}_{\rm 2}}T_{\rm 2}\\
t'_{\rm 2}\alpha'z'_{\rm 1}\ldots z'_{\it n}\un{T_{\rm 2}}\end{array}\right\}\end{array}.
\end{equation}
In this statement the top and bottom parts on the left of$\to\to$ can be combined independently with the top and bottom parts on the right of$\to\to$ i.e. there are four combinations possible. Of these the distinctions on the left of $\to\to$ do not change the type of the new IRR this being respectively LRL and LRR for the top and bottom parts on the right of $to\to$. The IRR"s are also distinguished by different pairs $({\it j}_{\rm 1},{\it j}_{\rm 2})$. The type of an IGR is defined as the type of the IRR that it generates.
The corresponding right-left reversed results starting from an IRRP of type RLR also involve the parameters ${\it j}_{\rm 1}$ and ${\it j}_{\rm 2}$ obtained similarly but counting leftwards. Thus starting from
\begin{equation}\label{igr0.2}t_{\rm 1}y_{\it n}\ldots \un{y_{{\rm 1}}}\to\to t_{\rm 2}z_{\it n}\ldots z_{\rm 1}\_\end{equation}
likewise the following types of results are obtained
which can be classified according to the leftmost position relative to $y_{\rm 1}$, (${\it j}_{\rm 1}$) of the pointer. This satisfies ${\rm 0}\le {\it j}_{\rm 1}\le {\it n} - {\rm 1}$ and gives the following:
\begin{equation}\label{igr1.2}t_{\rm 1}y_{\it n}\ldots \un{y_{\rm 1}}\alpha\leftarrow \left\{\begin{array}{l}
t'_{\rm 1}y_{\it n}\ldots y_{\rm 1}\un{\alpha'}\text{ for }{\it j}_{\rm 1} = {\rm 0}\vspace{0.5em}\\
t'_{\rm 1}y_{\it n}\ldots y_{{\it j}_{\rm 1}+{\rm 2}}y'_{{\it j}_{\rm 1}+{\rm 1}}\ldots y'_{\rm 1}\un{\alpha'}\text{ for }{\rm 1}\le {\it j}_{\rm 1}\le {\it n}-{\rm 2}\vspace{0.5em}\\
t'_{\rm 1}\un{y'_{\it n}}y'_{{\it n} - {\rm 1}}\ldots y'_{\rm 1}\alpha \text{ for }{\it j}_{\rm 1}={\it n} -{\rm 1}\end{array}\right.\end{equation}
Naturally, \eqref{r1} and \eqref{r2} and are still valid and all the types of result in \eqref{igr_types} have corresponding mirror image forms.
%and have the respective forms\\
%$1\to r_1\to 2\to n+1\to 1\to r_2\to 0$\\
%$1\to r_1\to 2\to n+1\to 1\to n+2$\\
%where the numbers (see \eqref{irr_deriv2}) indicate CS's where the pointer position is at some extreme points in the computation and $\alpha$ is this time at position 1 because it is the first symbol of the derived IRRP.
These types of result in \eqref{igr_types} are expressed with the shortest strings of symbols possible (i.e. the $y$'s and $z$'s). The strings $T_{\rm 1}$ and $T_{\rm 2}$ being arbitrary, so can be replaced by any strings. They do not have to have the same length.
These together with their left-right reversed forms are all the different types of IGR's possible.
Simple examples of these are in \eqref{f2_array}, and \eqref{igr1} and \eqref{igr2} indicate the general method for deriving them which is as follows. After the symbol $\alpha$ has been added to the origins on the left, reverse steps of the TM are made recursively, making sure that all possible reverse steps at each stage are done and stopping only when further reverse steps are impossible without the knowledge of what the strings $T_{\rm 1}$ and $T_{\rm 2}$ are, as described in Section~\ref{sec2}.
Thus an IGR is defined to have no redundant symbols where the pointer does not reach during its derivation. This is
analogous to IRR's being irreducible. In the derivation of the IGR from an IRR of length ${\it n}$, the backward search
to obtain the new origins and in the forward computation to obtain the new RHS, the pointer can obviously never move
outside the strings of lengths ${\it r_{\rm 1}}$ and ${\it r_{\rm 2}}$ introduced above except for the last TM step in the forward computation. In addition all these positions
of the pointer are reached during the derivation, the string of length ${\it r_{\rm 1}}$ for the derivation of a new
origin and the string of length ${\it r_{\rm 2}}$ for the derivation of the new RHS
If the pointer ends up at one
end of the string $T_{\rm 2}$ ( indicated by $\un{T_{\rm 2}}$), the pointer position is clear from the context.
The pair of strings of symbols $(T_{\rm 1},T_{\rm 2})$ of lengths $({\it n}+{\rm 1}-{\it r_{\rm 1}},{\it n}+{\rm 1}-{\it r_{\rm 2}})$ respectively in \eqref{igr_types} that are not passed by the pointer during the derivation of an IGR from an IRR of length ${\it n}$ that is the basis of its LHS will be removed and listed as ``context pairs" so that the result is presented in its minimal form i.e. as an IGR in computer output.
A IGR could be defined to include all the possible results that can be derived for any possible value of $\alpha$ (an IGR member), i.e. all the possible origins for each $\alpha$, but if there is not likely to be confusion I will refer to such statements as IGR's as was done above. Thus an IGR would be the union over $\alpha$ of the IGR members.
An IGR member has the form (IRRP,$\alpha$) $\Rightarrow$ set of IRRP's, so the above results in \eqref{f2_array} could be described as IGR members. Thus it would be possible for different RHS's of the IGR to have different values of ${({\it r}_{\rm 1},{\it r}_{\rm 2})}$ corresponding to different values of $\alpha$, but these will be separated into different IGR's in the computer output.
There can be a problem that occurs in the computer representation of the IGR's after the context strings have been separated out, which is to determine whether the original IRRP on its left is of type LRL or RLR. Provided ${\it n }>1$, it is not immediately obvious which is the case because the pointer positions and the parameter ${\it j}_{\rm 1}$ can be counted going either way, for example compare
\eqref{igr1} with \eqref{igr1.2}. The way it works is that a CS in the computer program output is represented as $CS(t,p,l,string)$ where $t$ is the machine state, $p$ is the pointer position counted from the left and is one for the symbol on the left, and is 0 for the position just to the left of this symbol, and is $l+{\rm 1}$ for the position just to the right of the string, where $l={\it n}$ is the length of the string. The string is spelled out inside quote marks in printed output. After the context strings have been split out of the derived IGR, the pointer position in the origin of the IRRP set on the LHS of \eqref{igr0} is 1 by convention if the
original IRRP (see \eqref{igr1}) (the LHS of the new IGR) was of type LRL or LRR because the pointer starts at 1 and is not affected by the truncation of the symbols from the right. If the original IRRP was of type RLR or RLL, the pointer position
in its origin (LHS of \eqref{igr0.2}) is initially by convention at ${\it n}$ (i.e. the right hand end)
and is reduced as a result of splitting out the context symbols. This for ${\it j}_{\rm 1}={\rm 0}$ is position ${\it n}$ minus the length of the string of symbols removed also ${\it n}$ i.e. {\rm 0}, and is ${\it n}$ minus the length of $y_{\it n}\ldots y_{{\it j}_{\rm 1} + {\rm 2}}$ otherwise, which is ${\it j}_{\rm 1} + {\rm 1}$. This value can never be 1, so the value 1 is characteristic of the original IGR being of type LRL. This implies that the value $p = {\rm 1}$ in an origin CS on the LHS of an IGR indicates, provided ${\it n}>{\rm 1}$, that the context strings ($T_{\rm 1}$ and $T_{\rm 2}$) are added on the right, and on the left otherwise. For the case ${\it n}={\rm 1}$ this is obvious from the RHS of the IRRP on the LHS of the IGR.
which is of the form $t_{\rm 2}\_z_{\rm 1}$ or $t_{\rm 2}z_{\rm 1}\_$ according to whether the IGR is of type LRL or RLR respectively. This shows that this obvious convention for defining the pointer positions in the different cases distinguishes the LRL, LRR from the RLR, RLL types of IGR.
The above argument shows, when combined with Theorem~\ref{irr_ind_thm}, that\\
(1) every IRR of length ${\it n}+{\rm 1}$ of type RL can be derived by $F$ from another IRR of length ${\it n}$
of type LRL by an IGR with parameters ${({\it r}_{\rm 1},{\it r}_{\rm 2})}$ of type \eqref{igr_types}.1 (LRL \eqref{igr_types}) in satisfying
${\rm 1}\le\it r_{\rm 1}\le{\it n}$ and ${\rm 1}\le{\it r}_{\rm 2}\le{\it n}+{\rm 1}$ as described and\\(2)
every IRR of length ${\it n}+{\rm 1}$ of type LRR can be derived by $F$ from another IRR of length ${\it n}$ of
type LRL by an IGR of type \eqref{igr_types}.2 (LRR in \eqref{igr_types}) (with parameters ${\it r}_{\rm 1}$ and ${\it r}_{\rm 2}$ such
that ${\rm 1}\le\it r_{\rm 1}\le{\it n}$ and ${\it r}_{\rm 2}={\it n}+{\rm 1}$.
These can be applied recursively to show that
\begin{Theorem}\label{thm1}any extendable IRR (type LRL or RLR) of length $\ge {\it 3}$ can be obtained from a member of IRR(2) by a sequence of substitutions of IGR's as described here under case (1). Any non-extendable IRR (type RLL or LRR) can be obtained from a member of IRR(2) by the above substitutions (0 or more) followed by a single substitution step under case (2).
\end{Theorem}
This theorem is illustrated by the example at the beginning of this section.
This suggests the obvious process for generating the set of all the IGR's could start as follows after finding all the members of IRR(2). Essentially this was the method used in the latest version of the program \cite{tie_v3_0} to generate Table~\ref{table3}.
Find all the members of IRR(3) and the IGR's used to generate them from the IRR(2). These will be IGR's of lengths
$({\rm 1,1})$, $({\rm 1,2})$, $({\rm 1,3}), ({\rm 2,1})$, $({\rm 2,2})$, and $({\rm 2,3})$. Likewise the IRR(4) can be obtained from the IRR(3) and the IGR's summarising this can be added while not duplicating any IGR's already found etc.. This can be repeated to generate up to the IRR(${\it n}$). After a while hopefully to generate the ${\rm IRR}({\it n}+{\rm 1})$ from the ${\rm IRR}({\it n})$ will not require any IGR's that have not already been obtained for ${\it n}$ sufficiently large.
In the remainder of the paper the following example was studied because the results from \eqref{1} became very complicated.
\begin{equation}\label{tm2}\begin{array}{c}
1\un{a}\to 2b \_\\
1\un{b}\to 3\_b\\
1\un{c}\to 1b\_\\
2\un{a}\to 3b\_\\
2\un{b}\to 2c\_\\
2\un{c}\to 1\_c\\
3\un{a}\to 1\_a\\
3\un{b}\to 1\_a\\
3\un{c}\to 3c\_\\
\end{array}\end{equation}
The results for the IGR's from TM \ref{tm2} were as follows in Table~\ref{table3} giving the maximum length of the computation rules as 10.
\newpage
\fontsize{10}{10}\selectfont
\begin{longtable}{ll}
\caption{IGR's generated by the computer program\label{table3}}\\
1&$1\un{T_1}\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{c}T_1\to\to 3\_bT_2$\\
2&$1\un{c}aT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}2\un{a}ca\\2\un{a}cb\end{array}\right\}T_1\to\to 3\_bT_2$\\
3&$1\un{c}aaT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{a}baa\\1\un{a}bab\end{array}\right\}T_1\to\to 3\_bT_2$\\
4&$1\un{c}ababT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{a}bbccbT_1\to\to 3\_bT_2$\\
5&$1\un{c}ababcT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{a}bbccacT_1\to\to 3\_bT_2$\\
6&$1\un{c}abcT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}2\un{a}ccac\\2\un{a}ccbc\end{array}\right\}T_1\to\to 3\_bT_2$\\
7&$1\un{c}cT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{a}bcT_1\to\to 3\_bT_2$\\
8&$2\un{T_1}\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{a}T_1\to\to 3\_bT_2$\\
9&$3\un{T_1}\to\to 1\_T_2\stackrel{b}{\Rightarrow}2\un{a}T_1\to\to 3\_bT_2$\\
10&$3\un{T_1}\to\to 1\_aT_2\stackrel{c}{\Rightarrow}3\un{c}T_1\to\to 2bb\un{T_2}$\\
11&$1\un{c}cT_1\to\to 1\_ababT_2\stackrel{c}{\Rightarrow}2\un{b}bcT_1\to\to 3bbbbb\un{T_2}$\\
12&$1\un{c}aT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T_1\to\to 3\_bababaT_2$\\
13&$1\un{c}aaT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}2\un{b}baa\\2\un{b}bab\end{array}\right\}T_1\to\to 3\_bababaT_2$\\
14&$1\un{c}ababT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}2\un{b}bbccbT_1\to\to 3\_bababaT_2$\\
15&$1\un{c}ababcT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}2\un{b}bbccacT_1\to\to 3\_bababaT_2$\\
16&$1\un{c}abcT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ccac\\3\un{c}ccbc\end{array}\right\}T_1\to\to 3\_bababaT_2$\\
17&$1\un{c}cT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}2\un{b}bcT_1\to\to 3\_bababaT_2$\\
18&$2\un{T_1}\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}2\un{b}T_1\to\to 3\_bababaT_2$\\
19&$1\un{c}cT_1\to\to 1\_ababcT_2\stackrel{c}{\Rightarrow}2\un{b}bcT_1\to\to 3bbbbbc\un{T_2}$\\
20&$1\un{c}aT_1\to\to 1\_abcT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T_1\to\to 1bbbb\un{T_2}$\\
21&$2\un{T_1}\to\to 1\_cT_2\stackrel{c}{\Rightarrow}2\un{b}T_1\to\to 1bb\un{T_2}$\\
22&$1\un{T_1}\to\to 3\_T_2\stackrel{b}{\Rightarrow}1\un{c}T_1\to\to 1\_aT_2$\\
23&$1\un{c}aT_1\to\to 3\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}2\un{a}ca\\2\un{a}cb\end{array}\right\}T_1\to\to 1\_aT_2$\\
24&$1\un{c}aaT_1\to\to 3\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{a}baa\\1\un{a}bab\end{array}\right\}T_1\to\to 1\_aT_2$\\
25&$1\un{c}ababT_1\to\to 3\_T_2\stackrel{b}{\Rightarrow}1\un{a}bbccbT_1\to\to 1\_aT_2$\\
26&$1\un{c}ababcT_1\to\to 3\_T_2\stackrel{b}{\Rightarrow}1\un{a}bbccacT_1\to\to 1\_aT_2$\\
27&$1\un{c}abcT_1\to\to 3\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}2\un{a}ccac\\2\un{a}ccbc\end{array}\right\}T_1\to\to 1\_aT_2$\\
28&$1\un{c}cT_1\to\to 3\_T_2\stackrel{b}{\Rightarrow}1\un{a}bcT_1\to\to 1\_aT_2$\\
29&$2\un{T_1}\to\to 3\_T_2\stackrel{b}{\Rightarrow}1\un{a}T_1\to\to 1\_aT_2$\\
30&$3\un{T_1}\to\to 3\_T_2\stackrel{b}{\Rightarrow}2\un{a}T_1\to\to 1\_aT_2$\\
31&$2\un{T_1}\to\to 3\_baT_2\stackrel{c}{\Rightarrow}2\un{b}T_1\to\to 3bbb\un{T_2}$\\
32&$2\un{c}aT_1\to\to 3\_babT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T_1\to\to 3\_babaT_2$\\
33&$1\un{c}aaT_1\to\to 3\_babT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}2\un{b}baa\\2\un{b}bab\end{array}\right\}T_1\to\to 3\_babaT_2$\\
34&$1\un{c}ababT_1\to\to 3\_babT_2\stackrel{c}{\Rightarrow}2\un{b}bbccbT_1\to\to 3\_babaT_2$\\
35&$1\un{c}ababcT_1\to\to 3\_babT_2\stackrel{c}{\Rightarrow}2\un{b}bbccacT_1\to\to 3\_babaT_2$\\
36&$1\un{c}abcT_1\to\to 3\_babT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ccac\\3\un{c}ccbc\end{array}\right\}T_1\to\to 3\_babaT_2$\\
37&$1\un{c}cT_1\to\to 3\_babT_2\stackrel{c}{\Rightarrow}2\un{b}bcT_1\to\to 3\_babaT_2$\\
38&$2\un{T_1}\to\to 3\_babT_2\stackrel{c}{\Rightarrow}2\un{b}T_1\to\to 3\_babaT_2$\\
39&$3\un{T_1}\to\to 3\_babT_2\stackrel{c}{\Rightarrow}3\un{c}T_1\to\to 3\_babaT_2$\\
40&$1\un{T_1}\to\to 1T_2\_\left\{\begin{array}{l}\stackrel{a}{\Rightarrow}\left.\begin{array}{l}3T_1\un{a}\\3T_1\un{b}\end{array}\right\}\to\to 2T_2b\_\\\stackrel{c}{\Rightarrow}2T_1\un{c}\to\to 1T_2b\_\end{array}\right.$\\
41&$1\un{T_1}\to\to 2T_2\_\stackrel{a}{\Rightarrow}\left.\begin{array}{l}3T_1\un{a}\\3T_1\un{b}\end{array}\right\}\to\to 3T_2b\_$\\
42&$3\un{T_1}\to\to 2T_2\_\stackrel{b}{\Rightarrow}1T_1\un{b}\to\to 2T_2c\_$\\
43&$1\un{T_1}\to\to 3T_2\_\stackrel{c}{\Rightarrow}2T_1\un{c}\to\to 3T_2c\_$\\
44&$3T_1bb\un{b}\to\to 3T_2\_\stackrel{c}{\Rightarrow}\left.\begin{array}{l}2T_1aab\un{c}\\2T_1abb\un{c}\end{array}\right\}\to\to 3T_2c\_$\\
45&$1\un{T_1}\to\to 2T_2b\_\stackrel{c}{\Rightarrow}2T_1\un{c}\to\to 3\un{T_2}bc$\\
46&$1\un{T_1}\to\to 2T_2c\_\stackrel{c}{\Rightarrow}2T_1\un{c}\to\to 1T_2bb\_$\\
47&$3\un{T_1}\to\to 3T_2c\_\stackrel{b}{\Rightarrow}1T_1\un{b}\to\to 2T_2bb\_$\\
48&$1\un{T_1}\to\to 2T_2bb\_\stackrel{c}{\Rightarrow}2T_1\un{c}\to\to 1\un{T_2}abc$\\
49&$3\un{T_1}\to\to 3T_2bb\_\stackrel{b}{\Rightarrow}1T_1\un{b}\to\to 1\un{T_2}aba$\\
50&$3\un{T_1}\to\to 3T_2cb\_\stackrel{b}{\Rightarrow}1T_1\un{b}\to\to 3T_2bbb\_$\\
51&$3T_1bb\un{b}\to\to 3T_2cb\_\stackrel{a}{\Rightarrow}\left.\begin{array}{l}3T_1aab\un{a}\\3T_1abb\un{a}\\3T_1aab\un{b}\\3T_1abb\un{b}\end{array}\right\}\to\to 3T_2bbb\_$\\
52&$3\un{T_1}\to\to 3T_2bbb\_\stackrel{b}{\Rightarrow}1T_1\un{b}\to\to 3\un{T_2}baba$\\
53&$1\un{T_1}\to\to 3T_2bbbbb\_\stackrel{a}{\Rightarrow}\left.\begin{array}{l}3T_1\un{a}\\3T_1\un{b}\end{array}\right\}\to\to 3\un{T_2}bababa$\\
54&$3\un{T_1}\to\to 3T_2bbbbb\_\stackrel{b}{\Rightarrow}1T_1\un{b}\to\to 3\un{T_2}bababa$\\
55&$3T_1bb\un{b}\to\to 3T_2bbbbb\_\stackrel{a}{\Rightarrow}\left.\begin{array}{l}3T_1aab\un{a}\\3T_1abb\un{a}\\3T_1aab\un{b}\\3T_1abb\un{b}\end{array}\right\}\to\to 3\un{T_2}bababa$\\
\end{longtable}
\fontsize{12}{14}\selectfont
Theorem~\ref{thm1} demonstrates the importance of derivations of IRR's using chains of IGR's substituted into each other.
Connected with this is the relation `can be followed by' which restricts the possible sequences of substitutions of IGR's. This is given in Table~\ref{table4} and requires a match on the LHS and on the RHS in which the machine state and the symbol strings must match, as well as the direction for adding $\alpha$, and the first IGR must be of extendable type i.e. it must generate IRR's of type LRL or RLR.
In Table~\ref{table4} the numbers refer to IGR's in Table~\ref{table3}. The letters if present refer to the part of the IGR associated with that letter as the symbol above $\Rightarrow$ i.e. the symbol called $\alpha$, otherwise the whole IGR is referred to. The following number refers to the sub-part of the IGR with that numbered origin in the RHS of the IGR. On the RHS of Table~\ref{table3} (to the right of $\to$) all parts and sub-parts of an IGR referenced are included. Every IGR on the left of $\to$ can be followed by any IGR on the right of $\to$ in the same row.
\newpage
\fontsize{10}{10}\selectfont
\begin{longtable}{ll}
\caption{The relation `can be followed by'\label{table4}}\\
$1\to$ &$22,23,24,25,26,27,28,32,33,34,35,36,37$\\
$3b1,3b2,4,5,7,8\to$ &$22$\\
$\left.\begin{array}{l}2b1,2b2,6b1,6b2,9,13c1,13c2,14,15,\\17,18,33c1,33c2,34,35,37,38\end{array}\right\}\to$ &$29,31,38$\\
$12c1,12c2,16c1,16c2,36c1,36c2,39\to$ &$30,39$\\
$22\to$ &$1,2,3,4,5,6,7,10,11,12,13,14,15,16,18,19$\\
$23b1,23b2,27b1,27b2,30\to$ &$8,18$\\
$24b1,24b2,25,26,28,29\to$ &$1$\\
$32c1,32c2\to$ &$29,38$\\
$40a1,40a2\to$ &$42$\\
$41a1\to$ &$49,50,52,54$\\
$41a2\to$ &$44,49,50,51,52,54,55$\\
$42\to$ &$41,46$\\
$47\to$ &$41,45,48$\\
$50\to$ &$43,53$\\
$51a1,51a2,51a3\to$ &$49,52,54$\\
$51a4\to$ &$44,49,52,54,55$\\
\end{longtable}
\fontsize{12}{14}\selectfont
By examining these IGR's in Table~\ref{table3} and the compatibility relations in Table~\ref{table4} the following facts become evident:
\begin{enumerate}
\item There are a relatively small number of distinct origins of the LHS's of these IGR's. Each of these together with the value of $\alpha$ gives rise to the same origin of the RHS of the IGR regardless of the RHS of the LHS of the IGR. For example $1\un{c}aT_{\rm 1}$ with $\alpha=b$ is always associated with $\left.\begin{array}{l}2\un{a}ca\\2\un{a}cb\end{array}\right\}T_{\rm 1}$ in IGR's 2 and 23.
\item IGR's can be chained together by substitutions for the arbitrary strings $T_{\rm 1}$ and $T_{\rm 2}$.
\item In the chain of substitutions, there is a restriction on which IGR can follow another IGR; this results from the structure of the IGR's themselves. This information is given in Table~\ref{table4}.
\item Other restrictions result from the way in which sequences of substitutions operate.
\item By carrying out $F$ to the RHS of an IGR, it is sometimes possible to deduce that no previous IGR's to a sequence of them can affect which IGR's can follow the sequence.
\item If by carrying out $F$ to any sequence of IGR's to find which IGR's can be next in the sequence, there always results IGR's that have already been listed, then it would show that the set of IGR's found is sufficient to generate all the IRR's for the TM.
\end{enumerate}
Temporarily disregarding property 1, and in the hope that Table~\ref{table3} would have property 6, manual calculation was started beginning with IGR $22$ because
from Table~\ref{table4}, IGR $22$ clearly plays an important role. By restricting at first consideration to IGR $1$ followed by IGR $22$ denoted by $1\cdot 22$ fewer possibilities will result for the following IGR's.
It was soon found that this is likely to get very unwealdy because of the large number of cases to be considered, Nevertheless is was instructive to try.
The first case to be considered was what IGR's that can follow $1\cdot 22$?
The sequence of IGR's $1\cdot 22$ is $1\un{T_1}\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{c}T_1\to\to 3\_bT_2\stackrel{b}{\Rightarrow}1\un{c}cT_1\to\to 1\_abT_2$ obtained by substituting $cT_1$ for $T_1$ and $bT_2$ for $T_2$ in IGR $22$. The result of this is a composite IGR. The IRR's that it generates are a subset of the IRR's generated by looking for which IGR's follow IGR $22$ alone. By trying to apply $F$ to this general form, results dependent on the arbitrary strings $T_{\rm 1}$ and $T_{\rm 2}$ will be produced.
This starts by considering what CS's can lead to $1\alpha\un{c}cT_1$ for any symbol $\alpha$. It is easy to see that \begin{equation}\label{eq23}1\alpha\un{c}cT_1\left\{\begin{array}{l}\stackrel{\alpha = b}{\leftarrow}1\un{c}ccT_1\\\leftarrow 2\alpha c\un{c}T_1\end{array}\right..\end{equation}
in one TM step in either case. The first of these will lead to the IRRP
$1\un{c}ccT_{\rm 1}\to\to 3\_babT_{\rm 2}$ because $1\un{b}abT_{\rm 2}\to 3\_babT_{\rm 2}$. The strings $ccT_{\rm 1}$ and $abT_{\rm 2}$ are not changed because the pointer does not enter them in the derivation of the IRRP, so the IGR used is $1\un{T_{\rm 1}}\to\to 1\_T_{\rm 2}\stackrel{b}{\Rightarrow} 1\un{c}T_{\rm 1}\to\to 3\_bT_{\rm 2}$ i.e. IGR $1$ in Table~\ref{table3}. The second result of \eqref{eq23} has reached condition 2 in the backward search if $T_{\rm 1}$ is the empty string, which implies that there is no point in continuing the backward search further in that case.
If $T_{\rm 1}$ is not the empty string, the general reasoning indicates that $T_{\rm 1}$ needs to be specialised further by prepending the sequence of IGR's $1\cdot 22$ with others, however the backward search can be logically continued giving
\begin{equation}2\alpha c\un{c}T_1\leftarrow 2\alpha\un{b}cT_1\left\{\begin{array}{l}\stackrel{\alpha = b}{\leftarrow} 1\un{a}bcT_1\\\stackrel{\alpha = c}{\leftarrow}2\un{b}bcT_1\end{array}\right.\end{equation}
which is independent of $T_{\rm 1}$ because the first of these reverse steps from $2\alpha c\un{c}T_1$ cannot lead to any other result than the one indicated (because there is no TM step ending in $2\_\beta$ no matter what the symbol $\beta$ in $T_{\rm 1}$ is). This shows that if $T_{\rm 1}$ is not the empty string, the result will always be that condition 1 is reached, giving another IGR.
Returning to the general argument,
\begin{comment}
Instead, expressing \eqref{eq23} as an IGR (shortest form) gives the same result as \ref{table3}.1 with $\un{T_1}$ replaced by $\un{c}cT_1$ and $T_2$ replaced by $abT_2$ after combining it with $1\un{b}abT_2\to 3\_babT_2$ and identifying
the longest strings of symbols that are not altered.
\end{comment}
taking a further step back in the sequence of IGR's to be considered gives for example $22\cdot 1\cdot 22$.
This sequence gives \begin{equation}
1\un{T_1}\to\to 3\_T_2\stackrel{22b}{\Rightarrow}1\un{c}T_1\to\to 1\_aT_2\stackrel{bb}{\Rightarrow}1\un{c}ccT_1\to\to 1\_abaT_2\end{equation} the second part of which comes from $1\cdot 22$ above. The symbols above the symbols $\Rightarrow$ respectively indicate IGR $22$ with $\alpha = b$ and as above ($1\cdot 22$) with two steps of IGR's with $\alpha = b$. Applying $F$ to this starts by the backward search from $1\alpha\un{c}ccT_1$ giving (e.g. using \eqref{eq23})
\begin{equation}\label{eq2}1\alpha\un{c}ccT_1\left\{\begin{array}{l}\leftarrow 2\alpha c\un{c}cT_1\leftarrow 2\alpha\un{b}ccT_1\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}bccT_1\\\stackrel{c}{\leftarrow}2\un{b} bccT_1\end{array}\right.\\\stackrel{b}{\leftarrow} 1\un{c}cccT_1\end{array}\right..\end{equation}
Combining this with $1\un{b}abaT_2\to 3\_babaT_2\text{ and }1\un{c}abaT_2\to 3babb\un{T_2}$ and absorbing any unchanged symbols into $T_1$ or $T_2$ because the pointer has not reached them gives the results $1$, $7$ and
\begin{equation}\label{eq1}1\un{c}cT_1\to\to 1\_abaT_2\stackrel{c}{\Rightarrow}2\un{b}bcT_1\to\to 3bbcb\un{T_2}.\end{equation}
[As an aside comment, Actually $17$ is a special case of $11$ which is itself a special case of \eqref{eq1} formed by successively decreasing the length of the string in the RHS by 1. Because in these three cases, $17$ uniquely has the pointer finishing at the $\alpha$ end of the string in RHS of the RHS, such a sequence as \eqref{eq1}, $11$ and $17$ cannot be continued by specialising $T_{\rm 2}$ and continuing the computation to the end in the RHS so any sequence of IGR's ending with $17$]
In \ref{eq2} because of the absence of a branch of the backward search taking the pointer to the opposite end of the string from $\alpha$, it implies that any special cases of $T_{\rm 1}$ that would result from prior IGR's in the sequence could not affect the new origins of IGR's that could be next in the sequence, only the RHS's could vary. This is because the general form of the derivation of a new origin follows the pattern in \eqref{eq2} whatever substitutes for $T_{\rm 1}$. Because $1$ can also be preceded by $24b1$, $24b2$, $25$, $26$, $28$, $29$, these cases could now be considered in turn preceding $1\cdot 22$.
These results are very complicated and the way forward seems unclear, because in the derivation of new IGR's by applying $F$, both the new origins then the new RHS's have to be found and there are a lot of different combinations of cases that can arise. Also the number of cases to be considered seems prohibitively large based on the relation `can be followed by' in Table~\ref{table4}.
\begin{comment}The above comment on \eqref{res} implies that there are no special cases regarding regarding what symbols $T_1$ starts with that can generate another branch or extra case in \eqref{res} i.e. \eqref{res} is essentially complete. This special circumstance implies that if the same analysis ($F$) was applied to any sequence of IGR's that end in $1\to 22$, the equivalent results for the set of IGR's that can follow the sequence would be obtained that can also be expressed as $\{1,7,\eqref{new}\}$.
\subsubsection{Applying $F$ to $\ldots\cdot 1\cdot 22$}
$24b1\cdot 1\cdot 22$ gives the RHS $1\un{c}cabaaT_1\to\to 1\_abaT_2$. Applying $F$ to this gives for the backward search
\begin{equation}1\alpha\un{c}cabaaT_1\left\{\begin{array}{l}\leftarrow 2\alpha c\un{c}abaaT_1\leftarrow 2\alpha\un{b}cabaaT_1\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}bcabaaT_1\\\stackrel{c}{\leftarrow}2\un{b}bcabaaT_1\end{array}\right.\\\stackrel{b}{\leftarrow}1\un{c}ccabaaT_1\end{array}\right..\end{equation}
When expressed in terms of the longest strings of symbols unaltered gives same result as above i.e.
\begin{equation}\ldots 24b1\to 1\to 22\stackrel{F}{\Rightarrow} \{1, 7, \eqref{eq1}\}.\end{equation}
$24b2\to 1\to 22$ gives a very similar result giving the same result when reduced to its shortest form i.e.
\begin{equation}\ldots 24b2\to 1\to 22\stackrel{F}{\Rightarrow} \{1, 7, \eqref{eq1}\}.\end{equation}
The same thing happens with the others that include all the possible IGR's preceding $1\to 22$ so the results can be written briefly as
\begin{equation}\ldots\{22, 24b1, 24b2, 25, 26, 28, 29\}\to 1\to 22\stackrel{F}{\Rightarrow} \{1, 7, \eqref{eq1}\}.\end{equation}
The reason for this is that they all involve tracing back from $1\alpha\un{c}c\ldots$ that does not involve the pointer reaching beyond the third symbol so the results are the same when reduced to the shortest form.
\subsubsection{$3\to 22$}
This can be written as \begin{equation}\label{3.22}1\un{c}aaT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}\un{a}baa\\\un{a}bab\end{array}\right\}T_1\to\to 3\_bT_2\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}T_1\to\to 1\_abT_2.\end{equation} after substituting
$\un{a}baaT_1$ respectively $\un{a}babT_1$ for $T_1$ and $bT_2$ for $T_2$ in IGR $22$.
Applying $F$ to the first part of this i.e. using $1\un{c}abaa$ as the origin to start from gives the long form result (without reducing the strings to minimal form)
\begin{equation}\label{3b1.22.long}1\un{c}abaaT_1\to\to 1\_abT_2\left\{\begin{array}{l}\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{c}cabaa\\2\un{a}cabaa\\2\un{a}cbbaa\end{array}\right\}T_1\to\to 3\_babT_2\\\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}cabaa\\3\un{c}cbbaa\end{array}\right\}T_1\to\to 2bbc\un{T_2}\end{array}\right..\end{equation}
By tracking the rightmost position of the pointer in each branch in the backward search starting from $1\alpha \un{c}abaaT_1$, the minimal forms of the results in \eqref{3b1.22.long} turn out to be $1$ and $2$ and the new one
\begin{equation}\label{extraIGR}1\un{c}aT_1\to\to 1\_abT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T_1\to\to 3bbc\un{T_2}.\end{equation}
Along with the above are the residual origins\begin{equation}\label{extra}\left.\begin{array}{l}3\alpha caab\un{a}\\3\alpha caab\un{b}\\3\alpha cabb\un{a}\\3\alpha cabb\un{b}\end{array}\right\}T_1\end{equation} derived from the first part of \eqref{3.22} i.e. $3b1\to 22$,
which are the residual CS's where the pointer reached the opposite end of the string from $\alpha$. These are not included in the results of $F$ because they are not themselves new IGR's, but they are needed when the results are used as starting points for the calculation of $F$ for a special case of $3b1\to 22$ as occurs when there are extra IGR's preceding the sequence of IGR's considered, because this frequently results in $T_1$ being specialised by specifying the first few symbols of it.
This could result in an enlarged backward search tree. Thus in this case, if other previous history is specified before IGR $3$, more following IGR's might result. Importantly note that in the absence of residual origins, the set of IGR's as a result of $F$ cannot change as a result of specialising $T_1$ i.e. specifying previous IGR's in the sequence studied.
The residual origins \eqref{extra} be written as \begin{equation}3\alpha ca\left\{\begin{array}{l}a\\b\end{array}\right\}b\left\{\begin{array}{l}\un{a}\\\un{b}\end{array}\right\}T_1\end{equation}
where the symbols in the two arrays can be chosen independently.
Similarly applying $F$ to $3b2\to 22$ gives the long form result
\begin{equation}\label{3b2.22.long}1\un{c}ababT_1\to\to 1\_abT_2\left\{\begin{array}{l}\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{c}cabab\\2\un{a}cabab\\2\un{a}cbbab\end{array}\right\}T_1\to\to 3\_babT_2\\\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}cabab\\3\un{c}cbbab\end{array}\right\}T_1\to\to 2bbc\un{T_2}\end{array}\right.\end{equation} which is the same as \eqref{3b1.22.long} except that the symbol just before $T_1$ is $b$ instead of $a$, because the pointer is not interacting with this symbol. It can by truncation
to the minimum number of symbols be written as $\{1, 2, \eqref{extraIGR}\}$ as above. Likewise there are the residual origins \eqref{extra2} to be included that are affected by this change of symbol and are
\begin{equation}\label{extra2}\left.\begin{array}{l}1\alpha caba\un{b}\\1\alpha cabb\un{b}\\1\alpha cbba\un{b}\\1\alpha cbbb\un{b}\end{array}\right\}T_1\end{equation}
i.e. \begin{equation}1\alpha c\left\{\begin{array}{l}a\\b\end{array}\right\}b\left\{\begin{array}{l}a\\b\end{array}\right\}\un{b}T_1.\end{equation}
Thus the main results of this section can be summarised as
\begin{equation}3\to 22\stackrel{F}{\Rightarrow}\{1,2,\eqref{extraIGR}\}.\end{equation}
For extending \eqref{3.22} to include previous history note that the result \eqref{3.22} cannot be repeated because the strings do not match i.e. $3\to 22\to 3\to 22$ is not possible. Table~\ref{table4} shows that IGR $3$ can only be preceded by IGR $22$. Therefore any IRR's derived ending with $3\to 22$ must take the form $\ldots x\to 22\to 3\to 22$ where $x$ is not IGR $3$.
Reasoning from the other end shows that IGR $22$ with context $(b,b)$, $22(b,b)$, is $1\un{b}T_1\to\to 3\_bT_2\stackrel{b}{\Rightarrow}1\un{c}bT_1\to\to 1\_abT_2$ which cannot be followed by IGR $3$ because $1\un{c}bT_1$ does not match $1\un{c}aaT_1$, and $(b,b)$ is the context in which IGR $22$ appears in the set IRR(2) from which all IRR's are derived by IGR's.
\subsubsection{$22\to 3 \to 22$}
This can be written as \begin{equation}\label{22.3.22}1\un{a}aT_1\to\to 3\_T_2\stackrel{bbb}{\Rightarrow}\left.\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}T_1\to\to 1\_abaT_2.\end{equation}
Applying $F$ to $22\to 3b1\to 22$ gives the long form result (without reducing the strings to minimal form)
similar to \eqref{3b1.22.long} and differs from it only in that $T_2$ is replaced by $aT_2$:
\begin{equation}\label{22.3b1.22.long}1\un{c}abaaT_1\to\to 1\_abaT_2\left\{\begin{array}{l}\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{c}cabaa\\2\un{a}cabaa\\2\un{a}cbbaa\end{array}\right\}T_1\to\to 3\_babaT_2\\\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}cabaa\\3\un{c}cbbaa\end{array}\right\}T_1\to\to 3bbcb\un{T_2}\end{array}\right.\end{equation}
thus minimal forms of the results in \eqref{22.3b1.22.long} are $1$ and $2$ and the new one
\begin{equation}\label{extraIGR_2}1\un{c}aT_1\to\to 1\_abaT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T_1\to\to 3bbcb\un{T_2}.\end{equation}
In addition, the residual origins are the same as \eqref{extra} becuase the starting point for the backward search is the same.
Similarly applying $F$ to $22\to 3b2\to 22$ gives
\begin{equation}\label{22.3b2.22.long}1\un{c}ababT_1\to\to 1\_abaT_2\left\{\begin{array}{l}\stackrel{b}{\Rightarrow}\left.\begin{array}{l}1\un{c}cabab\\2\un{a}cabab\\2\un{a}cbbab\end{array}\right\}T_1\to\to 3\_babaT_2\\\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}cabab\\3\un{c}cbbab\end{array}\right\}T_1\to\to 3bbcb\un{T_2}\end{array}\right..\end{equation} which is the same as \eqref{22.3b1.22.long} except that the symbol just before $T_1$ is $b$ instead of $a$, because the pointer is not interacting with this symbol. The results of this section can by truncation to the minimum number of symbols be written as $22\to 3\to 22\stackrel{F}{\Rightarrow}\{1, 2, \eqref{extraIGR_2}\}$ as above with the same two sets of residual origins \eqref{extra} and \eqref{extra2} to be included from both parts of \eqref{22.3.22} respectively.
In $22\to 3$, $T_1$ in $22$ must start with $aa$. This is inconsistent with $T_1$ starting with $c$ if $1$ precedes $22$, and $T_1$ starting with $ab$ if $22$ is preceded by any of $3$ $4$, $5$ and $7$, therefore $22\to 3$ can be preceded only by $8$, the only other option in Table~\ref{table4}.
\subsubsection{$8\to 22\to 3\to 22$}
This can be written as
\begin{equation}\label{8.22.3.22}2\un{a}T_1\to\to 1\_T_2\stackrel{8b}{\Rightarrow}1\un{a}aT_1\to\to 3\_bT_2\stackrel{b22\to 3\to 22}{\Rightarrow}\left.\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}T_1\to\to 1\_ababT_2\end{equation}
Now $F$ can be applied to this easily because the backward searching has already been done in the two cases above. In fact \eqref{8.22.3.22} only differs from \eqref{22.3.22} in that $T_2$ has the requirement to begin with $b$. Then it is easy to continue the computations of the RHS's to show that \begin{equation}\label{eq44}1\un{b}ababT_2\to 3\_bababT_2\text{ and }1\un{c}ababT_2\to 3bbbbb\un{T_2}.\end{equation}
and so $F$ applied to both parts of \eqref{8.22.3.22} are, in long form, \eqref{22.3b1.22.long} and \eqref{22.3b2.22.long} but with the $T_2$ strings modified as above, which will not affect the shortest forms of the $T_1$ strings. Reducing it to shortest form can be seen to yield the same result but with the $T_2$ strings modified i.e.
$1$, $2$ and \begin{equation}\label{extraIGR_1}1\un{c}aT_1\to\to 1\_ababT_2\stackrel{c}{\Rightarrow}\left.\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T_1\to\to 3bbbbb\un{T_2}.\end{equation}
Therefore \begin{equation}8\to 22\to \{3b1,3b2\}\to 22\stackrel{F}{\Rightarrow}\{1,2,\eqref{extraIGR_1}\}.\end{equation}
The results \eqref{extra} and \eqref{extra2} continue to apply in these cases because the backward searches are the same.
Because of \eqref{extra} and \eqref{extra2}, this analysis is not complete.
Referring again to \eqref{table4} shows that $8$ can be preceded only by all parts of $23$, $27$ and $30$.
\subsubsection{$\{23,27,30\}\to 8\to 22\to 3\to 22$}
Consider first starting with $23$. When this is followed by \eqref{8.22.3.22} this gives the result
\begin{equation}\label{23.8.22.3.22}1\un{c}aT_1\to\to 3\_T_2\stackrel{b^5}{\Rightarrow}\left.\begin{array}{l}1\un{c}abaaca\\1\un{c}ababca\\1\un{c}abaacb\\1\un{c}ababcb\end{array}\right\}T_1\to\to 1\_ababaT_2\end{equation}
Applying $F$ to the RHS of this can be started by doing the backward search first from $1\alpha\un{c}abaa$ and $1\alpha\un{c}abab$ as in \eqref{22.3.22} which have already been done. This resulted in \eqref{extra} and \eqref{extra2} together with results in \eqref{22.3b1.22.long} and \eqref{22.3b2.22.long}. The latter involve the pointer returning to the left hand end of the string, and so the above results will be unaffected when the extra symbols $ca$ and $cb$ are added to the right and the results are expressed with the minimum number of symbols. The RHS of the RHS of \eqref{23.8.22.3.22} has the same form as the RHS of the RHS of \eqref{22.3.22} therefore the shortest form of these results of $F$ will be same as before which are $1$ and $2$. In addition to this there could be results from the continuation of the backward search from \eqref{extra} and \eqref{extra2} by appending to these the strings $ca$ and $cb$ on the right.
First adding just $c$ to the right of \eqref{extra} gives just two results where the pointer reaches an end of the string: \begin{equation}\label{38_c}2\alpha caaab\un{c}T_1\text{ and }2\alpha caabb\un{c}T_1.\end{equation}
Again adding $a$ and $b$ in turn to the right hand end of the string and continuing the backward search gives in each case no resulting string where the pointer reaches an end. Therefore from \eqref{extra} there are no results of $F$. Now add $c$ to the right of \eqref{extra2} and continuing the backward search gives\begin{equation}\label{extra2_c}\left.\begin{array}{l}2\alpha cabab\un{c}\\2\alpha cabbb\un{c}\\2\alpha cbbab\un{c}\\2\alpha cbbbb\un{c}\end{array}\right\}T_1\end{equation}and \begin{equation}\label{extra3}1\un{a}bbccbcT_1\text{ with }\alpha = b\text{ and }2\un{b}bbccbcT_1\text { with }\alpha = c.\end{equation}
Now adding $a$ to the right of \eqref{extra2_c} and continuing the backward search gives
\begin{equation}\label{extra_ca}1\un{a}bbccacaT_1\text{ with }\alpha = b\text{ and }2\un{b}bbccacaT_1\text{ with }\alpha = c\end{equation}
Finally adding $b$ to the right of \eqref{extra2_c} and continuing the backward search gives
\begin{equation}\label{extra_cb}1\un{a}bbccacbT_1\text{ for }\alpha = b\end{equation}
The results \eqref{extra3} came from $1\un{c}ababc$ and involved the pointer moving between there and where it is in \eqref{extra2} with $c$ added on the right. In these paths the pointer cannot ever reach the end of the string because the backward searching algorithm halts when this happens, therefore the pointer can never get to the $c$ at the end, so this symbol is redundant and is the only one redundant, thus it must be removed. On the RHS's, putting $\alpha = b$ it is done in a single step. For $\alpha = c$, using \eqref{eq44}.2 it follows that \begin{equation}\label{eq_alpha_c}1\un{c}ababaT_2\to 3\_bababaT_2\end{equation} and this uses all the symbols written, therefore the following IGRs are obtained:
\begin{equation}1\un{c}ababT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{a}bbccbT_1\to\to 3\_bT_2\end{equation}
which is $4$ and
\begin{equation}1\un{c}ababT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}2\un{b}bbccbT_1\to\to 3\_bababaT_2.\end{equation} which is $14$.
Similarly from \eqref{extra_ca} in the backward searching, only the last symbol $a$ is redundant, and on the right, for $\alpha = b$ it is a single TM step, and for $\alpha = c$ \eqref{eq_alpha_c} applies, so the long form result
\begin{equation}1\un{c}ababcaT_1\to\to 1\_ababaT_2\left\{\begin{array}{l}\stackrel{b}{\Rightarrow} 1\un{a}bbccacaT_1\to\to 3\_bababaT_2\\\stackrel{c}{\Rightarrow}2\un{b}bbccacaT_1\to\to 3\_bababaT_2\end{array}\right.\end{equation}
reduces to
\begin{equation}1\un{c}ababcT_1\to\to 1\_T_2\stackrel{b}{\Rightarrow}1\un{a}bbccacT_1\to\to 3\_bT_2\end{equation}
i.e. $5$ and
\begin{equation}1\un{c}ababcT_1\to\to 1\_ababaT_2\stackrel{c}{\Rightarrow}2\un{b}bbccacT_1\to\to 3\_bababaT_2\end{equation} which is $15$.
The final result \eqref{extra_cb} again gives $5$ when expressed in the shortest form.
The results of this section so far can be summarised as \begin{equation}\label{summ23.8.22.3.22}\ldots 23\to 8\to 22\to 3\to 22\stackrel{F}{\Rightarrow}\{1,2,4,5,14,15\}\end{equation} because there are no residual origins with the pointer
oppsite $\alpha$, so no extra results that can occur as a result of any specialisations of $T_1$ and $T_2$ that would result from any prior IGR's in the sequence.
Next consider starting from $27$. When this is followed by \eqref{8.22.3.22} with the substitutions $T_1\to ccacT_1$ and $T_2\to aT_2$ it gives
\begin{equation}\label{27.8.22.3.22}1\un{c}abcT_1\to\to3\_T_2\stackrel{b^5}{\Rightarrow}\left\{\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}\left\{\begin{array}{l}ccac\\ccbc\end{array}\right\}T_1\to\to 1\_ababaT_2.\end{equation}
Because the RHS of this is a special case of the RHS of \eqref{22.3.22} the results of that section apply and the results $1$, $2$ will be unaffected by the extra symbols added after the results are reduced to minimal form. The former residual origins \eqref{extra} and \eqref{extra2} could give more results. Compared with \eqref{22.3.22}, the first extra $c$ to added to \eqref{extra} just gives \eqref{38_c} as above. The next $c$ added gives no extra results for the same reason as above. Now proceeding from \eqref{extra2}, the first $c$ added gives \eqref{extra2_c} and \eqref{extra3} as above. For the next $c$ added to these, \eqref{extra3} gives no new results but \eqref{extra2_c} does give just \begin{equation}\label{extra_cc}1\un{a}bbccacc\text{ for }\alpha = b\text{ and }2\un{b}bbccacc\text{ for }\alpha = c.\end{equation} By identifying the provenance of this result from $1\alpha\un{c}ababcc$ and noting that the final $c$ must be removed similar to the above argument, it follows that \eqref{extra_cc} reduces to the shortest forms which are again $5$ and $15$. Furthermore there are no more residual origins with the pointer opposite $\alpha$ so these results combined show that
\begin{equation}\label{summ27.8.22.3.22}\ldots 27\to 8\to 22\to 3\to 22\stackrel{F}{\Rightarrow}\{1,2,5,15\}\end{equation}
Consider starting from $30$. When this is followed by \eqref{8.22.3.22} this gives
\begin{equation}3\un{T_1}\to\to 3\_T_2\stackrel{b^5}{\Rightarrow}\left.\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}T_1\to\to 1\_ababaT_2.\end{equation} Again the backward search is as before and together with \eqref{eq_alpha_c} it is straightforward to show that $F$ applied to this gives $1$,$2$ and
$12$ together with the residual origins \eqref{extra} and \eqref{extra2} as before. Therefore preceding IGR's must be considered for this case.
$30$ can be preceded by just $12$,$16$,$36$,$39$.
\subsubsection{$x\to 30\to 8\to 22\to 3\to 22$}
The RHS of this for $x = 12$ is \begin{equation}\left.\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}\left\{\begin{array}{l}cca\\ccb\end{array}\right\}T_1\to\to 1\_abababababaT_2.\end{equation}
Following very similar reasoning to the above shows that the result of $F$ for this is as in \eqref{summ27.8.22.3.22} with no residual origins. This is a consequence of $1\un{c}abab$ being followed by $cc$ and is also true for $x$ being $16$, $36$, but not $39$.
i.e. \begin{equation}\{12,16,36\}\to 30\to 8\to 22\to 3\to 22\stackrel{F}{\Rightarrow} \{1,2,5,15\}\end{equation}
$4\to 22\to 3$ is impossible therefore so is $4\to 22\to 3\to 22$.
\subsubsection{$39\to 30\to 8\to 22\to 3\to 22$}
This is \begin{equation}\label{39.30.8.22.3.22}3\un{T_1}\to\to 3\_babT_2\stackrel{c}{\Rightarrow}3\un{c}T_1\to\to 3\_babaT_2\stackrel{b^5}{\Rightarrow}\left.\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}cT_1\to\to 1\_ababababaT_2\end{equation}
$F$ applied to this gives $1$,$2$,$4$,$14$ and \eqref{extra2_c}. Again because there are residual IGR's the search must continue back. The IGR's that can precede $39$ are $12$,$16$,$36$,$39$. In each of these cases, the LHS of the RHS has $c$ on the left. This implies that when substitutions are made into \eqref{39.30.8.22.3.22} to follow each of these cases in turn, $T_1$ is replaced by a string that begins with $c$. Therefore the RHS is of the form
\begin{equation}\left.\begin{array}{l}1\un{c}abaa\\1\un{c}abab\end{array}\right\}ccT_3\to\to 1\_ababaT_4\end{equation} where $T_3$ and $T_4$ are new strings dependent on $T_1$ and $T_2$ and on which case is being considered. Now applying $F$ the logic follows similarly to the analysis of \eqref{27.8.22.3.22} showing that the result is again $\{1,2,5,15\}$ i.e. \begin{equation}\ldots \{12,16,36,39\}\to 39\to 30\to 8\to 22\to 3\to 22\stackrel{F}{\Rightarrow}\{1,2,5,15\}.\end{equation}
Now there is no need to continue further back because there are now no residual origins.
The starting points of these chains of IGR's to generate all the IRR's must be the IGR's involved in the IRR(2) together with their associated contexts.
\begin{longtable}{c|c}
\caption{The IGR's and contexts that give on their RHS's all the IRR(2)\label{table5}}\\
IGR&Set of context pairs\\
\hline
$41$ &$(a,b)$\\
$22$&$(b,b)$\\
$40$&$(c,b)$\\
$8$&$(c,c)$\\
$9$&$(a,a),(b,a)$\\
$47$&$(c,)$\\
$45$&$(a,)$\\
$21$&$(c,)$\\
$10$&$(b,),(a,)$\\
\end{longtable}
\end{comment}
\section{Further simplification and LIGR's}
Returning to property 1 of Table~\ref{table3}, it appears that the left and right hand halves of the RHS of each IGR can be derived independently (it is only $\alpha$ that connects them), and the left hand sides (the origin of the LHS and the origin of the RHS) have a lot of repetition, many appearing multiple times, thus the presentation in Table~\ref{table3} is far from optimal although the list of IGR's given there for generating any IRR from the IRR(2) does now seem to be complete and can can be derived systematically up to any given length of the IRR's.
What is hinted at above is that there could be an alternative algorithm to generate the IGR's directly from each other by applying $F$ in these general cases for arbitrary strings $T_{\rm 1}$ and $T_{\rm 2}$. This became extremely complicated because of dealing with new origins and RHS's together. It is this that I want to arrive at by just considering at first the derivation of new origins for the IGR's, for which I introduce the new concept of LIGR (Left IGR) because the RHS's can always be filled in later just with forward computations.
The aim of this section will be to demonstrate this algorithm before formulating it precisely and hopefully show that if it does come to an end, then the LIGR's so obtained from a Turing Machine will be sufficient rules to allow the computation of all the IRR's to any level desired. Unfortunately in the present example it has as yet proved too difficult to complete this analysis.
\subsection{LIGR's\label{5.1}}
An LIGR or left IGR is the origin of the LHS of an IGR, and the origin of the RHS of the same IGR, combined with the symbol $\alpha$. For example IGR's $2$, $23$ have the common LIGR
\begin{equation}\label{ligr1}1\alpha\un{c}aT_1\stackrel{\alpha = b}{\leftarrow}\left.\begin{array}{l}2\un{a}ca\\2\un{a}cb\end{array}\right\}T_1.\end{equation} Similarly
\begin{equation}\label{ligr2}1\alpha\un{c}aT_1\stackrel{\alpha =c}{\leftarrow}\left.\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T_1\end{equation}
is common to IGR's $12$ and $20$. These examples show that in common with IGR's, LIGR's can have parts (labelled by $\alpha$) and sub-parts that will be labelled in lexicographical order of the strings with the most significant symbol (sorted first) being where the pointer is. Also the symbol $\alpha$ may be omitted for brevity because it is always at the opposite end of the string from $T_1$, which in the context of LIGR's will be called just $T$ because $T_{\rm 2}$ is not involved. For example if \eqref{ligr1} and \eqref{ligr2} are treated as parts of the complete LIGR $X$ then \eqref{ligr1} is $X.b$ and \eqref{ligr2} is $X.c$. The length of an LIGR will be the length of the symbol string on its right, which is one more than the length of the symbol string on the left assuming $\alpha$ is ommited.
This notation with the reverse facing arrow will be used because as usual the arrows ($\leftarrow$ or $\to$) indicate the direction of the computation of the TM as distinct from logical derivation indicated by $\Rightarrow$. Thus LIGR's are also reverse computation rules, but very special ones because they arise in the context of IGR's.
There are obvious advantages of treating IGR's in this way as can be seen in the drastically shortened list of results (12 LIGR's from Table~\ref{table3} not counting parts and sub-parts separately). Moreover if an LIGR (on its LHS) matches the origin of an IRR, $F$ applied to this IRR has as origins the result of the substitution for $T_1$ in the RHS of the LIGR, and its RHS can be computed directly from the original RHS using alpha of the LIGR. Thus the RHS's can be filled in later and do not need to be recorded in the rule for generating new IRR's from existing ones.
\subsection{\label{5.2}Sequences of LIGR's and $F$}
A sequence of LIGR's is a chain of LIGR's that can follow each other written with $\cdot$ between them so for example if\begin{equation}L_1= 1\un{c}aT\stackrel{b}{\leftarrow}\left.\begin{array}{l}2\un{a}ca\\2\un{a}cb\end{array}\right\}T.\end{equation}
\begin{equation}L_2 = 2\un{T}\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}T\\\stackrel{c}{\leftarrow}2\un{b}T\end{array}\right.\end{equation}
\begin{equation}L_3 = 1\un{T}\stackrel{b}{\leftarrow}1\un{c}T\end{equation}
then
\begin{equation}\begin{array}{l} L_{1.2} = 1\un{c}aT\stackrel{b}{\leftarrow}2\un{a}cbT\\
L_{2.1} = 2\un{T}\stackrel{b}{\leftarrow}1\un{a}T\end{array}\end{equation}
and the chain $L_{1.2}\cdot L_{2.1}\cdot L_3$ is the the result of the three substitutions of the LHS performed in that sequence giving
\begin{equation}\label{ligr}1\un{c}aT\leftarrow 2\un{a}cbT\leftarrow 1\un{a}acbT\leftarrow 1\un{c}aacbT\end{equation} so the combination is $1\un{c}aT\stackrel{bbb}{\leftarrow}1\un{c}aacbT.$
Similarly to the way in which $F$ was applied to sequences of IGR's combined together, this can obviously be done for sequences of LIGR's.
\begin{comment}
Now the result of $F$ will be defined as a pair $(F_{\rm 1},F_{\rm 2})$, the first component $F_{\rm 1}$ being the set of LIGR's as possible n'ext LIGR's in the sequence, and the second component $F_{\rm 2}$ being the set of residual CS's.
\end{comment}
The result of $F$ applied to a sequence of LIGR's of length 1 cannot give rise to any residual CS's because there is not enough ``room" and can be affected by adding an extra LIGR to the beginning of the sequence. To show this
suppose an LIGR or a sequence of LIGR's combined as above $X_1$ with $\alpha$ on the left has a sub-part of the form
\begin{equation}s_1\label{ligr3}\un{y_1}\ldots y_rT\stackrel{\alpha}{\leftarrow}s_2\un{z_1}\ldots z_{r+1}T.\end{equation}
Likewise let $X_2$ be\begin{equation}\label{ligr4}s'_1\un{y'_1}\ldots y'_{r'}T\stackrel{\alpha'}{\leftarrow}s'_2\un{z'_1}\ldots z'_{r'+1}T.\end{equation}
Then for the sequence $X_2\cdot X_1$ to be possible requires, $s'_2 = s_1$ and $\un{y_1}\ldots y_r$ is a substring of $\un{z'_1}\ldots z'_{r'+1}$ on the left, and $\alpha$ is on the left for $X_{\rm 2}$ too. The result of $X_2\cdot X_1$ is
\begin{equation}\label{ligr5}s'_1\un{y'_1}\ldots y'_{r'}T\stackrel{\alpha'}{\leftarrow}s'_2\un{z'_1}\ldots z'_{r'+1}T =s_1\un{y_1}\ldots y_rz'_{r+1}\ldots z'_{r'+1}T\stackrel{\alpha}{\leftarrow}s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_{r'+1}T.\end{equation}
Comparing \eqref{ligr3} with \eqref{ligr5} shows the effect on $X_1$ of preceding it with $X_2$ which is to add extra symbols next to $T$ in its right hand member. Therefore the results of the backward search starting from the RHS of \eqref{ligr3} are reproduced when started from the RHS of \eqref{ligr5} and shortened to the shortest form provided the pointer ends up at $\alpha$; these give rise to LIGR's. In addition there may be some extra LIGR's resulting from the pointer reaching the extra symbols which may be classified by the position of the rightmost symbol reached. Crucially, this happens only when $F$ applied to $X_{\rm 1}$ leads to cases in the backward search when the pointer ends up at the opposite end of the string from $\alpha$ i.e. condition 2 is reached because the above searches can then be truncated when they reach the opposite end from $\alpha$. These were termed residual CS's because they are cases that do not lead directly to any more IGR's and LIGR's but indicate the possibility of them if the sequence of LIGR's to which $F$ is applied increases in length as a result of a preceding LIGR appended to the sequence in question.
Finally, there may be results of this where the pointer ends up at the opposite end of the string from $\alpha$ i.e. the pointer goes right when the rightmost symbol is reached.
These are the new residual CS's in the result of $F$ applied to \eqref{ligr5} and will be designated as $F_2(X_{\rm 2}\cdot X_{\rm 1})$.
Therefore it makes sense to introduce $\Delta F_{\rm 1}$ as the set of extra LIGR's from $F$, as a result of adding an extra LIGR $Y_{\rm 1}$ at the beginning of the sequence where $S=X_{\rm 1}\cdot X_{\rm 2}\ldots\cdot X_{\rm n}$ is a sequence of LIGR's:
\begin{equation}\label{ligr6}\Delta F_1(Y_1,S)=F_1(Y_1\cdot S)\setminus F_1(S).\end{equation}
In this notation the result of the preceding paragraph can be written as \begin{equation}F_{\rm 2}(S)=\emptyset\Rightarrow \Delta F_1(Y_1,S)=\emptyset.\end{equation} The converse is not true because it could be that there are some reverse search paths that go beyond the symbols in $S$ but none of them go back to $\alpha$. In this case $F_{\rm 2}(Y_{\rm 1}\cdot S)\ne\emptyset$ or some of these reverse search paths just reach an end because at some point no reverse TM step is possible.
Here the result of $F$ applied to a sequence of LIGR's was split into two components $F=(F_{\rm 1},F_{\rm 2})$.
Also the result of $F$ for a collection of LIGR's in a sequence is defined as the result of $F$ for the combined LIGR, which actually only depends on the its RHS and results from applying the backward search algorithm to it. A consequence of this is that the arguments of $F$ can be written in different ways e.g. the sequence of LIGR's can be replaced by the equivalent sequence of symbols in the RHS of the combined LIGR.
\begin{comment}
Consider for example the sequence $14\cdot3$ can be written as \begin{equation}\label{3.22}1\un{c}aaT\stackrel{b}{\leftarrow}1\un{a}baaT\stackrel{b}{\leftarrow}1\un{c}abaaT.\end{equation} after substituting
$\un{a}baaT$ for $T$ in LIGR $3$.
Applying $F$ to this i.e. using $1\un{c}abaa$ as the origin to start from, the backward search gives the initial result i.e. without reducing the strings to minimal form
\begin{equation}\label{3b1.22.long}1\un{c}abaaT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}\left\{\begin{array}{l}1\un{c}cabaa\\2\un{a}cabaa\\2\un{a}cbbaa\end{array}\right\}T\\[18pt]\stackrel{c}{\leftarrow}\left\{\begin{array}{l}3\un{c}cabaa\\3\un{c}cbbaa\end{array}\right\}T\end{array}\right..\end{equation}
By tracking the rightmost position of the pointer in each branch in the backward search starting from $1\alpha \un{c}abaaT$, with $\alpha$ indicated on the backward arrows, the minimal forms of the results in \eqref{3b1.22.long} turn out to be $3$, $10$, $11$, $12$ and $13$ respectively.
\begin{equation}\label{extraIGR}1\un{c}aT\stackrel{c}{\leftarrow}\left\{\begin{array}{l}3\un{c}ca\\3\un{c}cb\end{array}\right\}T.\end{equation}
Along with the above are the residual origins\begin{equation}\label{extra}\left.\begin{array}{l}3\alpha caab\un{a}\\3\alpha caab\un{b}\\3\alpha cabb\un{a}\\3\alpha cabb\un{b}\end{array}\right\}T\end{equation} also derived from $14\cdot3$
\end{comment}
\subsection{\label{apply_f}Evaluating \eqref{ligr6} one extra symbol at a time}
The following is a description of the above calculation taken one symbol at a time. It can be applied when several symbols are added in one step from a single LIGR as was the original intention, or when a sequence of LIGR's is added that each contribute just one symbol etc..
The result of \eqref{ligr6} can obviously be obtained by adding each symbol separately, so in the
general case above the extra symbols can also be called $z'_{r+1}\ldots z'_{r'+1}$ and one can write:
\begin{equation}\label{ligr7}\begin{array}{l}F_1(Y_1\cdot S)=F_1(s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_{r'+1})\\
= \left[\bigcup_{i=r+1}^{i=r'+1}
\Delta F_1(z'_i,s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_{i-1})\right]\cup F_1(s_2\un{z_1}\ldots z_{r+1})\end{array}\end{equation}
where the first term of the union is \eqref{ligr6} and the second term is $F_1(S).$
Each step uses the residual CS's from the previous step. These residual CS's with the single extra symbol are the starting points of the continuing backward search which would of course stop if at some point there were no more residual CS's.
In more detail, in order to calculate \begin{equation}\Delta F_1(z'_i,s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_{i-1})\end{equation}
which is by definition \begin{equation}F_1(s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_i)\setminus F_1(s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_{i-1}),\end{equation}
in the backward search the pointer must reach $z'_i$ before ending up at the right or left end (otherwise duplicate results are obtained that are to be eliminated), therefore the backward search can start from \begin{equation}F_2(s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_{i-1})\un{z'_i}\end{equation} where the last symbol is concatenated to the residual results of $F_2$.
If the pointer reaches $\alpha$ the result is a new LIGR otherwise it gives a residual CS which is in
\begin{equation}F_2(s_2\un{z_1}\ldots z_{r+1}z'_{r+1}\ldots z'_i).\end{equation}
Putting ${\it i = r}+{\rm 1}$ initially, then this shows that the backward search starts from $F_2(s_2\un{z_1}\ldots z_{r+1})\un{z'_{r+1}}$ i.e. the set of residual CS's from the initial backward search for $S$ each appended with the first extra symbol $z'_{r+1}$ on the right. If the pointer reaches $\alpha$ as the backward search continues, this gives a new LIGR otherwise it gives a residual CS in $F_2(s_2\un{z_1}\ldots z_{r+1}z'_{r+1})$ if the pointer reaches the opposite end of the string of symbols, or comes to a point where the backward search can go no further or end in an infinite stationary loop. Then for ${\it i = r}+{\rm 2}$, the backward search starts from this appended with $z'_{r+2}$ on the right. Again the backward search continues either the pointer reaches $\alpha$ giving a new LIGR, or away from it giving a residual CS in $F_2(s_2\un{z_1}\ldots z_{r+1}z'_{r+1}z'_{r+2})$ etc..
This continues until all the new symbols have been added and all possible backward search paths are followed at each stage. If at any stage there are no residual CS's in $F_2$ it terminates. All the new LIGR's are accumulated and any final residual CS's are noted. Naturally, there is an equivalent version of this if $\alpha$ is on the right.
\subsection{The procedure for finding the LIGR's for a TM}
This algorithm is extremely complicated and is very hard to describe so the reader is not expected to understand this immediately. For this reason I attempt to do so here in this section and then the algorithm is applied to TM \eqref{tm2} in detail in Section \ref{5.5} when it should become clearer.
\begin{alg}\label{alg5.1}
The algorithm $F$ applied repeatedly can generate all the IRR's starting with members of IRR(2) therefore
the first step is to find $L$ the set of LIGR's corresponding to the formation of the members of IRR(3) from those of IRR(2) by applying $F$. Doing this starts with putting the arbitrary symbol $\alpha$ at one end of the pair of symbols in the origin of the member of IRR(2) and the backward search starts with the pointer at the middle symbol. A single reverse TM step gives a member of IRR(3) if the pointer moves to $\alpha$ and if it goes the other way condition 2 occurs giving a residual CS, so only one symbol is involved therefore the reduced form (the LIGR) that results (if the pointer goes to $\alpha$) must have length 1. The RHS of each of these LIGR's of length 1 already is a residual CS because the pointer is already adjacent to $T$.
Next the LIGR's involved in forming the IRR$({\it n}+{\rm 1})$ from the IRR$({\it n})$ need to be found for all ${\it n}\ge{\rm 3}$. This can be done by searching for all LIGR's that can follow sequences of LIGR's that have already been found. This involves applying $F$ to an arbitrary sequence $S$ of such of LIGR's substitiuted into each other as in Section~\ref{5.2}. This has to be done until closure i.e. until no more LIGR's can be found if this is repeated one more time. For this, as shown in Section~\ref{5.2}, $\Delta F_1$ and $F_2$ need to be found only if the previous $F_2\ne\emptyset$
\begin{comment}Then the following recursive function is applied to each of the LIGR's found as the initial values of the sequences $S$ of LIGR's.
Applying the procedure to $S$ starts as follows.
\end{comment}
i.e. only if $F$ applied to $S$ gives $F_2(S)\ne\emptyset$, carry out $F$ to obtain $\Delta F_1(X\cdot S)$ and $F_2(X\cdot S)$ for each LIGR $X$ that can precede $S$ where the requirement for precedence is given in \eqref{ligr5}. This calculation can start from the previous $F_2$ with the substitution made for $T$ indicated by $X$. This condition will be met for each of the initial set of LIGR's in $L$ because as shown above their RHS's each have the form of a residual CS. Any new LIGR's from $\Delta F_1(X\cdot S)$ are added to $L$. For any members of $F_2(X\cdot S)$ apply this algorithm recursively i.e. with $X\cdot S$ taking the place of $S$ above etc.. It is expected that this algorithm will terminate because the matching criterion for new LIGR's that can be prepended to the sequence gets increasingly stringent as the length of the strings increases. If this happens repeat this algorithm the ``grand search" with the new enlarged set $L$ of LIGR's. This should in fact be just to add to the previous results instead of repeating them because the previous LIGR's are still in $L$. Repeat this ``grand search" until the set of extra LIGR's added to $L$ in one cycle is empty.
\end{alg}
\begin{comment}
The main part of this algorithm is to find, for each sequence of LIGR's that can be substituted into each other in sequence as in \eqref{ligr}, what the next LIGR in the sequence could be by applying the backward search i.e. $F$ as usual. For this $\Delta F_1$ and $F_2$ need to be found only if the previous $F_2\ne\emptyset$.
The result of $\Delta F_1$ adds to the set of LIGR's if any new ones have been found and the grand search continues back only if the current $F_2\ne\emptyset$.
To obtain $\Delta F_1$ the methods of subsection~\ref{apply_f} apply if needed. If $F_2=\emptyset$ then the grand search continues with the next possible sequence of LIGR's according to the following: the current first LIGR in the sequence is replaced by its successor if there is one according to a defined ordering. If not, go back one step down the grand search tree by deleting the current first member of the sequence and repeat this procedure.
LIGR, or one or more LIGR's are produced some of which may be new ones to be added to the set.
If this also yields any residual CS's, this implies that an extra LIGR added at the beginning of the sequence could result in extra LIGR's as a result of applying $F$. All possible preceding LIGR's one at a time must be prepended to the sequence being studied which is checked for following LIGR's using $F$ etc. and recursively. If such a sequence of LIGR's does not have any residual CS's in the result of $F$, the grand search continues from the next sequence of LIGR's to be checked in some pre-defined order. This continues until, if this procedure terminates, every possible sequence of LIGR's has been analysed to find all the possible subsequent LIGR's that are possible. In order to do this the current set of LIGR's has to be maintained together with the set of LIGR's that can precede each LIGR.
\end{comment}
\begin{Definition}
A finite set of LIGR's $Z$ is closed under $F$ if for any sequence of members of $Z$ that can be substituted into one another in sequence as in \eqref{ligr}, the backward search $F$ applied to the result of this generates results that are each a member of the set $Z$.
\end{Definition}
\begin{Theorem}
If there is a finite set $Z$ of LIGR's for a Turing Machine that is closed under $F$ as described above and includes all the LIGR's involved in obtaining the set IRR(3) from the set IRR(2) then every IRR for that TM can be obtained from a member of IRR(2) by a sequence of applications of LIGR's each in $Z$ as described in Section~\ref{5.2}.
\end{Theorem}
It is also obvious that no LIGR's could be removed from this set $Z$ and $Z$ still have this property because members of $Z$ are only put there when they are required.
\begin{proof}
Consider deriving the members of IRR(4) from IRR(3). This can be done by applying $F$ to each member of IRR(3) and accumulating all the results. Applying $F$ gives results that come from members of $Z$ because any LIGR following an LIGR in $Z$ is also in $Z$ by the closure property. Likewise deriving members of IRR(5) involve applying $F$ to members of IRR(4) that themselves have been derived using a pair of LIGR's. Again all such derivations of LIGR's that can follow this sequence are in $Z$ by the closure property etc..
\end{proof}
This all assumes that $Z$ is finite.
The case if the closure algorithm does not terminate leading to an infinite set $Z$ closed under $F$
might be interesting.
\begin{comment}
&\begin{array}{c}\text{{\rm which can be grouped}}\\\text{\rm together as}\end{array}&
\begin{array}{l}
1\un{T}\left\{\begin{array}{l}\stackrel{a}{\leftarrow}\left\{\begin{array}{l}3T\un{a}\\3T\un{b}\end{array}\right.\\[10pt]\stackrel{c}{\leftarrow}2T\un{c}\end{array}\right.\\[30pt]1\un{T}\stackrel{b}{\leftarrow}1\un{c}T\\[10pt]
2\un{T}\left\{\begin{array}{l}\stackrel{b}{\leftarrow} 1\un{a}T\\\stackrel{c}{\leftarrow}2\un{b}T\end{array}\right.\\[20pt]
3\un{T}\left\{\begin{array}{l}\stackrel{b}{\leftarrow}2\un{a}T\\\stackrel{c}{\leftarrow}3\un{c}T\end{array}\right.\\[20pt]
3\un{T}\stackrel{b}{\leftarrow}1T\un{b}\end{array}\end{array}\end{equation}
\end{comment}
The remainder of this section contains the application of Algorithm~\ref{alg5.1} to the example \eqref{tm2}.
The results are not all presented in the order in which they were derived i.e. there are forward references to LIGR's that have not yet been derived. This is because $L$ is increasing in size as the algorithm proceeds and to avoid duplication, the results are presented assuming the current $L$ is the final one and in the order determined by the grand search i.e.``depth first" (if not the results will be added to). This all assumes that the final $L$ is finite. It will soon be clear that it is useful throughout this section to use the symbol $d$ to mean eaither $a$ or $b$.
That there is a finite number of LIGR's has been strongly suggested in the present case by the computer results that established Table~\ref{table3} using any value of the maximum length of the strings involved ({\it n}) between 10 and 16 and show the same result. The computations rapidly increase in number and time taken as {\it n} increases.
Checking the arguments requires the derivation route from the initial LIGR's in $L$ to all the final ones which will be given so that the results can all be checked.
The following are the 7 LIGR's that arise from the derivation of the IRR(3) from the IRR(2):
\begin{equation}\begin{array}{lcl}
1&2\un{T}\stackrel{b}{\leftarrow}1\un{a}T\\
2&3\un{T}\stackrel{b}{\leftarrow}1T\un{b}\\
3&1\un{T}\stackrel{b}{\leftarrow}1\un{c}T\\
4&2\un{T}\stackrel{c}{\leftarrow}2\un{b}T\\
5&1\un{T}\stackrel{c}{\leftarrow}2T\un{c}\\
6&1\un{T}\stackrel{a}{\leftarrow}3T\un{a}\\
7&1\un{T}\stackrel{a}{\leftarrow}3T\un{b}\\
\end{array}.\end{equation}
The relation ``can possibly be preceded by" on the LIGR's is also being discovered continually as the LIGR's are being discovered. The criterion is that the RHS of the preceding LIGR must match the LHS of the original LIGR in state, string of symbols and direction. The relation ``can possibly be preceded by" initially among the 7 LIGR's is given by
\begin{equation}\begin{array}{ll}
1\text{\hspace{1cm}}&4\\
2\text{\hspace{1cm}}&6,7\\
3\text{\hspace{1cm}}&1,3\\
4\text{\hspace{1cm}}&4\\
5\text{\hspace{1cm}}&2\\
6\text{\hspace{1cm}}&2\\
7\text{\hspace{1cm}}&2\\
\end{array}.\end{equation}
While carrying out the main argument the following results emerged and are collected here for convenience because they may need to be referred to anywhere throughout the main argument.
As explained above, it is not now obvious why these propositions are needed, but this becomes clear later on.
\begin{Lemma}\label{lemma}
The reversed TM cannot cross the symbol $a$ going left or the pairs of symbols $cx$ going right where $x$ is any symbol.
\end{Lemma}
\begin{proof}
There is no reverse TM step of the form $xa\_\leftarrow CS$ therefore
the pointer cannot get left of the $a$ which is maintained. Also if the pointer were to reach just left of the symbol $c$ a further reverse step to the right is only possible if it is to the CS $2\un{c}$ (using $2\un{c}\to 1\_c$ in reverse). The next reverse TM step must be to the left if at all because there are no TM steps of the form $CS\to 2\_x$ where $x$ is any symbol. Thus the symbols $cx$ are maintained.\end{proof}
\begin{Lemma}\label{lemma2}
The backward search from any CS of the form $1Ta\left\{\begin{array}{l}a\\b\end{array}\right\}b\un{a}aa\alpha$
cannot lead to any new LIGR's or residual CS's provided the string $T$ contains the symbol $a$.
\end{Lemma}
\begin{proof} This is by continuing the backward search from there and using Lemma~\eqref{lemma}. This gives the following tree
\begin{equation}1Tadb\un{a}aa\alpha\leftarrow\left\{\begin{array}{l}1Tad\un{c}a^3\alpha\leftarrow\left\{\begin{array}{l}3Tadc\un{d}a^2\alpha\leftarrow 3Tad\un{c}da^2\alpha\leftarrow \left\{\begin{array}{l}2Ta\un{a}cda^2\alpha\\1Tadc\un{b}a^2\alpha *\end{array}\right.\\1Ta\un{c}ca^3\alpha\end{array}\right.\\3Tadba\un{d}a\alpha\end{array}\right.\end{equation}
\begin{equation}1Tadc\un{b}a^2\alpha\leftarrow3Tadcb\un{d}a\alpha\leftarrow 2Tadc\un{a}da\alpha\leftarrow
2Tad\un{b}ada\alpha\leftarrow 1Ta\un{a}bada\alpha\end{equation}where the computation stopped whenever either no reverse TM step is possible, or when by Lemma~\eqref{lemma} the pointer cannot go beyond the string as a result of continued backward searching. Because all branches of the tree do eventually lead to a halt, no LIGR's or residual CS's can result from further backward searching.
\end{proof}
\begin{Lemma}\label{lemma3}
Backward searching starting from any CS of the form $1Td\un{c}abada\alpha$ leads to exactly the following set of CS's regardless of the arbitary string $T$ in addition to possible CS's with the pointer at the left depending on $T$:
\begin{equation}\begin{array}{l}
1Tdca^2dbd\un{b}\\3Tdca^3db\un{d}\\2Tdca^3db\un{c}\\1Tdcdbdbd\un{b}\\3Tdcdcbdb\un{d}\\2Tdcdcbdb\un{c}\\3Tdcdbadb\un{d}\\2Tdcdbadb\un{c}\end{array}\end{equation}
These are related to the set of LIGR's in {\rm \ref{newligrs1}.20-23}.
\end{Lemma}
\newpage
\begin{proof}
The backward search stops if either (1) the pointer can be shown not to get to the right because of $cx$ on the right of the pointer or (2) no further backward TM steps are possible or (3) the end of the known symbols on the string is reached or (4) a stationary cycle is reached. The numbers after * indicate continuations.
\begin{equation}\begin{array}{l}1Td\un{c}abada\alpha\leftarrow\left\{\begin{array}{l}1T\un{c}cabada\alpha\\3Tdc\un{d}
bada\alpha\leftarrow\left\{\begin{array}{l}3Td\un{c}dbada\alpha\leftarrow\left\{\begin{array}{l}2T\un{a}cdbada\alpha\\1Tdc\un{b}
bada\alpha\end{array}\right.\\ 1Tdcd\un{b}ada\alpha\leftarrow\left\{\begin{array}{l}1Tdc\un{c}
bada\alpha\\3Tdcdb\un{d}da\alpha *1
\end{array}\right.\end{array}
\right.\end{array}\right.\\[40pt]
*1\leftarrow\left\{\begin{array}{l}2Tdcd\un{a}dda\alpha\leftarrow 1Tdc\un{a}adda\alpha\leftarrow3Tdca\un{d}dda\alpha\leftarrow 1Tdcad\un{b}da\alpha*2\\1Tdcdbd\un{b}a\alpha*5\end{array}\right.\\[20pt]
*2\leftarrow\left\{\begin{array}{l}1Tdca\un{c}bda\alpha\\3Tdcadb\un{d}a\alpha\leftarrow2Tdcad\un{a}da\alpha\leftarrow1Tdca\un{a}ada\alpha\leftarrow3Tdcaa\un{d}da\alpha*3\end{array}\right.\\[20pt]
*3\leftarrow 1Tdcaad\un{b}a\alpha\leftarrow\left\{\begin{array}{l}1Tdcaa\un{c}ba\alpha\\3Tdcaadb\un{d}
\alpha\leftarrow\left\{\begin{array}{l}2dca^2d\un{a}d\alpha\leftarrow1Tdcaa\un{a}ad\alpha*4\\1Tdca^2dbd\un{b}\end{array}
\right.\end{array}\right.\\[30pt]
*4\leftarrow3Tdca^3\un{d}d\alpha\leftarrow1Tdca^3d\un{b}\alpha\leftarrow\left\{\begin{array}{l}1Tdca^3\un{c}b\alpha\\3Tdca^3db\un{d}\\2Tdca^3db\un{c}\end{array}\right.\\[20pt]
*5\leftarrow\left\{\begin{array}{l}1Tdcdb\un{c}ba\alpha\leftarrow 1Tdcd\un{c}cba\alpha\\
3Tdcdbdb\un{d}\alpha\leftarrow\left\{\begin{array}{l}2Tdcdbd\un{a}d\alpha\leftarrow1Tdcdb\un{a}ad\alpha\leftarrow\left\{\begin{array}{l}
1Tdcd\un{c}aad\alpha*6\\3Tdcdba\un{d}d\alpha*8\end{array}\right.\\1Tdcdbdbd\un{b}\end{array}\right.\end{array}\right.\\[30pt]
*6\leftarrow\left\{\begin{array}{l}1Tdc\un{c}caad\alpha\\3Tdcdc\un{d}ad\alpha\leftarrow3Tdcd\un{c}dad\alpha\leftarrow\left\{\begin{array}{l}2Tdc\un{a}cdad\alpha\\1Tdcdc\un{b}ad\alpha\leftarrow 3Tdcdcb\un{d}d\alpha*7\end{array}\right.\end{array}\right.\\[25pt]
*7\leftarrow\left\{\begin{array}{l}2Tdcdc\un{a}dd\alpha\leftarrow2Tdcd\un{b}
add\alpha\leftarrow1Tdc\un{a}badd\alpha\\[10pt]1Tdcdcbd\un{b}\alpha\leftarrow\left\{\begin{array}{l}1Tdcdcb\un{c}
b\alpha\leftarrow1Tdcdc\un{c}cb\alpha\\3Tdcdcbdb\un{d}\\2Tdcdcbdb\un{c}\end{array}\right.\end{array}\right.\\[35pt]
*8\leftarrow1Tdcdbad\un{b}\alpha\leftarrow\left\{\begin{array}{l}1Tdcdba\un{c}b\alpha\\3Tdcdbadb\un{d}\\2Tdcdbadb\un{c}\end{array}\right.\end{array}\end{equation}
\end{proof}
\subsection{\label{5.5}The main argument}
Due to the problem with presenting this and the forward references mentioned above,
in the following the numbers of LIGR's refer to the LIGR's listed in \eqref{newligrs1} which is the most up to date list of LIGR's obtained by Algorithm~\ref{alg5.1} applied to TM \eqref{tm2}.
Rather than repeating the phrase ``Applying $F$ to the sequence of LIGR's $X$ gives $\ldots$" on many occasions it will be shortened to $X\stackrel{F}{\Rightarrow}\ldots$. Another notation that could be useful is for ``there are no residual CS's in this result" because it implies that that branch of the grand search ends because no preceding LIGR's can generate any new LIGR's from it by $F$. It can be written as just $\dashv$.
\subsubsection{Sequences ending with LIGR $1$}
Applying $F$ to $1$ gives just
$1\alpha\un{a}T\stackrel{b}{\leftarrow}1\un{c}aT$ i.e. LIGR $3$ i.e. $1\stackrel{F}{\Rightarrow} 3$. Clearly applying $F$ to an LIGR of length 1 as is done here could possibly lead to more results if $T$ is specialised by giving a symbol at one end of the string (here the left end) therefore preceding LIGR's must be considered. LIGR 1 can be preceded by LIGR $4$ giving $4\cdot 1$ having the combined effect
$3\un{T}\stackrel{b}{\leftarrow}2\un{a}T\stackrel{b}{\leftarrow}1\un{a}aT$ i.e. $3\un{T}\stackrel{bb}{\leftarrow}1\un{a}aT$ and $4\cdot 1\stackrel{F}{\Rightarrow}3$ because $F$ gives the calculation
\begin{equation}\label{4to1}1\alpha\un{a}aT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{c}aaT\\\leftarrow\left\{\begin{array}{l}3\alpha a\un{a}T\\3\alpha a\un{b}T\end{array}\right.\end{array}\right.\text{ i.e. }1\alpha\un{a}aT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{c}aaT\\\leftarrow
3\alpha a\un{d}T\end{array}\right.\end{equation}
The first part of this is LIGR $3$, and the second part is a pair of residual CS's. By specialising this by giving the first symbol(s) of $T$, the first result will not generate any new LIGR's after reducing the result to its shortest form, the result will merely be replicated, but for the second part it is possible that the reverse computation could take the pointer back to $\alpha$ and so generate more new LIGR's so the search has to continue back, so we have thus far \begin{equation}\label{eq53}\begin{array}{c}\ldots1\stackrel{F}{\Rightarrow}\{3\}\\\ldots\cdot 4\cdot 1\stackrel{F}{\Rightarrow}\{3\}\end{array}.\end{equation}
The second member of this is related to its first member because any results of $F$ from the first part must be included in the results of the second part as happens here but the residual CS's are not the primary result of $F$ and are not included in \eqref{eq53}.2. There are residual CS's so any LIGR's that can precede $4\cdot 1$ must be considered and $F$ must be applied to all these.
The LIGR's that can precede $4$ are just $9$,$12$ and $13$. The sequence $9\cdot 4\cdot 1$ gives $3\un{T}\stackrel{c}{\leftarrow}3\un{c}T\leftarrow 1\un{a}acT$. Applying $F$ to this starts from (from \eqref{4to1} with the substitiution given by LIGR $9$)
$1\alpha \un{a}acT\leftarrow3\alpha a\un{d}cT$
in addition to $3$ as above and $\Delta F_1$ is just the result of this backward search from
$3\alpha a\un{d}cT$ and because the computation cannot go back from there $\Delta F_1(9,4\cdot 1)=\emptyset$ and $F_2(9\cdot 4\cdot 1)=\emptyset$. Therefore there are no results of $F$ and it is
now it is clear that no preceding LIGR's specialising this $T$ can give any results of $F$, so the search for new results of $F$ stops in this branch of the grand search tree. \begin{comment}This will be expressed as $9\cdot4\cdot 1\stackrel{\Delta F}{\Rightarrow}\dashv$\end{comment}
The sequences $\{12,13\}\cdot 4\cdot 1$ have the effect $1\un{c}aT\leftarrow 1\un{a}accdT$ and applying $F$ gives $1\alpha\un{a}accdT\leftarrow 3\alpha a\un{d}ccdT$ from which there are no further backward steps so there are no new LIGR's or residual CS's and these branches of the grand search end i.e. $\Delta F_1(\{12,13\},4\cdot 1)=F_2(\{12,13\}\cdot 4\cdot 1)=\emptyset$. This completes the analysis for all sequences that can precede $4\cdot 1$ therefore
the next sequence of LIGR's to be considered is $5\cdot 1$ i.e. $2\un{T}\leftarrow 2\un{b}T\leftarrow 1\un{a}bT.$
The computation of $F$ starts from $1\alpha\un{a}bT$ and gives no result other than LIGR $3$, so
$\Delta F_1(5,1)=F_2(5\cdot 1)=\emptyset$. Next $10\cdot 1$ must be considered which is $1\un{c}aT\leftarrow 2\un{a}caT\leftarrow 1\un{a}acaT$. \begin{equation}10\cdot 1\stackrel{F}{\Rightarrow} 1\alpha\un{a}acaT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{c}aacaT\\3\alpha a\un{d}caT\end{array}\right..\end{equation} which is also a special case of \eqref{4to1}. The first of these is just LIGR $3$ and the second cannot continue, so there are no new LIGR's from preceding $1$ by $10$ i.e. $\Delta F_1(10,1)=F_2(10\cdot 1)=\emptyset$. Next consider $11\cdot 1$ which is $1\un{c}aT\leftarrow 2\un{a}cbT\leftarrow 1\un{a}acbT$ and applying $F$ gives a result practically the same as above with the same conclusion. It is not too difficult to show that the same results hold for all the other LIGR's that could precede LIGR $1$ and all the results starting with $F$ applied to $5\cdot 1$ in this paragraph can be summarised as
\begin{equation}\Delta F_1(\{5,10,11,16,17,19\}, 1)=F_2(\{5,10,11,16,17,19\}\cdot 1)=\emptyset.\end{equation}
This exhausts all search trees in the grand search starting from LIGR $1$.
\subsubsection{Sequences ending with LIGR $2$}
Next consider applying $F$ to sequences ending with $2$ which is
$3\un{T}\stackrel{b}{\leftarrow}1T\un{b}.$ $F$ applied to this gives \begin{equation}\label{eq96}1T\un{b}\alpha\left\{\begin{array}{l}\stackrel{a}{\leftarrow} 3Tb\un{d}\\
\stackrel{c}{\leftarrow}2Tb\un{c}\end{array}\right.\end{equation} which are LIGR's $6$,$7$, and $8$ so \begin{equation}2\stackrel{F}{\Rightarrow}\{6,7,8\}.\end{equation} The last symbol of $T$ in \eqref{eq96} could affect this result so LIGR's preceding $2$ must be considered which are $7$ and $8$, $21$ and $23.0-15$.
The sequence $7\cdot 2$ is $1\un{T}\stackrel{a}{\leftarrow}3T\un{a}\leftarrow 1Ta\un{b}$ and applying $F$ gives
the same set i.e. LIGR's $6,7,8$ and no residual CS's i.e. $\Delta F_1(7, 2)=F_2(7\cdot 2)=\emptyset$.
This is because the pointer cannot move left in the reverse computation regardless of any other specialisations of $T$ resulting from preceding LIGR's. Consider $8\cdot 2$ which is $1\un{T}\stackrel{a}{\leftarrow} 3T\un{b}\leftarrow 1Tb\un{b}$. $F$ gives $1Tb\un{b}\alpha\leftarrow 1T\un{c}b\alpha$ in addition to $6$,$7$, and $8$ and so can be potentially specialised further i.e. $\Delta F_1(8, 2)=\emptyset$ and $F_2(8\cdot 2)=1T\un{c}b\alpha$.
LIGR $8$ can only be preceded by $2$ and $20$ so the next sequence to be considered in the grand search is $2\cdot8\cdot 2$ which is $3\un{T}\stackrel{b}{\leftarrow}1T\un{b}\leftarrow 1Tbb\un{b}$. $F$ applied to this gives \begin{equation}\label{282}1Tbb\un{b}\alpha\leftarrow 1Tb\un{c}b\alpha\leftarrow 1T\un{c}cb\alpha\end{equation} i.e.
$\Delta F_1(2, 8\cdot 2)=\emptyset$ and $F_2(2\cdot 8\cdot 2)=1T\un{c}cb\alpha$.
This residual CS by Lemma~\eqref{lemma} cannot lead to any new LIGR's because the pointer can never reach $\alpha$ by the reverse TM computation however many preceding LIGR's are added to the sequence. Therefore there is no point in continuing grand search along this branch. This is a short cut that was not anticipated in the general algorithm \ref{alg5.1}. Next consider $20.8.2$ having the effect
$3Tb^5\un{a}\leftarrow 1Tc\left\{\begin{array}{c}db\\aa\end{array}\right\}dbdbb\un{b}$.
Applying $F$ to this gives a result of the same form as in \eqref{282} therefore the same conclusion follows and the grand search continues from $21\cdot 2$ which has the effect $3Tb^5\un{a}\leftarrow 1Tca^3dbd\un{b}$. Applying $F$ to this gives some results of the form \eqref{282} not leading to any new results as above or with the symbol $a$ in the rightmost but one position. This is of the form $1Tba\un{b}$ having no preceding TM step to the left in $F$ hence $F$ applied to this gives $\Delta F_1=F_2=\emptyset$.
The CS $23.2$ has the effect $3Tb^5\un{a}\leftarrow 3Tcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}db\un{d}\leftarrow 1Tcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}dbd\un{b}$.
Applying $F$ to this gives\newline
$1Tcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}dbd\un{b}\alpha\stackrel{b}{\leftarrow}1Tcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}db\un{c}b\alpha\leftarrow 1Tcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}d\un{c}cb\alpha$. There is no point going any further with the algorithm $F$ because from this CS, by Lemma~\eqref{lemma} it is not possible for the pointer to get to $\alpha$ regardless of any preceding LIGR's i.e. no new LIGR's can result from this, another unanticipated short cut to Algorithm~\ref{alg5.1}.
\begin{comment}
\leftarrow 1Tcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}\un{c}ccb\alpha
\stackrel{b}{\leftarrow}1Tcdc\un{c}c^3b\alpha\leftarrow 2Tcdc^2\un{c}c^2b\alpha\leftarrow 2Tcdc\un{b}c^3b\alpha\leftarrow 2Tcd\un{b}bc^3b\alpha\stackrel{b}{\leftarrow}1Tc\un{a}b^2c^3b\alpha$ from which no further backward steps are possible.
continues with $7$, $8$, $21$ or $23.0-15$ preceding $2$. Then the sequence $7\cdot 2\cdot(8\cdot 2)^{{\it k}}$ has the effect $1\un{T}\leftarrow 3T\un{a}\leftarrow 1Tab^{2{\it k}}\un{b}$.
The backward search for $F$ must have the form $1Tab^{2{\it k}}\un{b}\alpha\leftarrow STa\ldots cb\alpha$ provided ${\it k}>{\rm 0}$. Again by Lemma~\eqref{lemma} no new LIGR's and no new residual CS's can be obtained.
This gives $7\cdot 2\cdot (8\cdot 2)^k\stackrel{\Delta F}{\Rightarrow}\emptyset\dashv$ i.e. $7$ added on the left gives no new LIGR's and adds no new resuts of $F$.
Therefore the grand search continues with $8$ preceding $2$ giving the sequence $8\cdot 2\cdot (8\cdot 2)^k$ which has the effect $1\un{T}\leftarrow 3T\un{b}\leftarrow 1Tb^{2k+1}\un{b}$. Applying $F$ gives $1Tb^{2k+1}\un{b}\alpha\leftarrow Tb\ldots cb\alpha\leftarrow\ldots cb\alpha$. By Lemma~\eqref{lemma} $cb\alpha$ is maintained as above
so no new LIGR's can result, but residual CS's could be obtained and must end with $cb\alpha$.
Thus the grand search must continue with $2\cdot 8\cdot 2\cdot(8\cdot 2)^k = 2\cdot(8\cdot 2)^{k+1}$ with the effect $3\un{T}\leftarrow 1T\un{b}\leftarrow 1Tb^{2k+2}\un{b}$.
Applying $F$ again gives $1\un{T}b^{2(k+1)}\un{b}\alpha\leftarrow b\ldots cb\alpha$, and again $cb\alpha$ is maintained so no new LIGR's can be obtained. This establishes the inductive hypothesis by induction and hence all the intermediate steps, using the base case ${\it k}={\rm 0}$.
These results prove that any sequence of the form $(8\cdot 2)^k$ with ${\it k}>{\rm 0}$ under $F$ gives the LIGR's $\{6,7,8\}$ and possibly other residual CS's. Also any sequence of the form $7\cdot(8\cdot 2)^k$ with ${\it k}>{\rm 0}$ under $F$ gives also $\{6,7,8\}$ but this time having no residual CS's.
\end{comment}
\subsubsection{Sequences ending with LIGR $3$}
Consider sequences of LIGR's ending with $3$ which is $1\un{T}\stackrel{b}{\leftarrow}1\un{c}T$. Applying $F$ starts from $1\alpha\un{c}T\stackrel{b}{\leftarrow}1\un{c}cT$ showing that $3\stackrel{F}{\Rightarrow}\{3\}.$ $3$ can be preceded by $1$, $3$, $14$, $15$ and $18$. The sequence $1\cdot3$ is $2\un{T}\leftarrow1\un{a}T\leftarrow 1\un{c}aT.$
Applying $F$ starts from $1\alpha\un{c}aT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{c}caT\\[5pt]
\leftarrow3\alpha c\un{d}T\end{array}\right.$ showing that two new residual CS's are the only extra results of preceding $3$ with $1$. The sequence $4\cdot 1\cdot 3$ is $3\un{T}\leftarrow 2\un{a}T\leftarrow 1\un{c}aaT$. $F$ can be applied to the residual CS with the substitution $T\to aT$ and gives
\begin{equation}1\alpha\un{c}aaT\leftarrow3\alpha c\un{d}aT\leftarrow\ldots\left\{\begin{array}{l}\leftarrow3\alpha cb\un{d}T\\\stackrel{b}{\leftarrow}2\un{a}cdaT\\
\stackrel{c}{\leftarrow}3\un{c}cdaT\end{array}\right..\end{equation} where the pointer does not reach the $a$ adjacent to $T$ during this computation therefore this shortens to
\begin{equation}1\un{c}aT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}2\un{a}cdT\\\stackrel{c}{\leftarrow} 3\un{c}cdT\end{array}\right.\end{equation} which are new LIGR's and will be numbered $10-13$ respectively (e.g. LIGR $11$ is $1\un{c}aT\stackrel{b}{\leftarrow}2\un{a}cbT$), and the residual CS's which require further backward searching.
The sequence $9\cdot 4\cdot 1\cdot 3$ is $3\un{T}\leftarrow 3\un{c}T\leftarrow1\un{c}aacT$. Applying $F$ gives
\begin{equation}\label{9to4to1}1\alpha\un{c}aacT\leftarrow3\alpha cb\un{d}cT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}badcT\\\stackrel{c}{\leftarrow}2\un{b}badcT\end{array}\right.\end{equation} after a few steps. These when abbreviated are
\begin{equation}1\un{c}aaT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}badT\\\stackrel{c}{\leftarrow}2\un{b}badT\end{array}\right.\end{equation}
which will be numbered LIGR's $14-17$ respectively. Also there are now no residual CS's, so this branch of the grand search ends.
The sequence $12\cdot 4\cdot 1\cdot 3$ has the effect $1\un{c}aT\leftarrow 1\un{c}aaccaT$ and $F$ gives, using \eqref{9to4to1},
\begin{equation}1\alpha\un{c}aaccaT\leftarrow 3\alpha cb\un{d}ccaT\left\{\begin{array}{l}\stackrel{b}{\leftarrow} 1\un{a}badccaT\\\stackrel{c}{\leftarrow}2\un{b}badccaT\end{array}\right.\end{equation} which shorten to $14-17$ and no new residual CS's.
The sequence $13\cdot 4\cdot 1\cdot 3$ clearly gives the same result because it is the same as above except that the rightmost $a$ has been replaced by $b$ throughout which makes no difference.
Next consider $5\cdot 1\cdot 3$ with the effect $2\un{T}\leftarrow1\un{c}abT$. Then applying $F$ gives
\begin{equation}\label{5to1to3}1\alpha\un{c}abT\leftarrow3\alpha c\un{d}bT\leftarrow \left\{\begin{array}{l}3\alpha cdbT\left\{\begin{array}{l}\stackrel{b}{\leftarrow} 2\un{a}c
dbT\\\stackrel{c}{\leftarrow}3\un{c}cdbT\end{array}\right.\\1\alpha cd\un{b}T\end{array}\right.\end{equation} apart from CS's for which there is no preceding CS. This gives two double LIGR's which reduce to $10-13$ and a residual CS.
$4\cdot 5\cdot 1\cdot 3$ is $3\un{T}\leftarrow 1\un{c}abaT$ and $F$ gives
\begin{equation}1\alpha\un{c}abaT\leftarrow1\alpha cd\un{b}aT\leftarrow3\alpha cdb\un{d}T
.\end{equation} Note here to avoid repetition, only the residual CS from \eqref{5to1to3} with the substitution $T\to bT$ from LIGR $5$ was followed.
The sequence $9\cdot 4\cdot 5\cdot 1\cdot 3$ is $3\un{T}\leftarrow 1\un{c}abacT$. $F$ gives
$1\alpha \un{c}abacT\leftarrow3\alpha cdb\un{d}cT\stackrel{5}{\leftarrow}2\alpha cadb\un{c}T$. By Lemma~\ref{lemma} because of the $a$ on the left of the pointer, no new LIGR's can result if this branch of the grand search is continued.
For $12/13\cdot 4\cdot 5\cdot 1\cdot 3$ $F$ can start from $3\alpha cdb\un{d}ccdT\stackrel{3}{\leftarrow} 3\alpha ca\un{d}dccdT$ and again by Lemma~\ref{lemma} no LIGR's can result from this branch.
Consider $5\cdot 5\cdot 1\cdot 3$ $F$ can start from $1\alpha\un{c}abbT\leftarrow 1\alpha cd\un{b}bT\leftarrow 1\alpha c\un{c}bbT$ from which there are no RCS's or LIGR's. Applying $F$ to $10\cdot 5\cdot 1\cdot 3$ can start from $1\alpha\un{c}abacaT\leftarrow1\alpha cd\un{b}acaT\leftarrow 1\alpha c\un{a}adcaT$ and again by Lemma~\ref{lemma} no LIGR's can result from this branch.
$11\cdot 5\cdot 1\cdot 3$ is $1\un{c}aT\leftarrow 2\un{a}cbT\leftarrow 1\un{c}abacbT$ $F$ gives
$1\alpha\un{c}abacbT\leftarrow1\alpha cd\un{b}acbT\leftarrow 3\alpha ca\un{d}dcbT$ cannot continue.
$16\cdot 5\cdot 1\cdot 3$ is $1\un{c}aaT\leftarrow 2\un{b}baaT\leftarrow 1\un{c}abcaaT$
$F$ gives $1\alpha \un{c}abcaaT\leftarrow 1\alpha cd\un{b}caaT\leftarrow\left\{\begin{array}{l}2\un{a}ccdcaaT\\3\un{c}ccdcaaT\\2\alpha cca\un{c}aaT\end{array}\right.$ where the last result cannot give any LIGR's.
These shorten to the new LIGR's $24$ and $25$ respectively
$1\un{c}abcT\leftarrow\left\{\begin{array}{l}2\un{a}ccdcT\\3\un{c}ccdcT\end{array}\right.$.
$17\cdot 5\cdot 1\cdot 3$ is $1\un{c}aaT\leftarrow 2\un{b}babT\leftarrow 1\un{c}abbbabT$.
$F$ gives $1\alpha \un{c}abbbabT\leftarrow 1\alpha cd\un{b}bbabT\leftarrow 1\alpha c\un{c}b^3cT$ which cannot continue giving no RCS's and no LIGR's.
$19\cdot 5\cdot 1\cdot 3$ is $1\un{c}cT\leftarrow 2\un{b}bcT\leftarrow 1\un{c}ab^3cT$. $F$ gives
$1\alpha\un{c}ab^3cT\leftarrow 1\alpha cd\un{b}bbcT\leftarrow 1\alpha c\un{c}b^3cT$ no new results.
$10\cdot 1\cdot 3$ is $1\un{c}aT\leftarrow 2\un{a}caT\leftarrow 1\un{c}aacaT$ $F$ gives
$1\alpha\un{c}aacaT\leftarrow3\alpha c\un{d}acaT\leftarrow\left\{\begin{array}{l}2\un{a}cdacaT\\3\un{c}cdacaT\\1\un{a}badcaT\\2\un{b}badcaT\end{array}\right.$. These shorten to the LIGR's $10-17$ already found and no RCS's.
Similarly the results of $11\cdot 1\cdot 3$ give the same final results.
$16\cdot 1\cdot 3$ is $1\un{c}aaT\leftarrow 2\un{b}baaT\leftarrow 1\un{c}abbaaT$ $F$ gives
$1\alpha\un{c}abbaaT\leftarrow 3\alpha c\un{d}bbaaT\leftarrow\left\{\begin{array}{l}2\un{a}cdbbaaT\\3\un{c}cdbbaaT\end{array}\right.$ which shorten to LIGR's $10-14$ with no RCS's.
$17\cdot 1\cdot 3$ is $1\un{c}aaT\leftarrow 2\un{b}babT\leftarrow 1\un{c}abbabT$ $F$ gives
results that shorten to LIGR's $10-13$ with no RCS's.
$19\cdot 1\cdot 3$ is $1\un{c}cT\leftarrow 2\un{b}bcT\leftarrow 1\un{c}abbcT$. $F$ gives results that shorten to LIGR's $10-13$ again.
The sequence $3\cdot 3$ has the effect $1\un{T}\stackrel{b}{\leftarrow}1\un{c}T\leftarrow 1\un{c}cT$. $F$ gives $1\alpha\un{c}cT\leftarrow 2\alpha c\un{c}T$ a residual CS so continue.
$1\cdot 3\cdot 3$ has the effect $2\un{T}\stackrel{b}{\leftarrow}1\un{a}T\leftarrow 1\un{c}caT$
\begin{equation}1\alpha\un{c}caT\leftarrow 2\alpha c\un{c}aT\leftarrow 2\alpha \un{b}caT\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}bcaT\\\stackrel{c}{\leftarrow}2\un{b}bcaT\end{array}\right.\end{equation}
This shortens to\begin{equation}\label{eq114}1\un{c}cT\left\{\begin{array}{l}\leftarrow1\un{a}bcT\\\leftarrow 2\un{b}bcT\end{array}\right.\end{equation} without any residual CS's. Equation \eqref{eq114} will be called LIGR's $18$ and $19$ respectively.
Consider the sequence $3\cdot 3\cdot 3$ with effect $2\un{T}\stackrel{b}{\leftarrow}1\un{c}T\leftarrow 1\un{c}ccT$
\begin{equation}1\alpha\un{c}ccT\leftarrow2\alpha c\un{c}cT\leftarrow2\alpha\un{b}ccT\left\{\begin{array}{l}\stackrel{b}{\leftarrow} 1\un{a}bccT\\\stackrel{c}{\leftarrow} 2\un{b}bccT\end{array}\right.\end{equation} which shortens to $18$ and $19$ above, without any residual CS's.
Next consider $14/15\cdot 3$ which is $1\un{c}aaT\leftarrow 1\un{a}badT\leftarrow 1\un{c}abadT$. Applying $F$ gives
\begin{equation}1\alpha\un{c}abadT
\leftarrow \left\{\begin{array}{l}
\stackrel{b}{\leftarrow}2\un{a}cdbadT\\\stackrel{c}{\leftarrow}3\un{c}cdbadT\\
%3\alpha\un{c}\left\{\begin{array}{l}a\\b\end{array}\right\}baaT\left\{\begin{array}{l} \stackrel{b}{\leftarrow}2\un{a}c\left\{\begin{array}{l}a\\b\end{array}\right\}baaT\\\stackrel{c}{\leftarrow}3\un{c}c\left\{\begin{array}{l}a\\b\end{array}\right\}baaT\\\end{array}\right.
\leftarrow1\alpha cdbd\un{b}T\end{array}\right.
\end{equation}
The minimal forms of the first two results are the LIGR's $10-13$. The sequence $18\cdot 3$ is $1\un{c}cT\leftarrow 1\un{a}bcT\leftarrow 1\un{c}abcT$. $F$ gives
\begin{equation}\label{eq117}1\alpha\un{c}abcT\leftarrow\left\{\begin{array}{l}2\un{a}cdbcT\\
3\un{c}cdbcT\\
2\alpha cdb\un{c}T
\end{array}\right.\end{equation}
which when shortened give LIGR's $10-13$ and a residual CS. Only $3$ can precede $18$ and $3\cdot 18\cdot 3$ is $1\un{c}T\leftarrow 1\un{c}cT\leftarrow 1\un{c}abcT$. Note that here an extra symbol $c$ was needed in order that the RHS of $3$ matched the LHS of $18\cdot 3$. $F$ gives the same result as above. Of the LIGR's that can precede $3$ only $3$ is compatible because of the symbol $c$ on left and this gives $3\cdot 3\cdot 18\cdot 3$ which is $1\un{T}\leftarrow 1\un{c}T\leftarrow 1\un{c}abcT$ which again gives the same result of $F$.
$1\cdot 3\cdot 3\cdot 18\cdot 3$ is $2\un{T}\leftarrow 1\un{a}T\leftarrow 1\un{c}abcaT$. $F$ gives
no RCS's and LIGR's $24$ and $25$. $3\cdot 3\cdot3\cdot18\cdot3$ is $1\un{T}\leftarrow1\un{c}T\leftarrow1\un{c}abccT$. $F$ gives LIGR's $24$ and $25$ and no RCS's, and likewise for $14/15\cdot 3\cdot3\cdot 18\cdot 3$. It is now obvious that the same result will come from $18\cdot3\cdot3\cdot18\cdot3$ because it starts from a CS that shares in common with the previous case the string beyond which the computation to get these results does not go.
The sequences $14/15\cdot 3\cdot18\cdot3$ are $18\cdot3\cdot18\cdot3$ are not possible because of other compatibility restrictions based non-adjacent LIGR's.
\begin{comment}
$F$ gives \begin{equation}\label{eq118}1\alpha\un{c}cabcT\leftarrow2\alpha\un{b}cabcT\left\{\begin{array}{l}
\stackrel{b}{\leftarrow}1\un{a}bcabcT\\\stackrel{c}{\leftarrow}2\un{b}bcabcT\end{array}\right.\end{equation} showing that the results additional to $3$ are $18$ and $19$ i.e. $\ldots 3\cdot 18\cdot 3\stackrel{F}{\to}\{3,18,19\}$ without any residual CS's. Because only $3$ can precede $18$, all possible sequences ending with $18\cdot 3$ are included here despite the fact that \eqref{eq118} is not obtained by specialising $T$ in \eqref{eq117}.
\end{comment}
\subsubsection{Sequences ending with LIGR $4$}
LIGR $4$ is $3\un{T}\stackrel{b}{\leftarrow}2\un{a}T$. $F$ gives
\begin{equation}2\alpha\un{a}T\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}aT\\\stackrel{c}{\leftarrow}2\un{b}aT\end{array}\right.\end{equation} which shortens to $1$ and $5$, and this result could depend on the leftmost symbol of $T$ because right-moving reverse steps could occur.
Therefore LIGR's preceding $4$ must be considered.
$9\cdot 4$ is $3\un{T}\leftarrow 3\un{c}T\leftarrow 2\un{a}cT$, and applying $F$ gives no LIGR's or RCS's.
$12/13\cdot 4$ is $1\un{c}aT\leftarrow3\un{c}cdT\leftarrow 2\un{a}ccdT$ and $F$ gives no LIGR's or RCS's.
Therefore these results show that $\{9,12,13\}\cdot 4\stackrel{F}{\Rightarrow}\{1,5\}$ only.
*********************** edited to here ********************************
\subsubsection{Sequences ending with LIGR $5$}
LIGR $5$ is $2\un{T}\leftarrow 2\un{b}T$ $2\alpha\un{b}T\left\{\begin{array}{l}\stackrel{b}{\leftarrow}1\un{a}bT\\\stackrel{c}{\leftarrow}2\un{b}bT\end{array}\right.$
which shortens to $1$ and $5$ so $\ldots5\stackrel{F}{\to}\{1,5\}$.
$4\cdot 5$ is $3\un{T}\leftarrow 2\un{a}T\leftarrow 2\un{b}aT$ $2\alpha\un{b}aT$ gives nothing new and no residual CS's. This is likewise true for $5$,$10$,$11$,$16$ and $17$ preceding $5$ and all follow from the fact that $2\_a$ and $2\_b$ cannot be arrived at from a step of the TM, so $\ldots\{4,5,10,11,16,17\}\to 5\stackrel{F}{\to}\{1,5\}$.
\subsubsection{Sequences ending with LIGR $6$}
LIGR $6$ is $1\un{T}\leftarrow 2T\un{c}$. Applying $F$ gives
$2T\un{c}\alpha\leftarrow\emptyset$. A left-moving reverse step could occur depending on the rightmost symbol of $T$ so this needs to be specialised by considering all possible previous LIGR's i.e just $2$. The sequence
$2\cdot 6$ is $3\un{T}\leftarrow1T\un{b}\leftarrow 2Tb\un{c}$ and applying $F$ gives $2Tb\un{c}\alpha\leftarrow 1T\un{a}c\alpha$. Further calculations suggest the following inductive hypothesis that the LIGR sequence $2\cdot (8\cdot 2)^k\cdot 6$ has the effect $3\un{T}\leftarrow\ldots\leftarrow 2Tb^{2k+1}\un{c}$, and that all the results of the backward search for $F$ take the form
\begin{equation}\label{ind_1}2Tb^{2k+1}\un{c}\alpha\leftarrow S_1T\ldots c\alpha\end{equation} with the pointer not reaching the right hand end so that there are no derived LIGR's. All the backward searches then either halt or end with the pointer at the left hand end giving residual CS's. Then the grand rearch continues with a single LIGR preceding $2$ which must be $7$ or $8$. This subsection concludes with the proof of this by induction.
Consider the case when $7$ precedes $2$ giving the sequence $7\cdot 2\cdot (8\cdot 2)^k\cdot 6$. Then the effect of this sequence is $1\un{T}\leftarrow 3T\un{a}\leftarrow 2Tab^{2k+1}\un{c}$. The backward search for $F$ starts from $2Tab^{2k+1}\un{c}\alpha$. The leftmost symbol is $a$, so as the TM runs backwards, because there is no backward TM step of the form $Xa\_\leftarrow CS$, that symbol can never be changed and the pointer can never reach next to $T$ that would give a residual CS. Also from \eqref{ind_1} \begin{equation}\label{ind2}2Tab^{2k+1}\un{c}\alpha\leftarrow S_2Ta\ldots c\alpha\leftarrow\ldots\end{equation} and continuing the backward search from there the $c\alpha$ at the end is maintained because if the pointer reaches $\un{x}c\alpha$ where $x$ is any symbol, the TM can go backwards to the right only with $1\_c\leftarrow 2\un{c}$, giving $2\un{c}\alpha$ and the TM cannot go right on a reverse TM step from there. Going left from there on a reverse TM step maintains $c\alpha$ so no new LIGR's can result. These results together show that whatever LIGR's precede the $7$, it make no difference to the result of $F$, and there are no LIGR's as the result of $F$ i.e. $7\cdot 2\cdot (8\cdot 2)^k\cdot 6\stackrel{F}{\to}\emptyset$.
Now consider when $8$ precedes the $2$ giving the sequence $8\cdot 2\cdot (8\cdot 2)^k\cdot 6$. This has the effect
$1\un{T}\leftarrow3T\un{b}\leftarrow 2Tb^{2k+2}\un{c}$. Now the backward search starts from
$2Tb^{2k+2}\un{c}\alpha$ and again \eqref{ind_1} can be used to start the backward search giving
\begin{equation}\label{ind3}2Tb^{2k+2}\un{c}\alpha\leftarrow STb\ldots c\alpha\leftarrow\ldots\end{equation}Continuing from there the argument above again applies showing that no new LIGR's can result, but this time there no impossibility of new residual CS's, which from the examples do occur.
This shows that the residual CS's obtained have the $c\alpha$ at the right hand end.
Here because there are residual CS's, in the grand search all LIGR's capable of preceding the $8$ in the sequence must be considered i.e. just LIGR $2$.
So considering the sequence $2\cdot 8\cdot 2\cdot (8\cdot 2)^k\cdot 6$ which is
$2\cdot (8\cdot 2)^{k+1}\cdot 6$, it has the effect $3\un{T}\leftarrow 1T\un{b}\leftarrow 2Tb^{2k+3}\un{c}$. Now the backward search starts from $2Tb^{2k+3}\un{c}\alpha$ and again the above argument applies giving a result of the form
\begin{equation}2Tb^{2k+3}\un{c}\alpha\leftarrow S_3Tbb\ldots c\alpha\leftarrow S_4T\ldots c\alpha.\end{equation}
where there is no direct connection between states $S,S_1,S_2 \text{ and }S_3$. This establishes the inductive hypothesis for all non-negative integers $k$ using the base case $k=0$ and shows that all sequences of LIGR's ending with LIGR $6$ under $F$ do not lead to any other LIGR's i.e.
\begin{equation}\ldots 6\stackrel{F}\to\emptyset.\end{equation}
\subsubsection{Sequences ending with LIGR $7$}
LIGR $7$ is $1T\leftarrow 3T\un{a}$, and $3T\un{a}\alpha\stackrel{b}{\leftarrow}1Ta\un{b}$ which shortens to $3\un{T}\leftarrow 1T\un{b}$ i.e. $2$, so $\ldots 7\stackrel{F}{\leftarrow}\{2\}$. Because of this, from all subsequent specialisation of this resulting from LIGR's preceding $7$, all lead under $F$ to LIGR $2$, so this will be ignored by restricting the first reverse TM step to moving to the left. Only $2$ and $20$ can precede $7$ and $2\cdot 7$ is $3\un{T}\leftarrow 1T\un{b}\leftarrow 3Tb\un{a}$ and the backward search is just $3Tb\un{a}\alpha\leftarrow 2T\un{a}a\alpha$ giving a residual CS so the grand search continues back.
LIGR $2$ can be preceded by $7$ and $8$,$21$ and $23$. The sequence $7\cdot 2\cdot 7$ is $1\un{T}\leftarrow3T\un{a}\leftarrow 3Tab\un{a}$ and $3Tab\un{a}\alpha\leftarrow 2Ta\un{a}a\alpha$ which cannot be continued further back, because there are no residual CS's and no new LIGR's so this branch of the grand search ends giving $\ldots 7\cdot 2\cdot 7\stackrel{F}{\to}\{2\}$.
$8\cdot 2\cdot 7$ which has the effect $1\un{T}\leftarrow 3Tbb\un{a}$. The backward search is $3Tbb\un{a}\alpha\leftarrow 2Tb\un{a}a\alpha\leftarrow1T\un{a}aa\alpha$ i.e. there are no new LIGR's and one residual CS. Continuing back gives
$2\cdot 8\cdot 2\cdot 7$ with the effect $3\un{T}\leftarrow 3Tbbb\un{a}$ with the backward search giving only the following result ignoring branches that terminate with the pointer not at one end
\begin{equation}\label{2827}3Tbbb\un{a}\alpha\leftarrow 1T\un{c}aaa\alpha.\end{equation} This again gives one residual CS and no new LIGR's.
Continuing, the sequence
$7\cdot 2\cdot 8\cdot 2\cdot 7$ has the effect $1T\leftarrow 3Tabbb\un{a}$ with backward search that gives no
residual CS and no new LIGR after 3 steps and using \eqref{2827}.
By now a clear pattern has emerged with LIGR's $2$ and $8$ alternating, and with LIGR $7$ terminating the sequences, however it is not yet clear how an induction proof can be completed showing this generally. Attempts to do so initially failed with the wrong inductive hypothesis because insufficient symbols were used. These attempts forced a consideration of further iterations of the basic procedure as follows.
The sequence $8\cdot 2\cdot 8\cdot 2\cdot 7$ has the effect $1\un{T}\leftarrow 3Tbbbb\un{a}$ with backward search results using \eqref{2827} for the first step giving
\begin{equation}\label{82827}3Tb^4\un{a}\alpha\leftarrow1Tb\un{c}aaa\alpha\leftarrow \left\{\begin{array}{l}1T\un{c}caaa\alpha\\2T\un{a}cdaa\alpha\\1T\un{a}ba
d
a\alpha\end{array}\right..\end{equation}
Here there are three residual CS's and no new LIGR's. Continuing gives the sequence
$2\cdot 8\cdot 2\cdot 8\cdot 2\cdot 7$ with the effect $3\un{T}\leftarrow 3Tb^5\un{a}$ and the backward search started using \eqref{82827} gives
\begin{equation}\label{8282827}3Tb^5\un{a}\alpha\leftarrow\left\{\begin{array}{l}1Tb\un{c}caaa\alpha\leftarrow\left\{\begin{array}{l}1T\un{c}ccaaa\alpha\\1T\un{a}bcaaa\alpha\end{array}\right.\\
2Tb\un{a}cdaa\alpha\leftarrow1T\un{a}acdaa\alpha\\
1Tb\un{a}bad a\alpha\leftarrow
1T\un{c}abada\alpha
\end{array}\right..\end{equation}
Continuing for the last time gives the sequence $8\cdot 2\cdot 8\cdot 2\cdot 8\cdot 2\cdot 7$ with effect $1T\leftarrow 3Tb^6\un{a}$. The results of the backward search are
\begin{equation}3Tb^6\un{a}\alpha\leftarrow\left\{\begin{array}{l}
1Tb\un{c}ccaaa\alpha\leftarrow\left\{\begin{array}{l}1T\un{c}cccaaa\alpha\\1T\un{a}bc^2a^3\alpha\end{array}\right.\\
1Tb\un{a}bcaaa\alpha\leftarrow1T\un{c}abcaaa\alpha\\
1Tb\un{a}acdaa\alpha\leftarrow1T\un{c}aacd
aa\alpha\\
1Tb\un{c}abada\alpha\leftarrow
\left\{\begin{array}{l}
1T\un{c}cabada\alpha\\[10pt]
1Tbc\left\{\begin{array}{c}db\\aa\end{array}\right\}dbd\un{b}\\[20pt]
2T\un{a}cdbada\alpha\\[10pt]
3Tbca^3db\left\{\begin{array}{l}\un{a}\\\un{b}\end{array}\right\}\\[10pt]
2Tbca^3db\un{c}\\
Tbcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}db\left\{\begin{array}{l}3\un{a}\\3\un{b}\\2\un{c}\end{array}\right\}\\
1T\un{a}bbcaad\alpha\\[10pt]
1T\un{a}bacdad\alpha\\[10pt]
1T\un{a}bbccba\alpha\\
\end{array}\right.\end{array}\right.\end{equation}
In this surprising result note that all the new LIGR's result from a single residual CS in \eqref{8282827}.
The results have been expressed as succinctly as possible using arrays giving alternatives that can be nested. In every case the alternatives in the arrays can all be chosen independently of each other.
\newpage
Suppose the inductive hypothesis is if $k\ge 3$ then
$(8\cdot 2)^k\cdot 7$ is the substitution $1\un{T}\leftarrow3Tb^{2k}\un{a}$ and each derived residual CS as the result of applying $F$ contains the pair of symbols $ca$ or $cb$.
%\left\{\begin{array}{l}a\\b\end{array}\right\}
It follows from this that $2\cdot (8\cdot 2)^k\cdot 7$ is the substitution $3\un{T}\leftarrow 1T\un{b}\leftarrow 3Tb^{2k+1}\un{a}$.
While applying $F$ to this the backward search starts with the symbol $b$ on the left playing no part initially. Then the pointer could reach the right giving an LIGR that would be the same one as found before from $(8\cdot 2)^k\cdot 7$ because the $b$ at the left plays no part. Alternatively if the pointer reaches a CS of the form $STb\un{x}\ldots cd\ldots$
%[Now it is clear that case (1) does not have to be considered any more in the grand search because regardless of the sequence of preceding LIGR's when $F$ is applied, the same set of LIGR's will be again reproduced and these do not indicate any further results in the grand search.]
%With case (2) above the backward search starts from $Tb^{2k+1}\un{a}\alpha\leftarrow STb\ldots c\left\{\begin{array}{l}a\\b\end{array}\right\}\ldots\alpha$
then it either stops or gets to a residual CS with the pointer at the left having the symbols $ca$ or $cb$, or reaches a CS of the form $S_1T\ldots\_cd\ldots\alpha\stackrel{S_1=1}{\leftarrow}2T\ldots \un{c}d\ldots\alpha$ from which a reverse TM step to the right is impossible. Therefore $cd$ is left intact and the pointer cannot cross these symbols and the backward search could lead to a residual CS. Therefore any new residual CS's derived in this way must contain $ca$ or $cb$ and the set of LIGR's is the same as for $(8\cdot 2)^k\cdot 7$.
LIGR's $7$ and $8$,$21$ and $23$ can precede LIGR $2$ so consider first
$7\cdot 2\cdot (8\cdot 2)^k\cdot 7$ which is $1\un{T}\leftarrow 3T\un{a}\leftarrow 3Tab^{2k+1}\un{a}$.
Applying $F$ gives, using the above result, and a very similar argument to the one above with the difference that the added symbol $a$ prevents any residual CS's occurring by Lemma~\eqref{lemma}. The LIGR's produced are again the same set.
Next consider $(8\cdot 2)^{k+1}\cdot 7$ which has the effect $1\un{T}\leftarrow 3T\un{b}\leftarrow 3Tb^{2k+2}\un{a}$.
Applying $F$ gives again by the same argument the same set of LIGR's and each residual CS contains either $ca$ or $cb$. This establishes the inductive hypothesis for $k$ replaced by $k+1$ and hence all the other statements and establishes by induction the inductive hypothesis for all $k\ge3$, and for $k>3$ no new LIGR's are possible.
Next consider $21\cdot 2\cdot (8\cdot 2)^k\cdot 7$ which is the substitution
$3Tb^5\un{a}\leftarrow 3Tca^3db\un{d}\leftarrow 3Tca^3dbdb^{2k+1}\un{a}$.
For $k=0$ the backward search is
\begin{equation}\begin{array}{l}3Tca^3dbdb\un{a}\alpha\leftarrow2Tca^3dbd\un{a}a\alpha\leftarrow1Tca^3db\un{a}aa\alpha\leftarrow\left\{\begin{array}{l}1Tca^3d\un{c}a^3\alpha*1\\3Tca^3dba\un{d}a\alpha\end{array}\right.\\
*1\leftarrow\left\{\begin{array}{l}1Tca^3\un{c}ca^3\alpha\\3Tca^3dc\un{d}aa\alpha
\leftarrow3Tca^3d\un{c}daa\alpha\leftarrow\left\{\begin{array}{l}2Tca^3\un{a}cdaa\alpha\\
1Tca^3dc\un{b}aa\alpha\leftarrow3Tca^3dcb\un{d}a\alpha*2\end{array}\right.
\end{array}\right.\\[20pt]
*2\leftarrow 2Tca^3dc\un{a}da\alpha\leftarrow2Tca^3d\un{b}ada\alpha\leftarrow1Tca^3\un{a}bada\alpha\end{array}\end{equation}
giving no new LIGR's and no residual CS's.
For $k=1$ the backward search is as follows
\begin{equation}\begin{array}{l}3Tca^3dbdb^3\un{a}\alpha\leftarrow2Tca^3dbdb^2\un{a}a\alpha\leftarrow1Tca^3dbdb\un{a}aa\alpha*1\\[10pt]
*1\leftarrow\left\{\begin{array}{l}1Tca^3dbd\un{c}a^3\alpha\leftarrow\left\{\begin{array}{l}3Tca^3dbdc\un{d}a^2\alpha\leftarrow3Tca^3dbd\un{c}da^2\alpha*2\\1Tca^3db\un{c}ca^3\alpha\end{array}\right.\\3Tca^3dbdba\un{d}a\alpha
\end{array}\right.\\[20pt]
*2\leftarrow\left\{\begin{array}{l}2Tca^3db\un{a}cda^2\alpha\\1Tca^3dbdc\un{b}a^2\alpha
\leftarrow 3Tca^3dbdcb\un{d}a\alpha\leftarrow 2Tca^3dbdc\un{a}da\alpha*3\end{array}\right.\\[10pt]
*3\leftarrow2Tca^3dbd\un{b}ada\alpha\leftarrow1Tca^3db\un{a}bada\alpha\leftarrow1Tca^3d\un{c}abada\alpha\end{array}\end{equation}
with termination, except for the final CS, if the pointer reaches an end of the known symbols or no backward TM step is possible or if the pointer cannot reach either end by Lemma~\eqref{lemma}. The final CS has as a substring the string mentioned at the beginning of Lemma~\eqref{lemma3}, and because the symbol $a$ is left of the pointer in this final CS, continuing the backward search from there cannot lead to any residual CS's and does lead to exactly the list of CS's in Lemma~\eqref{lemma3}. When these results are reduced to their minimal form it gives the set of LIGR's in \eqref{newligrs1}.20-23 because the second $d$ in the last line of the above has to be $b$ not $a$ otherwise the derivation stops.
$20\cdot 8\cdot 2\cdot 7$ is $3Tb^5\un{a}\leftarrow 3Tc\left\{\begin{array}{l}ab\\bb\\aa\end{array}\right\}dbdbbb\un{a}$.
Adding alpha and doing the backward search gives just 5 residual CS's
\begin{equation}\begin{array}{l}
2T\un{b}bc^5a^3\alpha\\3T\un{c}ccdc^3a^a\alpha\\3T\un{c}cdbc^3a^3\alpha\\2T\un{b}bccabca^3\alpha\\2T\un{b}bccabca^3\alpha\end{array}\end{equation}
Consider $20\cdot (8\cdot 2)^k\cdot 7$. This has the effect \begin{equation}3Tb^5\un{a}\leftarrow 3Tc\left\{\begin{array}{l}ab\\bb\\aa\end{array}\right\}dbd\leftarrow 3Tc\left\{\begin{array}{l}ab\\bb\\aa\end{array}\right\}dbdb^{2k+1}\un{a}.\end{equation}
Then proceeding with the backward search from $3Tc\left\{\begin{array}{l}ab\\bb\\aa\end{array}\right\}dbdb^{2k+1}\un{a}\alpha$
and ignoring the single move to the right giving LIGR $2$, and bearing in mind that the reversed TM cannot cross $ca$ or $cb$ going to the right, or $a$ going to the left gives a tree of CS's showing that the only LIGR's that
result from this are precisely the set \eqref{newligrs1} for all $k>0$. The cases $k = 1,2$ need to be checked separately. It is interesting that this set is independent of $k$ but this is obvious for all sufficiently large $k$ from the fact that the reversed TM does not go further left than 6 places left of $\alpha$ and then return. Also the CS's in which the pointer is at its leftmost position the these derivations for the cases $k=1,2$ and $k\ge3$ are of the same form $1\ldots \un{c}abada\alpha$. This also shows that the set of LIGR's for these cases must be the same. The proof of this is straighforward but quite long and follows the usual reverse search procedure and is shortened somewhat by the non-crossing rules above. In one case 29 reverse steps were needed to get the final result.
Because new LIGR's have been found, additional sequences are possible. The new LIGR's listed in \eqref{newligrs1} below will be numbered as follows if needed. Within each group (labelled 20-23) the index number is represented in a base that depends on the place and is given by the lengths of the arrays in that group. So as the numbering is increasing down each array separately starting at 0, the arrays closest to the string $T$ are changing fastest as the index number within the group increases, so for example LIGR $20.8$ has RHS $1Tcaaabb\un{b}$ because ${\rm8 = 2*1 + 0*3 + 1*6}$ and the choices in the arrays are numbered 2,0,1 to get that RHS. Note that this puts the representation of the integer 8 in the reverse of the usual order which is for convenience when constructing table~\eqref{cbpb} because $T$ is here on the left. This uses a simple extention of the usual representation of integers in different bases.
$20\cdot 7$ is $3Tb^5\un{a}\leftarrow 3Tc\left\{\begin{array}{l}ab\\bb\\aa\end{array}\right\}
dbdb\un{a}$ and the backward search from there gives just the following residual CS's and no new LIGR's
\begin{equation}\begin{array}{l}3T\un{c}c\left\{\begin{array}{c}dacd\\dbca\\cdca\end{array}\right\}a^2\alpha\\[50pt]
2T\un{b}b\left\{\begin{array}{c}c^3a^2\\adcda\\cabad\end{array}\right\}a\alpha\end{array}.\end{equation}
LIGR's $20$ can be preceded only by $7$, so continuing the grand search gives
The sequence $21\cdot 2\cdot 7$ has the effect
$3Tb^5\un{a}\leftarrow 3Tca^3dbdb\un{a}$
and adding $\alpha$ on the right and doing the backward search gives no new LIGR's or residual CS's.
While doing this it became clear that the pointer of the reverse TM cannot cross $a$ going left, and $ca$ or $cb$ going right and this shortened some of the computations. The same result was obtained from $23\cdot 2\cdot 7$ whose proof was simplified by exploiting the similarity between this and the previous result.
\subsubsection{Sequences ending with LIGR $8$}
LIGR $8$ is $1T\leftarrow 3T\un{b}$ and $3T\un{b}\alpha\stackrel{b}{\leftarrow}1Tb\un{b}$ which shortens to LIGR $2$ i.e. $\ldots8\stackrel{F}{\cdot} 2$. LIGR $8$ can only be preceded by LIGR $2$ giving $2\cdot 8$ which has the effect $3T\leftarrow 3Tb\un{b}$ and $3Tb\un{b}\alpha\leftarrow 2T\un{a}b\alpha$ a residual CS, in addition to $2$ as above, so the preceding LIGR needs to be considered i.e. $7$ or $8$.
The sequence $7\cdot2\cdot 8$ has the effect $1T\leftarrow 3T\un{a}\leftarrow 3Tab\un{b}$ and $3Tab\un{b}\alpha\leftarrow2Ta\un{a}b\alpha$ from which no reverse TM step can be made so $\ldots 7\cdot 2\cdot 8\stackrel{F}{\to} 2$ and no further extensions to the sequence are necessary.
The sequence $8\cdot 2\cdot 8$ has the effect $1\un{T}\leftarrow 3Tbb\un{b}$ and the backward search gives $3Tbb\un{b}\alpha\leftarrow 1T\un{a}ab\alpha$ a residual CS only, so the next sequence to be considered is $2\cdot 8\cdot 2\cdot 8$ which has the effect $3\un{T}\leftarrow 3Tbbb\un{b}$. The backward search gives
\begin{equation}3Tbbb\un{b}\alpha\leftarrow\left\{\begin{array}{l}1T\un{c}aab\alpha\\3Tbadb\left\{\begin{array}{l}\un{a}\\\un{b}\end{array}\right\}\\2Tba
db\un{c}
\end{array}\right.\end{equation} giving 1 residual CS and 6 new LIGR's.
\subsubsection{Sequences ending with LIGR's $9-19$}
LIGR $9$ is $3\un{T}\leftarrow 3\un{c}T$ and $3\alpha\un{c}T\left\{\begin{array}{l}\stackrel{b}{\leftarrow}2\un{a}cT\\\stackrel{c}{\leftarrow}3\un{c}cT\end{array}\right.$ shortens to $4$ and $9$ so $\ldots9\stackrel{F}{\to}\{4,9\}$ but because the left end symbol of $T$ is not specified, specialising it by including previous LIGR's could generate more results. $9\cdot 9$ is $3\un{T}\leftarrow3\un{c}T\leftarrow3\un{c}cT$ and $3\alpha\un{c}cT$ gives nothing new so $\ldots9\to 9\stackrel{F}{\to}\{4,9\}$.
Similarly it follows that $12\cdot 9$ and $13\cdot 9$ under $F$ produce no new results, so $\ldots\{9,12,13\}\to 9\stackrel{F}{\to}\{4,9\}$.
In a similar manner also the following can be easily established
$\ldots\{10,11\}\stackrel{F}{\to}\{1,5\}$\\
$\ldots\{12,13\}\stackrel{F}{\to} \{4,9\}$\\
$\ldots\{14,15\}\stackrel{F}{\to} \{3\}$\\
$\ldots\{16,17\}\stackrel{F}{\to}\{1,5\}$\\
$\ldots\{18\}\stackrel{F}{\to}\{3\}$\\
$\ldots\{19\}\stackrel{F}{\to}\{1,5\}$\\
\subsubsection{The updated set of LIGR's}
Because new LIGR's have been found, the ``can possibly be preceded by" relation needs to be updated as follows
The augmented set of LIGR's is now given by
\begin{equation}\label{newligrs1}
\begin{array}{ll}
1&2\un{T}\stackrel{b}{\leftarrow}1\un{a}T\\
2&3\un{T}\stackrel{b}{\leftarrow}1T\un{b}\\
3&1\un{T}\stackrel{b}{\leftarrow}1\un{c}T\\
4&3\un{T}\stackrel{b}{\leftarrow}2\un{a}T\\
5&2\un{T}\stackrel{c}{\leftarrow}2\un{b}T\\
6&1\un{T}\stackrel{c}{\leftarrow}2T\un{c}\\
7&1\un{T}\stackrel{a}{\leftarrow}3T\un{a}\\
8&1\un{T}\stackrel{a}{\leftarrow}3T\un{b}\\
9&3\un{T}\stackrel{c}{\leftarrow}3\un{c}T\\
10&1\un{c}aT\stackrel{b}{\leftarrow}2\un{a}caT\\
11&1\un{c}aT\stackrel{b}{\leftarrow}2\un{a}cbT\\
12&1\un{c}aT\stackrel{c}{\leftarrow}3\un{c}caT\\
13&1\un{c}aT\stackrel{c}{\leftarrow}3\un{c}cbT\\
14&1\un{c}aaT\stackrel{b}{\leftarrow}1\un{a}baaT\\
15&1\un{c}aaT\stackrel{b}{\leftarrow}1\un{a}babT\\
16&1\un{c}aaT\stackrel{c}{\leftarrow}2\un{b}baaT\\
17&1\un{c}aaT\stackrel{c}{\leftarrow}2\un{b}babT\\
18&1\un{c}cT\stackrel{b}{\leftarrow}1\un{a}bcT\\
19&1\un{c}cT\stackrel{b}{\leftarrow}2\un{b}bcT\\
20.(0-11)&3Tb^5\un{a}\leftarrow 1Tc\left\{\begin{array}{c}d
b\\aa\end{array}\right\}d
bd
\un{b}\\[20pt]
21.(0-3)&3Tb^5\un{a}\leftarrow 3Tca^3db\left\{\begin{array}{l}\un{a}\\\un{b}\end{array}\right\}\\[20pt]
22.(0-1)&3Tb^5\un{a}\leftarrow 2Tca^3db\un{c}\\[20pt]
23.(0-23)&3Tb^5\un{a}\leftarrow Tcd\left\{\begin{array}{l}ba\\cb\end{array}\right\}db\left\{\begin{array}{l}3\un{a}\\3\un{b}\\2\un{c}\end{array}\right\}\\
\end{array}
\end{equation}
Because new LIGR's have been found, the ``can possibly be preceded by" relation needs to be updated as follows
\begin{equation}\label{cbpb}\begin{array}{ll}
1\text{\hspace{1cm}}&4,5,10,11,16,17,19\\
2\text{\hspace{1cm}}&7,8,21,23.(0-15)\\
3\text{\hspace{1cm}}&1,3,14,15,18\\
4\text{\hspace{1cm}}&9,12,13\\
5\text{\hspace{1cm}}&4,5,10,11,16,17,19\\
6\text{\hspace{1cm}}&2,20\\
7\text{\hspace{1cm}}&2,20\\
8\text{\hspace{1cm}}&2,20\\
9\text{\hspace{1cm}}&9,12,13\\
10-19\text{\hspace{1cm}}&3\\
20,21,22,23\text{\hspace{1cm}}&7
\end{array}\end{equation}
The word ``possibly" is included because there may be other symbols in either of the strings $T$ that prevent a match of the sequences.
\begin{comment}
The reader will probably suspect by now that this process will never end.
To prove this by induction, assume that when $F$ is applied to the result of the sequence $(8\to 2)^k$, some residual CS's defining the set $S$ are obtained but no new LIGR's. The search must then continue from these residual CS's. Also assume that the set of LIGR's is just the set $1-9$ mentioned above. Then LIGR $8$ can only be preceded by LIGR $2$ which is $3\un{T}\stackrel{b}{\leftarrow}1T\un{b}$. Also assume that $(8\to 2)^k$ is $1\un{T}\leftarrow 1Tb^{2k-1}\un{b}$ so $F$ gives $1Tb^{2k-1}\un{b}\alpha\leftarrow S$. Assume that the first derivation step in $F$ can be obtained from the derivation of the residual CS's in $F$ applied to $2\to(8\to 2)^{k-1}$ has the form $1\un{T}b^{2k-1}\un{b}\alpha\leftarrow\leftarrow$ Also let $R$ be the set of reverse rules used to get $S$ in the shortest form possible.
Then $2\to(8\to 2)^k$ is $3\un{T}\leftarrow 1T\un{b}\leftarrow Tb^{2k}\un{b}.$ Applying $F$ to this starts with the backward search from $Tb^{2k}\un{b}\alpha\leftarrow bS\leftarrow S'$ say and assume that this just results in the residual CS's $S'$. This requires the computation to continue with an extra preceding LIGR, which are $7$ and $8$. Ignore the results with $7$ for now. $(8\to 2)^{k+1}$ is therefore $1\un{T}\stackrel{a}{\leftarrow}3T\un{b}\leftarrow Tb^{2k+1}\un{b}$ and $F$ gives $Tb^{2k+1}\un{b}\alpha\leftarrow bbS\leftarrow bS'\leftarrow S''$ say. let $R$ be the set of reverse rules used to get $S$.
\end{comment}
\begin{thebibliography}{99}
\bibitem{jhn2013}\href{https://www.longdom.org/articles/methods-for-understanding-turing-machine-computations.pdf}{Methods for Understanding Turing Machine Computations}
\bibitem{jhn2017}
\href{https://www.longdom.org/articles/reverse-engineering-turing-machines-and-insights-into-the-collatz-conjecture.pdf}{John Nixon Reverse engineering Turing Machines and the Collatz Conjecture}
\bibitem{tie}
\href{http://www.bluesky-home.co.uk/tie_v2_1.txt}{The previous version in D of the computer program for analysis of Turing Machines}
\bibitem{Tarjan's_paper}\href{https://doi.org/10.1137/0201010}{SIAM Journal on Computing, 1 (2): 146-160, Depth-First Search and Linear Graph Algorithms doi:10.1137/0201010}
\bibitem{Tarjan's_algorithm}
\href{http://bluesky-home.co.uk/Tarjan_v1_0.txt}{An implementation of Tarjan's strongly connected components algorithm in D}
\bibitem{tie_v3_0}\href{http://www.bluesky-home.co.uk/tie_v3_0.txt}{The new program tie v3.0 for doing the computations in this paper}
\end{thebibliography}
\end{document}