\documentstyle[12pt]{article} \setlength{\oddsidemargin}{10pt} \setlength{\evensidemargin}{10pt} \setlength{\marginparwidth}{0pt} \setlength{\marginparsep}{0pt} \setlength{\topmargin}{-40pt} \setlength{\textwidth}{450pt} \setlength{\textheight}{630pt} \setlength{\tabbingsep}{0pt} \setlength{\headsep}{30pt} \setlength{\fboxsep}{40pt} \setlength{\fboxrule}{4pt} \setlength{\footnotesep}{20pt} \raggedright \setlength{\parindent}{25pt} \setlength{\parskip}{8pt plus 5pt} \begin{document} \title{Well behaved derivations in one-rule semi-Thue systems} \author{Robert McNaughton\thanks{Supported by Grant No. CCR-9500182 from the National Science Foundation.} \\ Department of Computer Science \\ Rensselaer Polytechnic Institute \\ Troy, NY 12180-3590, U.S.A.} \date{November, 1995} \maketitle {\bf 1. Introduction.} This paper is a contribution to the investigation of the problem, does a given one-rule semi-Thue system have an infinite derivation? It is an open question as to whether an algorithm exists for this problem, whose complement is sometimes called the uniform termination problem for one-rule semi-Thue systems. It is well known that the corresponding problem for semi-Thue systems with finite sets of rules is undecidable. The importance of the general problem of termination in various types of computing systems is acknowledged by all. The more specific area of uniform termination of various rewriting systems is also important, as seen in the abundant literature, with many interesting results obtained from several points of view. In this category there are three references that are most relevant to this paper: \cite{gkm}~points out the importance of the uniform termination problem for certain practical computing problems in the area of theorem proving; \cite{d87}~and \cite{d93} give good accounts of various termination problems; \cite{d93}~has a particularly useful description of the peculiarities of termination problems for one-rule semi-Thue systems among termination problems in general. The first stimulus for my own research in this area was the conference presentation of~\cite{d93}. Two suitable general references on semi-Thue systems are \cite{ja} and~\cite{bo}. There are only a few papers directed specifically at the unform termination problem for one-rule semi-Thue systems. The first such seems to be Winfried Kurth's Ph.D. dissertation \cite{ku1} (see also~\cite{ku2}), which contains an interesting broad introduction to the problem, as well as some far-reaching preliminary results. One of these is a complete characterization of all one-rule semi-Thue systems that have an infinite derivation based on a loop of length 2. In a later paper~\cite{ku3} Kurth gives a complete characterization of all such systems with infinite derivations based on loops of length 3. Zantema and Geser \cite{zg} have focused on the class of systems given by single rules of the form $c^m b^n \rightarrow b^p c^q$, $m,n,p,q \geq 1$. They have proved that such a system has an infinite derivation if and only if either (1)~$p \geq 2n$ and $q \geq 2m$, or (2)~$p > n$, $q>m$ and either $p$ is a multiple of $n$ or $q$ is a multiple of $m$. Their result is significant because some of the systems in their class had been difficult to deal with. There does not seem to be a prevalent unsolved question about the uniform termination of any particular one-rule semi-Thue system. Loosely speaking, we seem to be able to decide whether any such system is uniformly terminating. Perhaps it is for this reason that most (or all) of those who have worked on the problem are willing to conjecture that the general algorithm exists. This paper makes a distinction between two kinds of derivations in semi-Thue systems: well behaved derivations and ill behaved derivations. A derivation is ill behaved if the occurrence of the right side of a rule introduced in some line is, in a certain sense, completely destroyed in later lines. This concept must remain vague for now; a precise definition will be given early in Section~2. The first result, the decidability of the problem of whether a given semi-Thue system with finitely many rules has an infinite well behaved derivation, will appear at at the end of Section~2. Further results are an algorithm in Section~6 to determine whether a given one-rule semi-Thue system has a finite ill behaved derivation, and a computationally efficient algorithm in Section~8 to determine whether a given one-rule system has an infinite well behaved derivation. Theorems~3.8 and~4.4 are significant though minor results, interesting enough to be included even though they are not used in the proofs of the major results of this paper. While well behaved derivations may not have much bearing on the study of all semi-Thue systems, they may prove fruitful in the study of systems with one rule. In particular, I am confident that the analysis of well behaved derivations in Sections~3, 5 and~7 --- as well as the study of overlaps and phrases in Section~4 --- will be central to further research on one-rule semi-Thue systems. {\em Notation and terminology:\/} A {\em semi-Thue system\/} is a finite set of rules of the form $u_i \rightarrow v_i$, where $u_i$ (left side) and $v_i$ (right side) are words. The set of all characters appearing in the rules (except the arrow) is the {\em alphabet\/} of the system. A {\em derivation\/} is a finite or infinite sequence of words $x_1 ,x_2 , \ldots$ over the alphabet, where for each $n \geq 1$ there is a rule $u_i \rightarrow v_i$ such that $x_n = x'u_i x''$ and $x_{n+1} = x'v_i x''$ for some words $x',x''$. The letters ``$u$'' and ``$v$'' are reserved letters in this paper; without subscript, they always denote, respectively, the left and right side of the unique rule of a one-rule system. If the number of rules is unspecified or specified as more than one, then ``$u_i$'' and ``$v_i$'' denote the left and right sides of the $i^{th}$ rule. The arrow is used to denote a rule. But it will also be used to assert the existence of a derivation of one step, i.e., a derivation of two lines; e.g., $x_n \rightarrow x_{n+1}$. The notation $x \rightarrow ^n y$ means that there is a derivation $x_0 ,x_1 , \ldots ,x_n$ where $x_0 = x$ and $x_n = y$. We write $x \rightarrow ^* y$ ($x \rightarrow ^+ y$) to mean $x \rightarrow ^n y$ for some $n \geq 0$ (for some $n \geq 1$). The null word is denoted by ``$\lambda$''. A word $x$ is a {\em factor\/} (or subword) of a word $y$ if there are words $x',x''$ such that $y = x'xx''$; if $x' \neq \lambda$ or $x'' \neq \lambda$ then $x$ is a {\em proper factor\/} of $y$; if $x' = \lambda$ then $x$ is a {\em prefix\/} of $y$ (a {\em proper prefix\/} if $x'' \neq \lambda$); if $x'' = \lambda$ then $x$ is a suffix of $y$ (a {\em proper suffix\/} if $x' \neq \lambda$). The rule itself will be used as the name of a one-rule semi-Thue system. For any word $x$, $|x|$ is the length of $x$. We note that if $u \rightarrow v$ is a system in which $|v| \leq |u|$ then the system is uniformly terminating if and only if $v \neq u$. Since the uniform termination question has an easy answer in this case, it is excluded from consideration. Noting also that when $u$ is a factor of $v$ the system always has an infinite derivation, this case is also excluded from consideration. Thus in the remainder of the paper it will be assumed that a one-rule semi-Thue system $u \rightarrow v$ has the properties that $|v| > |u|$ and that $u$ is a not a factor of $v$. In the remainder of this paper, the word ``system'' unmodified will be reserved to mean a one-rule semi-Thue system having both these properties. The phrase ``semi-Thue system'' will denote a semi-Thue system with finitely many rules. In this paper, $x \triangleright y$ ($x \triangleright ^n y$) means that, for some $y'$ and $y''$, $x \rightarrow y'yy''$ ($x \rightarrow ^n y'yy''$). The notations $\triangleright ^*$ and $\triangleright ^+$ are defined similarly as for the arrow. If $x \triangleright ^n x$ for $n \geq 1$ then the derivation $x_0 ,x_1 , \ldots , x_n$ where $x_0 = x$ and $x_n = x'xx''$ is called a {\em loop of length $n$\/} on $x$. Thus there is a loop on $x$ if and only if $x \triangleright ^+ x$. Clearly, if there is a loop in any semi-Thue system then there is an infinite derivation. A conjecture about a converse to this proposition is discussed in Section~2. The well known fan theorem states that an infinite rooted tree in which each node has only finitely many children nodes has an infinite path. The following generalization will be used twice in this paper: {\bf Theorem 1.1.} If a forest of finitely many rooted trees has infinitely many nodes, each of which has only finitely many children nodes, then the forest has an infinite path. \vspace{.5in} {\bf 2. Well behaved derivation defined.} The definition is in terms of the concept of {\em inhibitor.\/} After these definitions, two examples will be discussed. Finally, as the Main Theorem of this section, we shall prove that the problem of whether a given semi-Thue system has an infinite well behaved derivation is decidable. {\bf Definition (inhibitor).} If a semi-Thue system has a character that occurs at least once on the right side of every rule but does not occur on the left side of any rule then we say that character is an {\em inhibitor.\/} Our convention will be to use small Greek iota as an inhibitor. {\bf Definition (inhibited rule, inhibition system).} If $u_i \rightarrow v'v''$ is a rule of a semi-Thue system $T$ without $\iota$ then $u \rightarrow v' \iota v''$ is an {\em inhibited rule\/} of $T$. ($v'$ or $v''$ can be the null string.) The {\em inhibition system\/} of $T$ is the semi-Thue system whose rules are all the inhibited rules of $T$. An immediate consequence of this definition is {\bf Theorem 2.1.} If $x_1 ,x_2 , \ldots$ is a finite or infinite derivation in the inhibition system of the semi-Thue system $T$ then, where each $x'_i$ is $x_i$ with all $\iota$'s erased, $x'_1 ,x'_2 , \ldots$ is a derivation in $T$. {\bf Definition (well behaved, ill behaved).} A derivation $D$ in a semi-Thue system $T$ without $\iota$ is {\em well behaved\/} if there is a derivation in the inhibition system of $T$ from which $D$ is the result of deleting all $\iota$'s. Otherwise $D$ is {\em ill behaved.\/} {\bf Example 1.} The simplest system with an infinite well behaved derivation is the well known system $cb \rightarrow bbcc$. The inhibition system of this system has five rules: \[ cb \rightarrow \iota bbcc \] \[ cb \rightarrow b \iota bcc \] \[ cb \rightarrow bb \iota cc \] \[ cb \rightarrow bbc \iota c \] \[ cb \rightarrow bbcc \iota \] This system has an infinite derivation. In fact, the one-rule system $cb \rightarrow bb \iota cc$ has an infinite derivation based on the following loop of length 2: \[ c \underline{cb} \] \[ \underline{c} \overline{\underline{b} b \iota cc} \] \[ \overline{bb \iota cc} b \iota cc \] (In this and the examples to follow, the part of the line with an underscore is the occurrence of $u$ that is written as $v$ in the next line, which has an overscore.) Accordingly, the original system also has an infinite well behaved derivation based on the loop \[ c \underline{cb} \] \[ \underline{c} \overline{\underline{b} bcc} \] \[\overline{bbcc} bcc \] {\bf Example 2.} The following is an ill behaved derivation in the system with the one rule $ccb \rightarrow bbccc$ (a system of the kind studied by Zantema and Geser in \cite{zg}): \[ cc \underline{ccb}b \] \[ \underline{cc} \overline {\underline {b} bccc} b \] \[ \overline {bbc \underline {cc} } \underline {b} cccb \] \[ bbc \overline {bbccc} c \underline {ccb} \] \[ bbcbbcc \underline {cc} \overline { \underline {b} bccc} \] \[ bbcbbcc \overline {bbccc} bccc \] To prove that this derivation is ill behaved we note that the inhibition system has six rules, whose right sides are, respectively, $\iota bbccc$, $b \iota bccc$, $bb \iota ccc$, $bbc \iota cc$, $bbcc \iota c$ and $bbccc \iota$. Thus the second line in the corresponding derivation in the inhibition system has six possibilities. We leave it to the reader to verify that in each of these six cases the $\iota$ will inhibit the replacement of the occurrence of $bbc$ in one of the lines below. (For example, if the $ccb$ in the first line is rewritten as $bb \iota ccc$ in the second line then the $ccb$ in the fifth line cannot be rewritten.) However, the first five lines of the above derivation form a well behaved derivation, which can be verified by considering the following derivation in the inhibition system: \[ cc \underline {ccb} b \] \[ \underline {cc} \overline { \underline {b} bc \iota cc} b \] \[ \overline { \iota bbc \underline{cc}} \underline {b} c \iota ccb \] \[ \iota bbc \overline { \iota bbccc} c \iota \underline {ccb} \] \[ \iota bbc \iota bbcccc \iota \overline {bbccc \iota } \] \noindent If we delete all the $\iota$'s from this derivation we get the first five lines of the above derivation in $T$. The system $ccb \rightarrow bbccc$ has an infinite derivation, which is clear from the first five lines of our original derivation, which shows that \[ ccccbb~ \triangleright ^4 ccccbb \] \noindent The sixth line of this infinite derivation is the sixth line of the above derivation, which shows that the infinite derivation is ill behaved. This system has no infinite well behaved derivation. This fact could be verified by showing that the inhibition system has no infinite derivation, using the algorithm described below in the proof of Theorem~2.3. However, the application of this algorithm is tedious. In Section~8 we shall develop a more efficient algorithm for determining whether a given one-rule semi-Thue system has an infinite well behaved derivation. We shall return in Section~9 to this example and, with that algorithm, show that the system has no infinite well behaved derivation. {\bf Definition.} For any $x,x'$ and for any rule $u_i \rightarrow v_i$ of a semi-Thue system, if the word $xu_i x'$ contains no occurrence of the inhibitor $\iota$ and $y$ is a maximal factor of $xv_i x'$ not containing $\iota$, then we write $xu_i x' \models y$. For example, if $u_i = bc$, $v_i = bb \iota cd \iota dc$ then, since \[ b \underline{bc} c \rightarrow b \overline{bb \iota cd \iota dc} c \] we have $bbcc \models bbb$, $bbcc \models cd$ and $bbcc \models dcc$. {\bf Theorem 2.2.} A semi-Thue system $T$ with an inhibitor $\iota$ has an infinite derivation if and only if there exists an infinite sequence $x_1 ,x_2 , \ldots$ such that, for each $i$, (1) $|x_i| \leq 2e - 2$, where $e = max\{|v_j| | 1 \leq j \leq r \}$, and (2) $x_i \models x_{i+1}$. {\em Proof:\/} The existence of an infinite sequence satisfying (2) alone implies the existence of an infinite derivation, giving us the proof from right to left. For the proof the other way, assume $T$ has an infinite derivation $w_1 ,w_2 , \ldots~$. Each character occurrence of $w_1$ is either forever unchanged through the derivation or is replaced in some $w_i$. Since $w_1$ has finite length there exists $p_0$ such that for all $p \geq p_0$ no original character occurrence of $w_1$ is replaced in going from $w_p$ to $w_{p+1}$. (In other words, all the character occurrences of $w_1$ that have not been rewritten by line $p_0$ are never rewritten.) Thus, there exist strings $y_0 , \ldots , y_m$, occurring in that order as nonoverlapping substrings of $w_1$, such that for all $p \geq p_0$ \[ w_p = y_0 z_{p,1} y_1 z_{p,2} y_2 \cdots y_{m-1} z_{p,m} y_m \] \noindent and no character of any $z_{p,j}$ is an original character of $w_1$. Furthermore, for at least one $j$, $1 \leq j \leq m$, the sequence \[ z_{p_0 ,j} ~,~z_{p_0 +1,j}~,~z_{p_0 +2,j}~,~ \ldots \] is an infinite derivation in $T$, with repetitions. We delete repetitions from this sequence and renumber with single-integer indices, setting $z_1 = z_{p_0 ,j}$. Thus for each $i \geq 1$, we have $z_i \rightarrow z_{i+1}$. The sequence $z_1 ,z_2 , \ldots $ is an infinite derivation, which we call the $z$-derivation. Since $z_1$ contains no original character occurrences of $w_1$, every character occurrence in the $z$-derivation must be present in the original derivation as a result of some application of a rule. In each application at least one $\iota$ is introduced, which is never replaced. From this we see that, for each $i \geq 1$, there exist $q_i \geq 1$ and words $t_{i,1} ,t_{i,2} , \ldots ,t_{i,q_i}$ such that \[ z_i = t_{i,1} \iota t_{i,2} \iota \cdots \iota t_{i,q_i} \] where each $t_{i,h}$ is either a proper factor of some $v_i$ without any occurrence of $\iota$ or the concatenation of two such factors. Consequently, for each $i$ and $h$, $|t_{i,h}| \leq 2e - 2$. For each line $i$ there is exactly one $h$ such that $t_{i,h}$ is rewritten by a rule; it thus becomes (for some $s \geq 1$) $t_{i+1,h} \cdots t_{i+1,h+s}$ in the $(i+1)^{st}$ line ; for all $h' \neq h, 1 \leq h' \leq q_i$, the occurrence $t_{i,h'}$ is copied to become the very same $t$-factor in the $(i+1)^{st}$ line. We define $C'(,)$ to mean that $t_{i,h}$ is copied to become $t_{i+1,h''}$ in the $(i+1)^{st}$ line. We then define $C$ to be the transitive, symmetric and reflexive closure of the relation $C'$. Thus $C(,)$ holds if either (1)~$i=i'$ and $h = h'$, (2)~$i' > i$ and $t_{i,h}$ is copied, recopied, etc., until it becomes $t_{i',h'}$ in the $(i')^{th}$ line, or (3)~$i > i'$ and $t_{i',h'}$ is copied, recopied, etc., to become $t_{i,h}$. Clearly, $C$ is an equivalence relation; furthermore if $C(,)$ then $t_{i,h} = t_{i',h'}$. Note also that, for any $i$ and $h \leq q_i$, if there is no $h' \leq q_{i+1}$ such that $C(,)$ then there is at least one $h'$ such that $t_{i,h} \models t_{i+1,h'}$. We now draw a graph whose nodes are the equivalence classes of the $C$ relation. The roots are the classes having the respective pairs $<1,1>, \ldots ,<1,q_1>$ as members. There is an edge from a node $N_1$ to a node $N_2$ if and only if there are $i,h,h'$ such that $~ \in N_1$, $~ \in N_2$ and the occurrence of $t_{i+1,h'}$ in the $(i+1)^{st}$ line is obtained by rewriting from the occurrence $t_{i,h}$ in the $i^{th}$. Clearly, this graph is a forest of rooted trees. It is infinite, since the $z$-derivation is infinite. We note that for all $i,h,i',h'$ and $N$ if $~ \in N$ and $~ \in N$ then $t_{i,h} = t_{i'h'}$. Thus we define $t(N) = t_{i,h}$ for $~ \in N$. Applying Theorem~1.1, there is an infinite path through the graph: $N_1,N_2, \ldots ~$. Putting $x_j = t(N_j)$ for all $j$ we have (1)~$|x_j| \leq 2e - 2$ and (2)~$x_j \models x_{j+1}$ for all $j$.$\Box$ {\bf Theorem 2.3.} It is decidable whether a given semi-Thue system with an inhibitor has an infinite derivation. {\em Proof:\/} Note Theorem 2.2. Let $s+1$ be the number of characters in the system's alphabet. Given words $x,x'$ over this alphabet but without the inhibitor $\iota$, it is easy to decide whether $x \models x'$. There exists an infinite sequence $x_1 ,x_2 , \ldots$ such that $|x_i | \leq 2e - 2$ and $x_i \models x_{i+1}$ for each $i$ if and only if there exists a finite such sequence $x_1 , \ldots , x_n$, such that $ n \leq s^{2e-2}$ and $x_n \models x_1$. Since the latter is decidable for a given system so is the former.$\Box$ {\bf Theorem 2.4.} A semi-Thue system with an inhibitor has an infinite derivation if and only if it has a derivation loop. {\em Proof:\/} As remarked in Section~1, any semi-Thue system with a derivation loop has an infinite derivation. Conversely, a system with an inhibitor and an infinite derivation has an infinite $\models$ sequence by Theorem~2.2, and hence a $\models$ loop by the proof of Theorem~2.3. >From the $\models$ loop, a derivation loop is easily constructed.$\Box$ \newpage The following two theorems are consequences of previous theorems: {\bf Theorem 2.5 (Main Theorem).} It is decidable whether a given semi-Thue system has an infinite well behaved derivation. {\bf Theorem 2.6.} A semi-Thue system with an infinite well behaved derivation has~a~loop. {\bf Conjecture.} Every one-rule semi-Thue system with an infinite derivation has a loop. If this conjecture turns out to be false then there must be a one-rule semi-Thue system with an infinite ill behaved derivation, and in which no infinite derivation is based on a loop. \vspace{.5in} {\bf 3. Analysis of derivations.} In this section, the concept of {\em trace \/} is introduced, leading to a new characterization of well behaved derivations. This concept will be central to the entire paper. It is developed in this section broadly enough to apply to well behaved and ill behaved derivations alike. Further development in Sections~5 and~7 will be applicable to well behaved derivations only. Consider the $n + 1$ positions in a string of length $n$: the position just to the left of the string, the position just to the right, and the $n - 1$ positions between the letters. For example, the six positions of the string $aabaa$ are shown graphically by placing six slashes thus: \[ /a/a/b/a/a/ \] When a line in a derivation is rewritten as the next line, it is natural to think of some positions in the new line as being the ``same'' as some positions in the old line and other positions as being created. Consider the following two-line derivation in the system $ccb \rightarrow bbccc$: \[ cc \underline{ccb} b \] \[ cc \overline{bbccc} b \] Let the seven positions in the first line be, in order from left to right, $p_0 ,p_1 , \ldots ,p_6$ and let the nine positions in the second line be $q_0 , q_1 , \ldots ,q_8$. It is natural to think that $p_0 = q_0$, $p_1 = q_1$, $p_2 = q_2$, $p_5 = q_7$ and $p_6 = q_8$. It is also natural to think of $p_3$ and $p_4$ as being destroyed and $q_3 , \ldots ,q_6$ as being created in the act of rewriting. It is helpful to define {\em traces\/} of positions: two positions are in the same trace when they are intuitively thought of as being the same position. We present these ideas formally as follows: {\bf Definition (position).} Where $z$ is a string and $z = z'z''$ we represent the $(|z'| + 1)^{st}$ {\em position\/} of $z$ from the left as $(z',z'')$. In particular, if $z' = \lambda$ then $(z',z'')$ is the {\em left-most position\/} of $z$ and if $z'' = \lambda$ then it is the {\em rightmost position.\/} {\bf Definition (trace).} Assume $x_1 ,x_2 , \ldots$ is a finite or infinite derivation. For $x_i = x'_i x''_i$ and $x_{i+1} = x'_{i+1} x''_{i+1}$, we define $R'((x'_i ,x''_i),(x'_{i+1} ,x''_{i+1} ))$ to mean that either $x'_i = x'_{i+1}$, $x''_i = y_1 u_j y_2$ and $x''_{i+1} = y_1 v_j y_2$ or else $x''_i = x''_{i+1}$, $x'_i = y_1 u_j y_2$ and $x'_{i+1} = y_1 v_j y_2$, for some $y_1$ and $y_2$ and rule $u_j \rightarrow v_j$. We let $R$ be the transitive, symmetric closure of $R'$, and define the {\em traces\/} of the derivation to be the equivalence classes of $R$. If $x_i = su_j t$ and $x_{i+1} = sv_j t$, note that the position $(s,u_j t)$ in the $i^{th}$ line and $(s,v_j t)$ in the $(i+1)^{th}$ are in the same trace; $(su_j ,t)$ and $(sv_j ,t)$ are in the same trace; and all the positions to the left of $(s,u_j t)$ and all those to the right of $(su_j ,t)$ in the $i^{th}$ line are in the same traces, respectively, as similarly placed positions in the $(i+1)^{st}$ line. But none of the remaining positions in the $i^{th}$ line (namely, those internal to the noted occurrence of $u_j$) is $R$-equivalent to any position in the $(i+1)^{st}$ line. {\bf Definition (traces destroyed and created, border traces).} If $su_j t$ and $sv_j t$ are the $i^{th}$ and $(i+1)^{st}$ lines of a derivation then the traces of the positions internal to the noted $u_j$ in the $i^{th}$ line are {\em destroyed\/} in the $(i+1)^{st}$ line, and the traces internal to the noted occurrence of $v_j$ in the $(i+1)^{st}$ line are {\em created\/} there. The traces of the two positions $(s,v_j t)$ and $(sv_j ,t)$ of $x_{i+1}$ are the {\em border traces\/} of that line. The reader may wonder why we have focused on positions between character occurrences of a string, and why we have considered traces of these positions rather than traces of the character occurrences themselves. A brief answer is that the concept of {\em well behaved derivation\/} depends on something more that the destruction of characters and the creation of other characters when we apply a rule of a semi-Thue system. We shall return to this matter after the next theorem, which should help to make clear the relationship between the concept of {\em traces of positions\/} and the concept of {\em well behaved derivation.\/} {\bf Theorem 3.1.} A derivation $D$ in a semi-Thue system $T$ is well behaved if and only if, for each line other than the first, there is at least one trace that is either a created trace or a border trace of that line and is never destroyed in the derivation. {\em Proof:\/} Consider the inhibition system $T'$ of $T$. If $D$ is well behaved then, by definition, there is a derivation $D'$ in $T'$ which becomes $D$ by having all it $\iota$'s erased. Consider the $(i+1)^{st}$ line in $D$ and $D'$. In $D'$ a new $\iota$ must be inserted in the $(i+1)^{st}$ line; this $\iota$ must correspond to a position in the $(i+1)^{st}$ line of $D$ that is either a created trace or a border trace in that line. That position is never destroyed in $D$ because of the $\iota$ that appears in the corresponding place in $D'$. Thus $D$ satisfies the condition of our theorem. It is easy to reverse the reasoning in the above paragraph and prove that if $D$ satisfies the condition of our theorem then there is a derivation $D'$ in $T'$ that becomes $D$ when all $\iota$'s are erased.$\Box$ \newpage For example, consider the following well behaved derivation in the system whose only rule is $dbc \rightarrow cdbdb$: \[ db \underline {dbc} c \] \[ \underline {db} \overline {\underline {c} /dbdb} c \] \[ \overline {cdbdb} /db \underline {dbc} \] \[ cdbdb/ \underline {db} \overline {\underline {c} dbdb} \] \[ cdbdb/ \overline {cdbdb} dbdb \] It is easy to see that the leftmost trace created in the third line and the rightmost trace created in the fourth line are not destroyed in the derivation. (The same is also true of the left border trace of the third line and the right border trace of the fourth line.) It is perhaps a bit more difficult to see that the leftmost trace created in the second line is also not destroyed in the derivation; as a visual aid, slashes have been placed in all the positions of that trace. Thus the derivation is well behaved. The reader should also note that, although there exists a trace created in the second line that is not later destroyed, all the character occurrences created in the second line are destroyed later in the derivation. This is the reason that well behaved derivations have to be characterized in terms of ``traces of positions'' and cannot be characterized in terms of a concept of {\em traces of characters,\/} which is not even formally defined in this paper. The remainder of this section is restricted to one-rule semi-Thue systems. {\bf Definition (${\bf TR_{j,i}}$, border traces of ${\bf TR_{j,j}}$).} For $j \geq 2$, $TR_{j,j}$ is the set of traces created in the $j^{th}$ line of a derivation in the system $u \rightarrow v$, together with the two border traces of that line, henceforth to be called the {\em left border trace of\/} $TR_{j,j}$ and the {\em right border trace of\/} $TR_{j,j}$. For $i > j \geq 2$, $TR_{j,i}$ is the subset of those traces of $TR_{j,j}$ present in the $i^{th}$ line. The use of this notation presupposes a derivation in a one-rule semi-Thue system, often not mentioned explicitly. An immediate consequence of these definitions is {\bf Theorem 3.2.} If $i > i' \geq j$ then $TR_{j,i} \subseteq TR_{j,i'}$. As an illustration of this definition consider the fourth line in the derivation given above for the system $dbc \rightarrow cdbdb$. That line has length $12$ and hence has $13$ positions. Let the traces of these positions be, in order from left to right, $t_0,t_1, \ldots , t_{12}$. Then $TR_{4,4} = \{ t_i | 7 \leq i \leq 12 \}$, with $t_7$ its left border trace and $t_{12}$ its right border trace ; $TR_{2,4} = \{ t_5 ,t_6 ,t_7 \}$; and $TR_{3,4} = \{ t_i | 0 \leq i \leq 5 \}$. Thus all of the traces present in the original line have been destroyed by line $4$. Note that $TR_{2,4} \cap TR_{4,4} = \{ t_7 \}$ and $TR_{3,4} \cap TR_{2,4} = \{ t_5 \}$. The trace $t_5$ (whose positions have the slashes) was the right border trace of $TR_{3,3}$. {\bf Theorem 3.3.} If $i \geq j > j'$ and $t \in TR_{j,i} \cap TR_{j',i}$ then $t$ is a border trace of $TR_{j,j}$. {\em Proof by induction on $i$:\/} For $i = j$, the assumption is $t \in TR_{j,j} \cap TR_{j',j}$. Since $t \in TR_{j',j} \subseteq TR_{j',j'}$, $t$ already exists before the $j^{th}$ line and hence is not created in the $j^{th}$ line. Thus, from the fact that $t \in TR_{j,j}$, $t$ must be a border trace of $TR_{j,j}$. Assume now as an inductive hypothesis that our theorem is true for $i \geq j$ and let $t$ be a trace in $TR_{j,i+1} \cap TR_{j',i+1}$. By Theorem~3.2, $t \in TR_{j,i} \cap TR_{j',i}$. Thus by the inductive hypothesis, $t$ is a border trace of $TR_{j,j}. \Box$ {\bf Definition (left, right, consecutive).} Trace $t$ is {\em to the left of\/} trace $t'$ if there is a line in which $t$ and $t'$ are both present and the position of $t$ in that line is to the left of the position of $t'$. (Note that if the position of $t$ is to the left of the position of $t'$ in any line then the same is true for any line in which both $t$ and $t'$ are present.) A set $T$ of traces present in line $i$ is {\em consecutive} in line $i$ if, for all $t,t',t''$ in left-to-right order in line $i$, if $t \in T$ and $t'' \in T$ then $t' \in T$. {\bf Definition (${\bf w(T)}$).} If $T$ is a consecutive set of traces present in line $i$ of a derivation then the word $w_i (T)$ is the factor of the $i^{th}$ line formed by the characters in order from the leftmost trace of $T$ to the rightmost. (For example, if $T$ is the set of traces of the six positions shown by the slashes in the following depiction of line $i$ \[ bbab/a/a/b/a/a/abab \] then $w_i (T) = aabaa$.) Note that $w_i (T) = w_j (T)$ if all the traces of $T$ are present in both lines $i$ and $j$. Thus we define $w(T) = w_i (T)$ for any $i$ such that all the traces of $T$ are present in line $i$. {\bf Definition (${\bf S_{i+1}}$).} In a derivation, $S_{i+1}$ is the set of traces of the $i^{th}$ line destroyed in the $(i+1)^{st}$ line. Note that $S_{i+1}$ is consecutive and that, if $u = au'b$ then $w(S_{i+1}) = u'$. {\bf Theorem 3.4.} For $i \geq j$, if $TR_{j,i}$ is nonempty then it is consecutive and $w(TR_{j,i})$ is a factor of $v$. {\em Proof by induction on $i$:\/} For $i = j$, $TR_{j,j}$ is clearly consecutive and $w(TR_{j,j}) = v$. Assuming that $TR_{j,i}$ is consecutive and $w(TR_{j,i})$ is a factor of $v$, we have $TR_{j,i+1} = TR_{j,i} - S_{i+1}$. If $TR_{j,i} \cap S_{i+1} \neq \emptyset$ then let the traces of $TR_{j,i}$ in left-to-right order be $t_1 , \ldots , t_h$. Since both $TR_{j,i}$ and $S_{i+1}$ are consecutive, if $TR_{j,i+1}$ is not consecutive then $S_{i+1}$ is entirely inside $TR_{j,i}$ and neither $t_1$ nor $t_h$ is in $S_{i+1}$. But that would imply that $u$ is a factor of $w(TR_{j,i})$ and hence of $v$, which has been disallowed. So $TR_{j,i+1}$ is consecutive; and $w(TR_{j,i+1})$ is a factor of ~$v$, since $w(TR_{j,i})$ is. On the other hand, if $TR_{j,i} \cap S_{i+1} = \emptyset$ then $TR_{j,i+1} = TR_{j,i}.\Box$ {\bf Theorem 3.5.} For $i \geq j$, if $TR_{j,i} \neq TR_{j,i+1} \neq \emptyset$ then $TR_{j,i} - TR_{j,i+1}$ (the subset of $TR_{j,i}$ destroyed in line $i+1$) is either entirely to the left or entirely to the right of $TR_{j,i+1}$ (the subset not destroyed). {\em Proof:\/} Let $A = TR_{j,i} - TR_{j,i+1}$. $A$ is a consecutive set since it is the intersection of two consecutive sets, $S_{i+1}$ and $TR_{j,i}$. The set $TR_{j,i+1}$ is also a consecutive set. But $A \cap TR_{j,i+1} = \emptyset$. Thus $A$ is either entirely to the left or entirely to the right of $TR_{j,i+1} . \Box$ {\bf Theorem 3.6.} If $i \geq j,j'$ and $j \neq j'$ then $|TR_{j,i} \cap TR_{j',i} | \leq 1$. {\em Proof:\/} Without loss of generality, assume $j > j'$. By Theorem~3.3, $I = TR_{j,i} \cap TR_{j',i} \subseteq \{ t_1 ,t_2 \}$, where $t_1$ and $t_2$ are the two border traces of $TR_{j,j}$. We complete our proof by showing that $I = \{ t_1 ,t_2 \}$ leads to contradiction: Since $TR_{j,i}$ and $TR_{j',i}$ are consecutive, their intersection $I$ is consecutive. Since all traces of $TR_{j,j}$ are between $t_1$ and $t_2$, we see that if $t_1$ and $t_2$ are both in $I$ then $TR_{j,j} = I$. Hence $|TR_{j,j}| = 2$, from which we infer that $|v| = |w(TR_{j,j})| = 1$. But this is impossible, by our stipulations (see Section~1) that $|v| > |u|$ and that $u$ is not a factor of $v. \Box$ {\bf Theorem 3.7.} For $j \neq j'$, $i \geq j$ and $i \geq j'$, if $TR_{j,i} \cap TR_{j',i} = \emptyset$, then either all the traces of $TR_{j,i}$ are to the left of those of $TR_{j',i}$ or else they are all to the right. Otherwise, $TR_{j,i} \cap TR_{j',i} = \{ t \}$, where $t$ is the leftmost trace of one and the rightmost trace of the other. The proof is immediate from Theorem~3.6 and the fact that each of $TR_{j,i}$ and $TR_{j',i}$ is a consecutive set.$\Box$ The following theorem is not used in this paper. It is included because it seems like a potentially fruitful result for future research: {\bf Theorem 3.8.} For $j,j' \leq i$ and $j \neq j'$, if $TR_{j,i}$ and $TR_{j',i}$ have a trace in common and otherwise $TR_{j,i}$ is to the left of $TR_{j',i}$, then either $j > j'$ and $w(TR_{j,i})$ is a suffix of $v$ or else $j' > j$ and $w(TR_{j',i})$ is a prefix of $v$. {\em Proof by induction on $i$:\/} For $i = 1$ our theorem is vacuously true. Assume for a given $i$ that our theorem is true for $i$. We must prove that it is true for $i + 1$. Accordingly, let $j$ and $j'$ be any two distinct integers such that $TR_{j,i+1}$ is to the left of $TR_{j',i+1}$ in line $i+1$, except for $t \in TR_{j,i+1} \cap TR_{j',i+1}$. By Theorem~3.3, $t$ is a border trace of $TR_{j,j}$ if $j > j'$, and is a border trace of $TR_{j',j'}$ if $j' > j$. Case I: $j = i + 1$. Then $j > j'$ and $w(TR_{j,i+1}) = v$. Case II: $j' = i + 1$. Then, $j' > j$ and $w(TR_{j',i+1}) = v$. Case III: $j,j' < i+1$. By Theorem~3.2, $t \in TR_{j,i+1}$ implies $t \in TR_{j,i}$, and $t \in TR_{j',i+1}$ implies $t \in TR_{j',i}$, so $t \in TR_{j,i} \cap TR_{j',i}$. By the inductive hypothesis, therefore, either $j > j'$ and $w(TR_{j,i})$ is a suffix of $v$ or $j' > j$ and $w(TR_{j',i})$ is a prefix of $v$. By Theorem~3.7, $t$ is at the right end of both $TR_{j,i}$ and $TR_{j,i+1}$, and is at the left end of both $TR_{j',i}$ and $TR_{j',i+1}$. Hence by Theorem~3.4, $w(TR_{j,i+1})$ is a suffix of $w(TR_{j,i})$ and $w(TR_{j',i+1})$ is a prefix of $w(TR_{j',i})$. Therefore, the inductive hypothesis implies that either $j > j'$ and $w(TR_{j,i+1})$ is a suffix of $v$ or $j' > j$ and $w(TR_{j',i+1})$ is a prefix of $v.\Box$ The last theorem of this section will have an application in the proof of Theorem~7.4: {\bf Theorem 3.9.} Assume line $1$ and line $i$ of a derivation have no traces in common, and let $TR_{j_1 ,i} ,TR_{j_2 ,i} , \ldots , TR_{j_p ,i}$ be in left-to-right order all the sets $TR_{j,i}$ such that $|TR_{j,i} | \geq 2$. Then the leftmost (rightmost) trace of line $i$ is the leftmost (rightmost) trace of $TR_{j_1 ,i}$ (of $TR_{j_p ,i}$). And for each $h$, $1 \leq h \leq p-1$, the rightmost trace of $TR_{h,i}$ is the same as the leftmost trace of $TR_{h+1,i}$. {\em Proof:\/} {\bf Lemma.} For every $i'$ and for every pair of consecutive traces $s_1$ and $s_2$ in line $i'$, either $s_1$ and $s_2$ are both traces existing in line $1$ or, for some $j$, $2 \leq j \leq i'$, both $s_1$ and $s_2 \in TR_{j,i'}$. {\em Proof of the lemma by induction on $i'$:\/} Clearly, the lemma holds for $i' = 1$. For $i' \geq 1$ assume the lemma is true for $i'$, and let $s_1 ,s_2$ be any two consecutive traces in line $i'+1$. Let the traces of line $i'$ be $t_0 , \ldots ,t_q$, in order from left to right, where $t_h ,t_{h+1} , \ldots ,t_{h+k}$ are the traces in left-to-right order that are destroyed in line $i'+1$ ($|u| = k + 2$). Then the traces of line $i'+1$ are \[ t_0 \ldots ,t_{h-1} ,t'_1 , \ldots t'_m ,t_{h+k+1} , \ldots ,t_q \] where $t'_1 , \ldots ,t'_m$ are the traces created in line $i'+1$ ($|v| = m + 1$). Note that, by the inductive hypothesis, the lemma is true in line $i'+1$ for all consecutive pairs $s_1 ,s_2$ of traces except possibly for $s_1 = t_{h-1} ,s_2 = t'_1$ and for $s_1 = t'_m ,s_2 = t_{h+k+1}$. But the lemma holds for both of those pairs by virtue of the fact that $t_{h-1} ,t'_1 ,t'_m ,t_{h+k+1}$ are all in $TR_{i'+1,i'+1}.\Box$ To conclude the proof of Theorem~3.9, the leftmost line in line~$i$, since it does not appear in line~$1$, must be the leftmost trace of $TR_{j_1 ,i}$. Likewise, the rightmost trace of line~$i$ must be the rightmost trace of $TR_{j_p,i}$. Finally, if $t$ is the rightmost trace in $TR_{h,i}$ ($1 \leq h \leq p-1$) then, by the Lemma, $t$ and the next trace to its right in line~$i$ must both be in $TR_{h+1,i}$. By Theorem~3.7, $t$ is the leftmost trace of $TR_{h+1,i} .\Box$ \vspace{.5in} {\bf 4. Overlaps and phrases.} These two concepts play an important role in the later sections of this paper. After the definitions, this section will supply evidence to show that they would be important in any attack on the uniform termination problem for one-rule semi-Thue systems. The Main Theorem asserts that any system $u \rightarrow v$ that does not have at least one left overlap and at least one right overlap is uniformly terminating. {\bf Definition (overlap, phrase).} A nonnull word $x$ is a {\em left overlap (right overlap)\/} of the system $u \rightarrow v$ if there are nonnull words $u',v'$ such that $u = u'x$ and $v = xv'$ ($u = xu'$ and $v = v'x$). The word $u'$ is the {\em companion left phrase (right phrase)} to $x$. {\bf Theorem 4.1.} Where $u \rightarrow v$ is a system with no right overlap, let $p \geq 0$ and, for $1 \leq i \leq p$, let $v_i$ be a nonnull suffix of $v$. If $yvv_p v_{p-1} \cdots v_1 z \rightarrow x$ then one of the following holds: \begin{quotation} (A) For some $y'$, $y \rightarrow y'$ and $x = y'vv_p \cdots v_1 z$. (B) For some $z'$, $z \rightarrow z'$ and $x = yvv_p \cdots v_1 z'$. (C) For some $y'$ and $v_{p+1}$ a nonnull suffix of $v$, $x = y'vv_{p+1} v_p \cdots v_1 z$ and $|y'| < |y|$. \end{quotation} {\em Proof:\/} Implicit use is made of the stipulations (see Section~1) that $|u| < |v|$ and that $u$ is not a factor of $v$. The factor $u$ in the word \[ y/vv_p \cdots v_1 /z \] cannot begin anywhere properly between the first slash and the second slash; nor can it begin at the first slash. For if it did it would either be a factor of $v$ or would imply the existence of a right overlap of the system. (For example, if it were a factor of $v_p v_{p-1}$ but not of $v_p$ or of $v_{p-1}$ then some nonnull proper prefix of $u$ would be a suffix of $v_p$ and hence a suffix of $v$, and would therefore be a right overlap of the system.) Thus if neither (A) nor (B) holds then, since $|u| < |v|$, the $u$ to be rewritten must be situated so that it is a factor of $yv$ but not a factor of $y$ or of $v$. Thus there exist $y', \gamma \neq \lambda , \delta \neq \lambda$ and $v_{p+1}$ such that $y = y' \gamma$, $v = \delta v_{p+1}$ and $u = \gamma \delta$. To verify (C), note that $|y'| < |y|$, the result of rewriting is $x = y'vv_{p+1} v_p \cdots v_1 z$ and $v_{p+1}$ is a suffix of $v_1$. We also have $|v_{p+1} | > 0$, since $| \delta | < |u| < |v|$ and $|v_{p+1} | = |v| - | \delta |. \Box$ {\bf Definition (form F).} A word $w$ has {\em form F\/} if, for some $p \geq 0$ and nonnull suffixes $v_1 , \ldots , v_p$ of $v$, $w = vv_p \cdots v_1$. {\bf Theorem 4.2.} If the system $u \rightarrow v$ has no right overlap and $y_1 \beta _1 y_2 \cdots y_m \beta _m y_{m+1} \rightarrow x$ where each $\beta _i$ has form F, then $x = y'_1 \beta '_1 y'_2 \cdots y'_n \beta '_n y'_{n+1}$ where each $\beta '_i$ has form F and $\sum_{i=1}^{n+1} |y'_i | < \sum_{i=1}^{m+1} |y_i|$. {\em Proof:\/} If the $u$ to be rewritten in $y_1 \beta _1 y_2 \cdots y_m \beta _m y_{m+1}$ is a factor of $y_i = y'_i uy''_i$ then \[ x = y_1 \beta _1 y_2 \cdots y_{i-1} \beta _{i-1} y'_i v y''_i \beta _i y_{i+1} \cdots y_m \beta _m y_{m+1} \] This expression is as required by our theorem since $v$ has form F and $|y'_i | + |y''_i | = | y_i | - |u|$. As we observed in the proof of Theorem~4.1, $u$ cannot be a factor of $\beta _i$ for any $i$, and it cannot overlap $\beta _i$ and the remainder of the word to the right. Thus if it is not a factor of any $y_i$, the $u$ to be rewritten must be a factor of some $y_i \beta _i$ but not a factor either of $y_i$ or of $\beta _i$; by Theorem~4.1, there are $y'_i$ and $\beta'_i$ in form F (obtained from $y_i$ and $\beta _i$ as in the proof of Theorem~4.1) such that \[ x = y_1 \beta _1 y_2 \cdots y_{i-1} \beta _{i-1} y'_i \beta '_i y_{i+1} \cdots y_m \beta _m y_{m+1} \] This expression is as required since $|y'_i | < |y_i |. \Box$ {\bf Theorem 4.3.} A system $u \rightarrow v$ with no right overlap has no infinite derivation. {\em Proof:\/} For any word $w$ let $f(w) = |w|$ if $w$ has no factor of form F. Otherwise, let $f(w) = \sum_{i=1}^{m+1} y_i$, where the parsing \[ w = y_1 \beta _1 y_2 \cdots y_m \beta _m y_{m+1} \] is that parsing of $w$ in which all $\beta_i$'s have form F and $\sum_{i=1}^{m+1} |y_i |$ is minimized. By Theorem~4.2, if $w \rightarrow x$ then $f(x) < f(w)$. Since there is no infinite descending sequence of nonnegative integers, there is no infinite derivation in the system $u \rightarrow v. \Box$ {\bf Theorem 4.4 (Main Theorem).} A system $u \rightarrow v$ that does not have both a left overlap and a right overlap has no infinite derivation. {\em Proof:\/} By left-right symmetry from Theorem~4.3, if the system has no left overlap it has no infinite derivation.$\Box$ The final two theorems of this section will be useful in later sections: {\bf Theorem 4.5.} If $\alpha$ is a right phrase then $v \alpha x \triangleright vx$ for any $x$. If $\beta$ is a left phrase then $y \beta v \triangleright yv$ for any $y$. {\em Proof:\/} Let $\alpha ' \alpha = \beta \beta ' = u$, where $\alpha '$ is a right overlap and $\beta '$ is a left overlap. Then, for some $v'$, $v \alpha x = v' \alpha ' \alpha x \rightarrow v'vx$. And, for some $v''$, $y \beta v = y \beta \beta 'v'' \rightarrow yvv''.\Box$ {\bf Theorem 4.6.} If $v = \alpha _1 \alpha _2 \cdots \alpha _p \eta \beta _q \cdots \beta _2 \beta _1$, where $p,q \geq 1$, $\alpha _1$ is a left overlap with $\alpha ' _1 \alpha _1 = u$, $\beta _1$ a right overlap with $\beta _1 \beta '_1 = u$, $\alpha _2 , \ldots , \alpha _p$ are right phrases and $\beta _2 , \ldots , \beta _q$ are left phrases, then $\alpha ' _1 u \beta '_1 \triangleright ^{p+q+1} v \eta v$. {\em Proof:\/} We derive \[ \alpha '_1 u \beta '_1 \] \[ \rightarrow \alpha '_1 v \beta '_1 = \alpha '_1 \alpha _1 \cdots \alpha _p \eta \beta _q \cdots \beta _1 \beta '_1 \] \[ \rightarrow ^2 v \alpha _2 \cdots \alpha _p \eta \beta _q \cdots \beta _2 v \] By applying Theorem~4.5 $p-1$ times we get \[ v \alpha _2 \cdots \alpha _p \eta \beta _q \cdots \beta _2 v \triangleright ^{p-1} v \eta \beta _q \cdots \beta _2 v \] And by applying it $q-1$ times we get \[ v \eta \beta _q \cdots \beta _2 v \triangleright ^{q-1} v \eta v. \Box \] Thus overlaps are important in the problem of whether a given system $u \rightarrow v$ is uniformly terminating. It seems that we should be able to make an assertion that is stronger than the main theorem: {\bf Conjecture.} If a system $u \rightarrow v$ has an infinite derivation then $v$ has both a prefix of the form $\alpha \beta$, where $\alpha$ is a left overlap and $\beta$ is a right phrase, and a suffix of the form $\delta \gamma$, where $\gamma$ is a right overlap and $\delta$ is a left phrase. As I announced in \cite{mcn} without proof, this conjecture is true when limited to systems $u \rightarrow v$ in which $u$ has no self overlap, i.e., systems in which there exist no $\alpha , \beta , \gamma \neq \lambda$ such that $u = \alpha \beta = \beta \gamma$. The parsing of $v$ in which one or more right phrases follow a left overlap at the left end, and one or more left phrases precede a right overlap at the right end, is used in two ways in later sections. I believe that such parsings will play an even more important role in the study of the uniform termination problem for one-rule semi-Thue systems. It is for this reason that the Main Theorem is so named in spite of the fact that it is not referred to explicitly in the remander of the paper. \vspace{.5in} {\bf 5. Analysis of well behaved derivations.} This section lays the groundwork for the next section, which will present an algorithm to determine whether a given one-rule semi-Thue system has an ill behaved derivation. The algorithm turns on the fact that if there is an ill behaved derivation then there is one of finite minimal length, which becomes a well behaved derivation if its last line is deleted. Thus the algorithm for determining whether there is an ill behaved derivation requires an analysis of well behaved derivations. That analysis is given in this section, continuing the more general analysis of Section~3 (which applies to well behaved and ill behaved derivations alike) and using the concepts of {\em overlap\/} and {\em phrase.\/} The Main Theorem gives a syntactic solution to the following problem: given a system $u \rightarrow v$ and a word $\eta$, does there exist a well behaved derivation in which $\eta = w(TR_{j,i})$ for some $i$ and $j$? {\bf Definition.} We write $L(j,j',i)$ to mean that, in line $i$ of a derivation, every trace of $TR_{j,i}$ is to the left of every trace of $TR_{j',i}$, except for the trace they have in common (if any). {\bf Theorem 5.1.} In a well behaved derivation, if $J_i = \{ j|TR_{j,i} \cap S_{i+1} \neq \emptyset \}$ then $|J_i| \leq 2$. ( Recall from Section~3 that $S_{i+1}$ is the set of traces of line~$i$ destroyed in line~$i+1$.) {\em Proof:\/} Assume $|J_i| \geq 3$ and $j_1 ,j_2 ,j_3 \in J_i$, $j_1 \neq j_2 \neq j_3 \neq j_1$. Without loss of generality assume $L(j_1 ,j_2 ,i)$ and $L(j_2 ,j_3 ,i)$. Since each of the sets $TR_{j_1 ,i}$, $TR_{j_2 ,i}$, $TR_{j_3 ,i}$ and $S_{i+1}$ is a consecutive set, we have $TR_{j_2 ,i} \subseteq S_{i+1}$. It follows that all of $TR_{j_2 ,j_2}$ is destroyed in the derivation, violating Theorem~3.1.$\Box$ {\bf Definition (destroyed from the left and right).} A trace of $TR_{j,i}$ is {\em destroyed from the left (from the right)\/} in line~$i+1$ if that trace and all traces of $TR_{j,i}$ to its left (to its right) are destroyed in line~$i+1$. {\bf Theorem 5.2.} In a well behaved derivation, if some traces of $TR_{j,i}$ are destroyed in line~$i+1$, then either these traces are all destroyed from the left leaving at least one trace from the right end of $TR_{j,i}$ in $TR_{j,i+1}$, or else they are all destroyed from the right leaving at least one at the left end. {\em Proof:\/} Since the derivation is well behaved, not all the traces of $TR_{j,i}$ are destroyed in line $i+1$. Thus Theorem~5.2 follows from Theorem~3.5.$\Box$ {\bf Theorem 5.3.} In a well behaved derivation, if $TR_{j_1 ,i} \cap TR_{j_2 ,i} = \{ t \}$ and $L(j_1 ,j_2 ,i)$, then some traces of $TR_{j_1 ,i}$ are destroyed from the right in line $i+1$ if and only if some traces of $TR_{j_2 ,i}$ are destroyed from the left in that line. {\em Proof:\/} If traces of $TR_{j_1 ,i}$ are destroyed from the right but no traces of $TR_{j_2 ,i}$ are destroyed from the left, then (1)~no traces of any $TR_{j',i}$ are destroyed for $L(j_2 ,j',i)$, (2)~no traces of any $TR_{j',i}$ are destroyed for $L(j',j_1 ,i)$, (since the leftmost trace of $TR_{j_1 ,i}$ is not destroyed, by Theorem~5.2). All traces destroyed would be from $TR_{j_1 ,i}$, implying that $u$ is a factor of $w(TR_{j_1 ,i})$ and thus a factor of $v$. A similar contradiction would follow if traces were destroyed from $TR_{j_2 ,i}$ but not from $TR_{j_1 ,i} . \Box$ As an immediate consequence of Theorem~5.3 we get {\bf Theorem 5.4.} In a well behaved derivation, if $i > j' > j$, $TR_{j',j'} \cap TR_{j,j'} = \{ t \}$ and $L(j',j,j')~~(L(j,j',j'))~$ then no traces of $TR_{j,j'}$ are destroyed from the left (right) in lines $j' + 1$ through $i$ if and only if no traces of $TR_{j',j'}$ are destroyed from the right (left) in those lines. We continue our analysis of well behaved derivations, the objective being to give a structural analysis of the relationship of $w(TR_{j,i})$ to $v = w(TR_{j,j})$ when $i > j$. This objective will be achieved in Theorem~5.9, although Theorems~5.7 and~5.8 will also be useful in Section~6. {\bf Theorem 5.5.} If line $r_1$ of a well behaved derivation is the first line in which traces of $TR_{j,j}$ ($r_1 > j$) are destroyed from the left then there is a left overlap $\alpha _1$, which is a prefix of $w(TR_{j,r_1 -1})$, which is a prefix of $v = w(TR_{j,j})$, such that $w(TR_{j,r_1 -1}) = \alpha _ 1 w(TR_{j,r_1})$. {\em Proof:\/} The $u$ of line $r_1 -1$ that is to be rewritten in line $r_1$ must overlap on the right with $w(TR_{j,r_1 -1})$. Since no traces of $TR_{j,j}$ are destroyed from the left in lines $j+1$ through $r_1 -1$, $w(TR_{j,r_1 -1})$ is a prefix of $v = w(TR_{j,j})$. By virtue of the rewriting that yields line $r_1$, we have $w(TR_{j,r_1 -1}) = \alpha _1 w(TR_{j,r_1})$, where $\alpha _1$ is a nonnull prefix of $v$ and hence fulfills the definition of ``left overlap.''$\Box$ {\bf Theorem 5.6.} If traces of $TR_{j,j}$ are destroyed from the left in lines $r_i$ and $r_{i+1}$ but not in the lines between, then there is a right phrase $\alpha _{i+1}$, which is a prefix of $w(TR_{j,r_{i+1} -1})$, which is a prefix of $w(TR_{j,r_i})$, such that $w(TR_{j,r_{i+1} -1}) = \alpha _{i+1} w(TR_{j,r_{i+1}})$. {\em Proof:\/} Note that $w(TR_{r_i ,r_i}) = v$ and $TR_{r_i ,r_i}$ is adjacent to and to the left of $TR_{j,r_i}$. By Theorem~5.4, $w(TR_{r_i ,r_{i+1} -1})$ is a suffix of $v$. The $u$ in line $r_{i+1} - 1$ that is rewritten in line $r_{i+1}$ is partly in $w(TR_{r_i ,r_{i+1} -1})$ and partly in $w(TR_{j,r_{i+1} -1})$, say, $u = \beta \alpha _{i+1}$ where $\alpha _{i+1}$ is a prefix of the latter and $\beta$ is a suffix of the former, and hence a suffix of $v$. So $\beta$ is a right overlap of the system and $\alpha _{i+1}$ is a right phrase. That $w(TR_{j,r_{i+1} -1})$ is a prefix of $w(TR_{j,r_i})$ also follows from Theorem~5.4. That $w(TR_{j,r_{i+1} -1}) = \alpha_{i+1} w(TR_{j,r_{i+1}})$ is clear from the rewriting that occurs from line $r_{i+1} -1$ to line $r_{i+1}. \Box$ By Theorems~5.5 and~5.6 we get {\bf Theorem 5.7.} For each $j \geq 2$, if lines $r_1 ,r_2 , \ldots , r_p$ ($p \geq 1$) of a well behaved derivation are the lines in which traces of $TR_{j,j}$ are destroyed at the left, then there exist a string $\delta$, a left overlap $\alpha _1$ and right phrases $\alpha _2 , \ldots , \alpha _p$ such that $v = \alpha _1 \alpha _2 \cdots \alpha _p \delta$; and, for each $i$, $w(TR_{j,r_i -1}) = \alpha _i \cdots \alpha _p \delta_i$ and $w(TR_{j,r_i}) = \alpha _{i+1} \cdots \alpha _p \delta_i$, where $\delta _i$ is some prefix of $\delta$. (If no traces of $TR_{j,j}$ are destroyed from the right before line $r_i$ then $\delta _i = \delta$.) By symmetry from Theorem~5.7 we get {\bf Theorem 5.8.} For each $j \geq 2$, if lines $s_1 , \ldots ,s_q$ ($q \geq 1$) are the lines of a well behaved derivation in which traces of $TR_{j,j}$ are destroyed at the right then there exist a string $\gamma$, a right overlap $\beta _1$ and left phrases $\beta _2 , \ldots , \beta _q$ such that $\gamma \beta _q \cdots \beta _ 2 \beta _1 = v$ and, for each $i$, $w(TR_{j,s_i -1}) = \gamma _i \beta _q \cdots \beta _i$ and $w(TR_{j,s_i}) = \gamma _i \beta _q \cdots \beta _{i+1}$, where $\gamma _i$ is a suffix of $\gamma$. (If no traces of $TR_{j,j}$ are destroyed from the left before line $s_i$ then $\gamma _i = \gamma$.) {\bf Theorem 5.9 (Main Theorem).} For a system $u \rightarrow v$ and word $\eta$, there exists a well behaved derivation in which some $w(TR_{j,i}) = \eta$ if and only if there is a parsing of \[ v = \alpha _1 \alpha _2 \cdots \alpha _p \eta \beta _q \cdots \beta _2 \beta _1 \] for some $p \geq 0$ and $q \geq 0$, where (if $p \geq 1$) $\alpha _1$ is a left overlap, (if $q_1 \geq 1$) $\beta _1$ is a right overlap, (if $p \geq 2$) $\alpha _2 , \ldots , \alpha _p$ are right phrases, and (if $q \geq 2$) $\beta _2 , \ldots , \beta _q$ are left phrases. {\em Proof from left to right:\/} By Theorems~5.7 and~5.8 we get $v = \alpha _1 \cdots \alpha _p \delta$ and $v = \gamma \beta _q \cdots \beta _1$. Since both of these are applications to a single well behaved derivation, $\alpha _1 \cdots \alpha _p$ must be a prefix of $\gamma$ and $\beta _q \cdots \beta _1$ must be a suffix of $\delta$, which gives us the parsing. {\em Proof from right to left:\/} Theorem~4.6.$\Box$ {\bf Open question:} Does Theorem~5.9 remain true when the phrase ``well behaved'' is deleted? In other words, is what Theorem~5.9 says about well behaved derivations true also about ill behaved derivations? \vspace{.5in} {\bf 6. Ill behaved derivations.} This paper offers no analysis of infinite ill behaved derivations. However, this section presents an algorithm to determine whether a given one-rule semi-Thue system has any ill behaved derivation, and if so to construct a finite ill behaved derivation. {\bf Theorem 6.1.} A system $u \rightarrow v$ has an ill behaved derivation if and only if at least one of the following conditions holds: (C1) For some $p,q \geq 1$, \[ v = \alpha _1 \alpha _2 \cdots \alpha _p \eta \beta _q \cdots \beta _2 \beta _1 \] and $u = A \eta B$, where $\alpha _1$ is a left overlap, $\beta _1$ is a right overlap, $\alpha _2 , \ldots , \alpha _p$ are right phrases, $\beta _2 , \ldots , \beta _q$ are left phrases, $A$ is a right overlap and $B$ a left overlap. (None of $\alpha _1 , \ldots , \alpha _p$, $\beta _1 , \ldots , \beta _q ,A,B$ may be null, but $\eta$ may be.) (C2) For some $p \geq 1$, $v = \alpha _1 \alpha _2 \cdots \alpha _p \eta$ and $u = A \eta B$, where $\alpha _1$ is a left overlap, $\alpha _2 , \ldots , \alpha _p$ are right phrases, $A$ is a right overlap and $B$ is nonnull. (None of $\alpha _1 , \ldots , \alpha _p , A$ or $B$ may be null, but $\eta$ may be.) (C3) For some $q \geq 1$, $v = \eta \beta _q \cdots \beta _2 \beta _ 1$ and $u = A \eta B$, where $\beta _1$ is a right overlap, $\beta _2 , \ldots , \beta _q$ are left phrases, $A$ is nonnull and $B$ is a left overlap. (None of $\beta _1 , \ldots , \beta _q , A, B$ may be null, but $\eta$ may be. Note that (C3) is the right-left symmetric analog of~(C2).) {\em Proof that (C1) implies the existence of an ill behaved derivation:\/} By Theorem~4.6 there is a derivation that gives us \[ \alpha '_1 u \beta '_1 ~ \triangleright ^{p+q+1} ~v \eta v \] where $\alpha '_1$ and $\beta '_1$ are the companion left phrase to $\alpha _1$ and the companion right phrase to $\beta _1$, respectively. By examining the proofs of Theorems~4.5 and~4.6 we see that the traces in and around $\eta$ are the only traces in the last line that are traces of the $v$ introduced in the second line. Where $A''A = BB'' = v$, we get $v \eta v = A''A \eta BB''$. Since $A \eta B = u$, we have $v \eta v \rightarrow A''vB''$, and hence \[ \alpha '_1 u \beta '_1 ~ \triangleright ^{p+q+2} A''vB'' \] Clearly, this derivation of $p+q+2$ lines is ill behaved. (It is important that $A$ and $B$ both are nonnull. E.g., if $A$ were null then there would be a trace remaining to the last line, namely the trace between the $\alpha _p$ and the $\eta$ created in the second line. It is also important that both $\alpha '_1$ and $\beta '_1$ are nonnull. E.g., if $\alpha '_1$ were null then the left border trace of the second line would not be destroyed in the derivation.) \newpage {\em Proof that (C2) implies the existence of an ill behaved derivation:\/} We take $\alpha '_1$ and $A''$ so that $\alpha '_1 \alpha _1 = u$ and $A''A = v$. By Theorem~4.5 we get: \[ \alpha '_1 uB \] \[ \rightarrow \alpha '_1 \alpha _1 \alpha _2 \cdots \alpha _p \eta B \] \[ \triangleright ^p v \eta B = A''A \eta B \] \[ \rightarrow A''v \] Again, all the traces created in the second line of this derivation as well as the two border traces, are destroyed in the later lines. (This would not be true if $A$ or $B$ were null. E.g., if $B$ were null the right border trace of the second line would be still present in the last line.) The proof for (C3) is symmetric to the proof for~(C2). It remains to prove that the existence of an ill behaved derivation implies either (C1), (C2) or~(C3). Assuming an ill behaved derivation, let $n$ be the smallest integer such that, for some $j < n$, all traces of $TR_{j,j}$ are destroyed in or before line $n$. Thus the first $n$ lines of this derivation constitute an ill behaved derivation $D_n$ but the first $n - 1$ lines constitute a well behaved derivation $D_{n-1}$. There may be several such $j$, but for each one at least one trace of $TR_{j,j}$ is destroyed in line $n$. Since $|v| > |u|$, and since the last traces of $TR_{j,j}$ are destroyed in line $n$, some traces of $TR_{j,j}$ are destroyed before line $n$. Since $D_{n-1}$ is well behaved, each of the traces destroyed before line $n$ must be destroyed from the left or from the right, by Theorem~5.2. Thus all the traces destroyed in line $n$ are to the right of those destroyed from the left in earlier lines, and all are to the left of those destroyed at the right in earlier lines. Case I: There exists a $j$ such that (1)~all traces of $TR_{j,j}$ are destroyed in $D_n$, and (2)~all traces that are destroyed in $D_{n-1}$ are destroyed from the left. Assume that $j$ is maximal with these two properties. By Theorem~5.7 we get $v = \alpha _1 \alpha _2 \cdots \alpha _p \delta$, where $p \geq 1$, $w(TR_{j,n-1}) = \delta$, $\alpha _1$ is a left overlap and $\alpha _2, \ldots , \alpha _p$ are right phrases. We are on our way to demonstrating that Condition~(C2) holds. Since $TR_{j,n} = \emptyset$, it follows that the occurrence of $u$ in line $n-1$ that is rewritten in line $n$ has the noted occurrence of $\delta$ as a factor, but not as prefix or suffix: for if it were prefix or suffix there would still be a trace of $TR_{j,j}$ remaining in the $n^{th}$ line. (E.g., if this $u$ had $\delta$ as prefix, then the leftmost trace of the $u$ would be a trace of $TR_{j,j}$ that is not destroyed in line~$n$.) Thus $u = A \delta B$ is a factor of the $(n-1)^{st}$ line, where this occurrence of $\delta$ coincides with the locus of $TR_{j,n-1}$ and neither $A$ nor $B$ is null. What remains to be proved for (C2) is that $A$ is a suffix of $v$, which will imply that it is a right overlap. Let $j'$ be the last line before line $n$ where some traces of $TR_{j,j}$ are destroyed from the left. We have $L(j',j,j')$. Since no traces of $TR_{j,j'}$ are destroyed from the left in lines $j' + 1$ through $n-1$, no traces of $TR_{j',j'}$ can be destroyed from the right in those lines, by Theorem~5.4. Therefore, $j'$ has property~(2). Furthermore, $L(j',j,n-1)$ holds, and the word $w(TR_{j',n-1})$ is a suffix of $v$. Now if $j'$ also has property~(1), i.e., that all traces of $TR_{j',j'}$ are destroyed in $D_n$, it would violate the stipulation that $j$ is maximal with properties~(1) and~(2). It follows that $TR_{j',n} \neq \emptyset$, from which we can conclude that the noted occurrence of $A$ (i.e., the prefix of the noted $u$ in line $n-1$) must be a suffix of $w(TR_{j',n-1})$, hence a suffix of $v$, and hence a right overlap. Case II: There exists a $j$ such that all traces of $TR_{j,j}$ are destroyed in $D_n$, but all that are destroyed in $D_{n-1}$ are destroyed from the right. Then Condition~(C3) holds; the proof is symmetrical to the proof for Case~I. Case III: For every $j$ such that all the traces of $TR_{j,j}$ are destroyed in $D_n$, some are destroyed from the left, and some from the right, in $D_{n-1}$. Select any such $j$. By Theorem~5.9, $v = \alpha _1 \alpha _2 \cdots \alpha _p \eta \beta _q \cdots \beta _2 \beta _1$, where $p,q \geq 1$, and $w(TR_{j,n-1}) = \eta$. Furthermore, $\alpha _1$ is a left overlap, $\beta _1$ is a right overlap, $\alpha _2 , \ldots , \alpha _p$ are right phrases, $\beta _2 , \ldots , \beta _q$ are left phrases, and $u = A \eta B$ is a factor of the $(n-1)^{st}$ line, where the locus of the $\eta$ is $TR_{j,n-1}$. In order to complete the proof we must prove that $A$ and $B$ are, respectively, suffix and prefix of $v$. Reminiscent of the last part of the proof in Case~I, let $j'$ be the last line before line~$n$ where some traces of $TR_{j,j}$ are destroyed from the left. By Theorem~5.4 and the fact that $L(j',j,j')$, no traces of $TR_{j',j'}$ are destroyed from the right in lines~$j'+1$ through~$n-1$. If all traces in $TR_{j',j'}$ are destroyed in $D_n$ there would be a violation of the definition of Case~III. It follows that $A$ is a suffix of $w(TR_{j',n-1})$ and, hence, of $v$. By symmetry, $B$ is a prefix of $v$.$\Box$ {\bf Corollary.} It is decidable whether a given one-rule semi-Thue system has an ill behaved derivation. {\em Proof:\/} The algorithm constructs all the left and right overlaps and all the left and right phrases; it then parses $v$ in all possible ways as $\alpha _1 \cdots \alpha _p \eta \beta _q \cdots \beta _1$ ($p,q \geq 1$), where $\alpha _1$ is a left overlap, $\beta _1$ is a right overlap, $\alpha _2 , \ldots , \alpha _p$ are right phrases and $\beta _2 , \ldots , \beta _q$ are left phrases. For each such parsing it determines whether or not $A$ and $B$ exist satisfying the remaining conditions of (C1). The conditions (C2) and (C3) are tested similarly. The system has an ill behaved derivation if and only if it satisfies at least one of these conditions.$\Box$ {\bf Example 1.} The system $c^m b^n \rightarrow b^h c^k$ (studied in \cite{zg}) where $h > n > 0$ and $k > m > 0$, has an ill behaved derivation. The left overlaps for this system are $b, b^2 ,\ldots , b^n$ with respective companion left phrases $c^mb^{n-1}, c^m b^{n-2}, \ldots , c^m$. The right overlaps are $c, \ldots , c^m$ with companion right phrases $c^{m-1} b^n , \ldots , b^n$. The condition~(C1) is satisfied: Let $h = q_1 n + r_1$, $1 \leq r_1 \leq n$, and $k = q_2 m + r_2$, $1 \leq r_2 \leq m$. Take $\alpha _1 = b^{r_1}$, $\alpha _2 = \alpha _3 = \cdots = \alpha _{q_1 +1} = b^n$, $\beta _1 = c^{r_2}$, $\beta _2 = \cdots = \beta_{q_2 +1} = c^m$, $\eta = \lambda$, $A = c^m$, $B = b^n$. To see the ill behaved derivation based on this, note first that $c^m b^{(q_1 +1)n} \rightarrow ^{q_1 + 1} xc^m$ for a certain string $x$, and, in the derivation, all internal traces of the original line are destroyed. Also, for a certain string $y$, $c^{(q_2+1)m}b^n \rightarrow ^{q_2 +1} b^n y$, where the derivation has the same property. The ill behaved derivation of $q_1 + q_2 + 5$ lines is then \[ c^m b^{n-r_1} uc^{m-r_2}b^n \] \[ \rightarrow c^m b^{n-r_1}vc^{m-r_2}b^n = c^m b^{(q_1 +1)n} c^{(q_2 +1)m} b^n \] \[ \rightarrow ^{q_1 + q_2 + 2} xc^m b^n y \] \[ \rightarrow xvy \] Note that all traces of $TR_{2,2}$ (the traces of the apparent $v$ of line~2) are destroyed in the derivation, the last trace being destroyed in the last line. {\bf Theorem 6.2.} There exist one-rule semi-Thue systems that have ill behaved derivations but no infinite derivations. {\em Proof:\/} The system $ccbb \rightarrow bbbccc$ shown to be uniformly terminating in \cite{zg} has a finite ill behaved derivation, as we have just demonstrated.$\Box$ {\bf Open question.} Does there exist a one-rule semi-Thue system with an infinite well behaved derivation and a finite ill behaved derivation but no infinite ill behaved derivation? {\bf Example 2.} The system $abcd \rightarrow cdcdbabab$ has no ill behaved derivation, which is interesting because: (1)~It has an infinite well behaved derivation, taken from the loop $ababcd \triangleright ^2 ababcd$. (2)~It has no inhibitor (although one could say, speaking loosely, that the leftmost occurrence of $b$ on the right side acts like an inhibitor.) This system has only one left overlap, $cd$, with companion left phrase $ab$, and only one right overlap $ab$ with companion right phrase $cd$. If we attempt to set up (C1), the only way to begin is to take $p=1$ or $2$ and $q = 1$ or $2$, with $\alpha _1 = \alpha _2 = cd$ and $\beta _1 = \beta _2 = ab$. With $p = q = 2$ we must have $\eta = b$, and we can find no right overlap $A$ and left overlap $B$ such that $AbB = abcd$. With $p = 1$ or $q = 1$ we get an $\eta$ that is not a factor of $abcd$. We conclude that (C1) does not hold. Condition~(C2) fails because if $v = \alpha _1 \alpha _2 \cdots \alpha _p \eta$ with $\alpha _1$ a left overlap and $\alpha _2 , \ldots , \alpha _p$ right phrases then, as we have noted, $p \leq 2$ and $\eta$ is too long to be a factor of $u$. Similarly, (C3) does not hold. \vspace{.5in} {\bf 7. Further derivation analysis.} The next major result of this paper is an efficient algorithm, formulated and justified in the next section, to determine whether a given system $u \rightarrow v$ has an infinite well behaved derivation. This section continues the analysis of derivations from Sections~3 and~5, thereby providing a basis for the proof that justifies that algorithm. The Main Theorem converts an infinite well behaved derivation into a convenient infinite sequence of words. {\bf Definition:} A {\em proper derivation\/} is one in which all traces present in the first line are eventually destroyed except for the traces at the left and right ends of the line. Note that from an infinite derivation one easily obtains an infinite proper derivation: For if $x_1 x_2 \cdots x_p$ is the first line and \[(x_1 ,x_2 \cdots x_p ),~(x_1 x_2 ,x_3 \cdots x_p ) , \ldots , (x_1 \cdots x_{p-1},x_p ) \] are all the internal positions whose traces are not destroyed in the derivation, then for at least one $i$, $1 \leq i \leq p$, there exists a proper infinite derivation whose first line is $x_i$. If the original derivation is well behaved then the latter is also well behaved. {\bf Definition.} The {\em critical line\/} in an infinite derivation is the last line in which some trace of the first line is destroyed. Since only finitely many traces are present in the first line, the critical line always exists. {\bf Definitions (${\bf S_{i+1} ,J_i ,L(j,j',i)}$).} $S_{i+1} =$ the set of traces of line~$i$ destroyed in line~$i+1$. $J_i = \{ j|TR_{j,i} \cap S_{i+1} \neq \emptyset \}$. We write $L(j,j',i)$ to mean that, in line $i$ of a derivation, every trace of $TR_{j,i}$ is to the left of every trace of $TR_{j',i}$, except for the trace they have in common (if any). (The definition of $S_{i+1}$ is repeated from Section~3. The concept $J_i$ was used without a formal definition in Theorem~5.1. The definition of $L(j,j',i)$ is repeated from Section~5.) {\bf Definition (adjacent).} The sets $TR_{j,i}$ and $TR_{j',i}$ are {\em adjacent\/} in line $i$ if there is no trace present in line $i$ that is properly between the two. {\bf Theorem 7.1.} If the $(i+1)^{st}$ line of a well behaved derivation is a postcritical line then $|J_i | = 2$. For $J_i = \{ j,j' \}$, $TR_{j,i}$ and $TR_{j',i}$ are adjacent in line $i$. {\em Proof:\/} By Theorem~5.1, $|J_i | \leq 2$. Since the $(i+1)^{st}$ line is postcritical, every trace destroyed in line~$i+1$ is in some $TR_{j,i}$; hence $|J_i | \neq 0$. But the set $J_i$ cannot have only one member $j$; for this would imply that $u$ is a factor of $w(TR_{j,i})$ and thus a factor of $v$. Hence, $|J_i | = 2$. For $J_i = \{ j,j' \}$ if $TR_{j,i}$ and $TR_{j',i}$ were not adjacent there would be a trace properly between the two sets and destroyed in line~$i + 1$. This trace would have to be either a trace of the first line of the derivation or a trace of some $TR_{j'',i}$ for $j \neq j'' \neq j'$. Both are impossible since line~$i$ is a postcritical line and $|J_i | = 2. \Box$ {\bf Definition (${\bf LOR(i)}$ and ${\bf ROR(i)}$).} If the $i^{th}$ line of a well behaved derivation is a postcritical line, $J_i = \{ j,j' \}$ and $L(j,j',i-1)$, then we let $j = LOR(i)$ and $j' = ROR(i)$ (left origin and right origin). Note that, since the $i^{th}$ line is post-critical and the derivation is well behaved, $TR_{j,i-1}$ and $TR_{j',i-1}$ are adjacent in line $i-1$. Note also that $LOR(i), ROR(i) < i$. \newpage {\bf Theorem 7.2.} If line $i$ is a postcritical line in a well behaved derivation, $j = LOR(i)$ and $j' = ROR(i)$ then the traces of $TR_{j,i-1}$ ($TR_{j',i-1}$) destroyed in line $i$ are destroyed from the right (left). Thus $TR_{i,i}$ is between $TR_{j,i}$ and $TR_{j',i}$. For $m = max(j,j')$, no traces of $TR_{j,m}$ ($TR_{j',m}$) are destroyed from the right (left) in lines $m+1$ through $i-1$. {\em Proof:\/} The first sentence follows from the facts that $J_{i-1} = \{ j,j' \}$ and that $S_i$ is consecutive. The second sentence follows from the first. Now suppose that the third sentence is false; say, for $m+1 \leq s \leq i-1$, either some traces of $TR_{j,s-1}$ are destroyed from the right or some traces of $TR_{j',s-1}$ are destroyed from the left in line $s$. Then, by Theorem~5.3, both of these are true and $TR_{s,s}$ is created between $TR_{j,s}$ and $TR_{j',s}$. Since the derivation is well behaved, $TR_{s,i-1}$ would be between $TR_{j,i-1}$ and $TR_{j',s-1}$, which is impossible since $S_i$ is consecutive and $|J_{i-1} | = 2. \Box$ {\bf Theorem 7.3.} Assume the hypothesis of Theorem~7.2 and put $m = max(j,j')$. Then there are words $x'$ and $y'$ such that $w(TR_{j,m})w(TR_{j',m}) = x'uy'$, $x'$ is a proper prefix of $w(TR_{j,m})$, $y'$ is a proper suffix of $w(TR_{j',m})$, $w(TR_{j,i})$ is a suffix of $x'$ and $w(TR_{j',i})$ is a prefix of $y'$. {\em Proof:\/} No traces of $TR_{j,m}$ are destroyed from the right and no traces of $TR_{j',m}$ are destroyed from the left in lines $m+1$ through $i-1$. Thus $w(TR_{j,i-1})$ is a suffix of $w(TR_{j,m})$ and $w(TR_{j',i-1})$ is a prefix of $w(TR_{j',m})$; say, $\alpha w(TR_{j,i-1}) = w(TR_{j,m})$ and $w(TR_{j',i-1}) \beta = w(TR_{j',m})$. The $u$ in line $i-1$ that is rewritten to become $w(TR_{i,i}) = v$ in line $i$ overlaps both the $w(TR_{j,i-1})$ and the $w(TR_{j',i-1})$. Accordingly, let $u = u_1 u_2$ where $u_1 \neq \lambda \neq u_2$, $u_1$ is a suffix of $w(TR_{j,i-1})$ and $u_2$ a prefix of $w(TR_{j',i-1})$. Note that $w(TR_{j,i}) u_1 = w(TR_{j,i-1})$ and $u_2 w(TR_{j',i}) = w(TR_{j',i-1})$. Put $x' = \alpha w(TR_{j,i})$ and $y' = w(TR_{j',i}) \beta$. Then \[ x'u_1 = \alpha w(TR_{j,i})u_1 = \alpha w(TR_{j,i-1}) = w(TR_{j,m}) \] Likewise, \[ u_2 y' = u_2 w(TR_{j',i}) \beta = w(TR_{j',i-1}) \beta =w(TR_{j',m}) \] We thus get \[ w(TR_{j,m}) w(TR_{j',m}) = x'u_1 u_2 y' = x'uy' \] and our theorem is proved. (The figure is helpful for understanding this proof, although it does not show $\alpha$ and $\beta$.)$\Box$ \begin{figure} \begin{center} \begin{tabbing} xxxxxxxxxxxxxxxxx \= line $i-1~$: \= $= \cdots w(TR_{j,i-1} ~~$ \= $u$ \kill \> line $m$: \> \> $\cdots w(TR_{j,m})$ \' $w(TR_{j',m}) \cdots $ \\ \> \> \> $= \cdots x'u_1$ \' $u_2 y' \cdots $ \\ \> \> \> $ \vdots $ \\ \> line $i-1$: \> \> $\cdots w(TR_{j,i-1})$ \' $w(TR_{j',i-1}) \cdots$ \\ \> \> \> $= \cdots w(TR_{j,i})u_1$ \' $u_2 w(TR_{j',i}) \cdots$ \\ \> line $i$: \> \> $ \cdots w(TR_{j,i})~~~$ \' $v~~w(TR_{j',i}) \cdots$ \end{tabbing} \end{center} \centerline{Figure: Illustration of Theorem 7.3} \end{figure} {\bf Definition (LC successor and RC successor).} Assume that, for a given parsed word $x_1 y_1$, there exist a proper prefix $x'_1$ of $x_1$ and a proper suffix $y'_1$ of $y_1$ such that $x_1y_1 = x'_1 uy'_1$. The parsed word $x_2 y_2$ is an {\em LC successor (left child)\/} of $x_1 y_1$ if $x_2$ is a suffix (not necessarily proper) of $x'_1$ and $y_2 = v$. It is an {\em RC successor (right child)\/} of $x_1 y_1$ if $x_2 = v$ and $y_2$ is a prefix (not necessarily proper) of $y'_1$. (The appropriateness of the graph-theoretic terms ``left child'' and ``right child'' will become clear in the proof of Theorem~7.4.) {\bf Definition.} An {\em $xy$-sequence\/} in a system $u \rightarrow v$ is an infinite sequence of parsed words $x_1 y_1 ,x_2 y_2 ,x_3 y_3 , \ldots$ such that (1),~for all $n \geq 1$, $x_{n+1}y_{n+1}$ is either an LC successor or an RC successor of $x_n y_n$, and (2)~either $x_1$ is a factor of $v$ and $y_1 = v$ or else $x_1 = v$ and $y_1$ is a factor of $v$. (Note that, in an $xy$-sequence, condition~(2) is true of $x_n y_n$ for all $n \geq 1$.) {\bf Theorem 7.4 (Main Theorem).} If the system $u \rightarrow v$ has an infinite well behaved derivation then it has an $xy$-sequence. {\em Proof:\/} If there is an infinite well behaved derivation then there is a proper infinite well behaved derivation. Let line~$i_0$ be the critical line of the latter. From this proper derivation we define relations on some ordered pairs of positive integers. We take \[ N = \{ (j,j')| L(j,j',max(j,j')) \mbox{ and } |TR_{j,max(j,j')} \cap TR_{j',max(j,j')}| = 1 \} \] If $j = LOR(i)$, $j' = ROR(i)$ and $(j,j') \in N$ (which imply that $(j,i),(i,j') \in N$) then we say that $(j,i)$ and $(i,j')$ are {\em children\/} of $(j,j')$. Let the {\em descendent\/} relation be the transitive closure of the child relation. We think of $N$ as the set of nodes of a graph where each child is connected by an edge to its parent. It is convenient to think of the graph as laid out so that, for $j = LOR(i)$ and $j' = ROR(i)$, the node $(j,i)$ is to the left of the node $(i,j')$, and the node $(j,j')$ is above both. The graph will be a forest of rooted trees with infinitely many nodes. Before we can apply Theorem~1.1, we must prove that there are only finitely many rooted trees, which we do as the last in a sequence of lemmas: {\bf Lemma 1.\/} If $i > i_0$ then $(LOR(i),i),~(i,ROR(i)),~(LOR(i),ROR(i)) \in N$. {\em Proof:\/} By Theorem~7.1, $|J_i | = 2$, say $J_i = \{ j,j' \}$ where $L(j,j',i-1)$. By definition, $j = LOR(i)$ and $j' = ROR(i)$. By the manner in which $TR_{i,i}$ is obtained from $TR_{j,i-1}$ and $TR_{j',i-1}$, we have $(j,i)$ and $(i,j') \in N$. It remains to prove that $(j,j') \in N$. Since $L(j,j',i-1)$, we have $L(j,j',m)$, where $m = max(j,j')$. So we need prove only that $|TR_{j,m} \cap TR_{j',m} | = 1$. We note first that there is no $h$ such that $L(j,h,m)$ and $L(h,j',m)$. For if there were, since the derivation is well behaved, we would have $L(j,h,i-1)$ and $L(h,j',i-1)$. Since some traces of $TR_{j,i-1}$ and some of $TR_{j',i-1}$ are destroyed in line~$i$, all the traces of $TR_{h,i-1}$ would be destroyed in line~$i$. This is impossible in a well behaved derivation. Thus $TR_{j,m}$ and $TR_{j',m}$ are adjacent in line $m$, and hence, by Theorem~3.9, $|TR_{j,m} \cap TR_{j',m} | = 1.\Box$ {\bf Lemma 2.} If $(j,i)$ and $(i,j') \in N$ and $i > j,j'$, then $j = LOR(i)$ and $j' = ROR(i)$. {\em Proof:\/} Since $(j,i) \in N$ and $i > j$, $TR_{j,i}$ and $TR_{i,i}$ have a trace in common, which is at the right end of $TR_{j,i}$ and the left end of $TR_{i,i}$. The set $TR_{i,i}$ is created in line $i$ partly from some traces at the right end of $TR_{j,i-1}$. Similarly, since $(i,j') \in N$ and $i > j'$, $TR_{i,i}$ is created partly from traces of the left end of $TR_{j',i-1}$. Thus $j = LOR(i)$ and $j' = ROR(i)$ by definition.$\Box$ {\bf Lemma 3.} If $i > i_0$, $i > j$ and $(j,i) \in N$ then $(j,i)$ is not a root node of $N$. {\em Proof:\/} By Lemma~1, $(LOR(i),i),~(i,ROR(i)),~(LOR(i),ROR(i)) \in N$. By Lemma~2, $j = LOR(i)$. Taking $j' = ROR(i)$, $(j,i)$ is a left child of $(j,j') \in N. \Box$ Similarly, we have {\bf Lemma 4.} If $i > i_0$, $i > j'$ and $(i,j') \in N$ then $(i,j')$ is not a root of $N$. {\bf Lemma 5.} The forest whose node set is $N$ has only finitely many root nodes, and hence only finitely many trees. {\em Proof:\/} By Lemmas~3 and~4, if $(h,k)$ is a root node of $N$ then $max(h,k) \leq i_0$. Only finitely many nodes of $N$ have this property.$\Box$ We now apply Theorem~1.1, getting an infinite sequence $(h_1 ,k_1), (h_2 ,k_2), \ldots ~$ such that, for each $n$, $(h_{n+1},k_{n+1})$ is a child of $(h_n ,k_n )$: thus, for each $n$, either $h_{n+1} = h_n$ and $k_{n+1}$ is new (in which case we say that $(h_{n+1} ,k_{n+1})$ is the {\em left child\/} of $(h_k ,k_n)$ ) or $h_{n+1}$ is new and $k_{n+1} = k_n$ ( $(h_{n+1},k_{n+1})$ is the {\em right child\/} of $(h_n ,k_n)$ ). For each $n$, put $m = m(n) = max(h_n ,k_n )$, $x_n = w(TR_{h_n ,m})$ and $y_n = w(TR_{k_n ,m})$. Note that if $(h_{n+1} ,k_{n+1})$ is a left child of $(h_n ,k_n)$ then $x_{n+1}$ is a proper factor of $v$ and $y_{n+1} = v$; and if it is a right child then $x_{n+1} = v$ and $y_{n+1}$ is a proper factor of $v$. Our theorem is proved by proving that $x_1 y_1 ,x_2 y_2 , \ldots$ is an $xy$-sequence. We prove first that Condition~(2) of the definition is satisfied, i.e., that either $x_1$ is a factor of $v$ and $y_1 = v$ or else $x_1 = v$ and $y_1$ is a factor of $v$. Case I: $(h_2 ,k_2 )$ is a left child of $(h_1 ,k_1)$ and $h_1 < k_1$. Then the hypotheses of Theorems~7.2 and~7.3 are satisfied with $j = h_1 = h_2$, $m = j' = k_1$ and $i = k_2$. We get $x_1 = w(TR_{j,j'})$ and $y_1 = w(TR_{j',j'} ) = v$; by Theorem~3.4, Condition~(2) is verified. Case II: $(h_2 ,k_2 )$ is a right child of $(h_1 ,k_1 )$ and $h_1 > k_1$. Here we must take $m = j = h_1$, $j' = k_1 = k_2$ and $i = h_2$ for Theorems~7.2 and~7.3. We get $x_1 = w(TR_{j,j}) = v$ and $y_1 = w(TR_{j',j})$, again verifying Condition~(2). Case III (left child, $h_1 > k_1$) and Case~IV (right child, $h_1 < k_1$) are similar. The proof is concluded by verifying Condition~(1) of the definition, i.e., for all $n \geq 1$, $x_{n+1} y_{n+1}$ is either an LC successor or an RC successor of $x_n y_n$. Case I: $(h_{n+1},k_{n+1})$ is a left child of $(h_n ,k_n )$. Then $h_{n+1} = h_n$ and $k_{n+1} > m \geq h_n = h_{n+1}$. Applying Theorem~7.3 (note also the figure), taking $j=h_n$, $j' = k_n$, $i = k_{n+1}$ , we obtain $x'$ and $y'$ satisfying the consequent of Theorem~7.3, which we rename as $x'_n$ and $y'_n$. (Note that $m = m(n)$ as defined above is consistent with its use in Theorem~7.3.) Thus $x'_n$ is a proper prefix of $x_n = w(TR_{h_n ,m})$ and $y'_n$ is a proper suffix of $y_n = w(TR_{k_n ,m})$ such that $x_n y_n = x'_n uy'_n$. Furthermore, $x_{n+1}$ is a suffix of $x'_n$ and $y_{n+1} = w(TR_{k_{n+1} ,k_{n+1}}) = v$. Thus $x_{n+1} y_{n+1}$ is an LC successor of $x_n y_n$. Case II: $(h_{n+1},k_{n+1})$ is a right child of $(h_n ,k_n )$. The proof that $x_{n+1} y_{n+1}$ is an RC successor of $x_n y_n$ is similar to the proof in the left-child case.$\Box$ \vspace{.5in} {\bf 8. Infinite well behaved derivations.} This section contains an efficient algorithm for the problem: does a given one-rule semi-Thue system have an infinite well behaved derivation? The algorithm of Section~2 (Theorem~2.3), which can be applied to semi-Thue systems with any finite set of rules, is inefficient even when it is applied to one-rule systems. {\bf Definition (LR trail, RL trail, length, trail cycle).} Where $\alpha _1$ is a left overlap and $\beta _1$ is a right overlap of a system $u \rightarrow v$, there is an {\em LR trail\/} from $\alpha _1$ to $\beta _1$ if $v = \alpha _1 \alpha _2 \cdots \alpha _h z$, $h \geq 2$, $\alpha _i$ is a right phrase for $2 \leq i \leq h$, and $u = \beta _1 \alpha _h$. There is an {\em RL~trail\/} from $\beta _1$ to $\alpha _1$ if $v = z' \beta _k \cdots \beta _ 2 \beta _1$, $k \geq 2$, $\beta _ i$ is a left phrase for $2 \leq i \leq k$, and $u = \beta _ k \alpha _1$. The {\em lengths\/} of these two trails are $h - 1$ and $k - 1$, respectively. A {\em trail cycle\/} is a sequence \[ \alpha _1 , \beta _1 , \alpha _2 , \beta _2 , \ldots , \alpha _n , \beta _n \] where $n \geq 1$, each $\alpha _i$ is a left overlap, each $\beta _i$ is a right overlap, there is an LR~trail from $\alpha _i$ to $\beta _i$, for $1 \leq i \leq n$, an RL~trail from $\beta _i$ to $\alpha _{i+1}$ for $i \leq n - 1$ and an RL~trail from $\beta _n$ to $\alpha _1$. The objective is achieved by proving that a one-rule semi-Thue system has an infinite well behaved derivation if and only if it has a trail cycle. The trail-cycle condition is a generalization of a condition of Kurth \cite{ku1}, who proved that a one-rule semi-Thue system has a loop of length~$2$ if and only if $v = \alpha _1 \alpha _2 z = z' \beta _2 \beta _1$, where $u = \beta _1 \alpha _2 = \beta _2 \alpha _1$. Note that this last condition implies that $\alpha _1$ is a left overlap, $\beta _1$ is a right overlap, there is an LR~trail of length $1$ from $\alpha _1$ to $\beta _1$, and there is an RL~trail of length~$1$ from $\beta _1$ to $\alpha _1$; in other words, that $\alpha _1 , \beta _1$ is a trail cycle (where $n = 1$). The infinite derivation is based on the following loop of length $2$: \[ \beta _2 \underline{u} \rightarrow \underline{\beta _2 \overline{\alpha _ 1}} \overline{\alpha _2 z} \rightarrow \overline{z' \beta _2 \beta_1} \alpha _2 z = z' \beta _2 uz \] {\bf Theorem 8.1.} If a system $u \rightarrow v$ has a trail cycle, then its inhibition system has an infinite derivation. {\em Proof:\/} Assuming the existence of the trail cycle we take, for each $i$, \[ v = \alpha _{i,1} \alpha _{i,2} \cdots \alpha _{i,h_i} z_i = z'_i \beta _{i,k_i} \cdots \beta _{i,2} \beta _{i,1} \] where, for $j \geq 2$, the $\alpha _{i,j}$'s are right phrases, the $\beta_{i,j}$'s are left phrases and \[ u = \beta _{i,1} \alpha _{i,h_i} = \beta _{i,k_i} \alpha _{i+1,1} \] (The $i$ here and below is taken $\bmod n$: if $i = n$ then $i+1 = 1$; and if $i = 1$ then $i-1 = n$.) The infinite derivation that will be constructed in the inhibition system (see Section~2) will use two rules $u \rightarrow \iota v$ and $u \rightarrow v \iota$. The symbols $\triangleright$, $\rightarrow$, etc., as used in the remainder of this proof refer to the inhibition system. The following lemmas use ideas similar to Theorems~4.5 and~4.6. {\bf Lemma 1.} $\beta _{i-1,k_{i-1}} v~ \triangleright ^{h_i -1} v \alpha _{i,h_i}$. {\em Proof:\/} \[ \beta _{i-1,k_{i-1}} v = \underline{\beta _{i-1,k_{i-1}} \alpha _{i,1}} \alpha _{i,2} \alpha _{i,3} \cdots \alpha _{i,h_i} z_i \] \[ \rightarrow \overline{\iota v} \alpha _{i,2} \alpha _{i,3} \cdots \alpha _{i,h_i} z_i = \cdots \underline{u} \alpha _{i,3} \cdots \alpha _{i,h_i} z_i \] (since the companion right overlap to the right phrase $\alpha _{i,2}$ is a suffix of $v$) \[ \rightarrow \cdots \overline{\iota v} \alpha _{i,3} \cdots \alpha _{i,h_i} z_i \] \[ \rightarrow ^{h_i -3} \cdots \iota v \alpha _{i,h_i} z_i \Box \] {\bf Lemma 2.} $v \alpha _{i,h_i} ~ \triangleright ^{k_i-1} \beta _{i,k_i} v$. The proof is similar to that of Lemma~1.$\Box$ From Lemmas~1 and~2 we get $\beta _{i-1,k_{i-1}} v ~ \triangleright ^{h_i + k_i -2} \beta _{i,k_i} v$, for $1 \leq i \leq n$. From this we get \[ \beta _{1,k_1} v ~ \triangleright ^L \beta _{1,k_1} v \] where $L = \sum_{i=1}^{n} (h_i + k_i - 2)$. In other words, there is a loop whose length is the sum of the lengths of all $2n$ trails. Hence the inhibition system has an infinite derivation.$\Box$ Theorem~7.4 tells us that if the system $u \rightarrow v$ has an infinite well behaved derivation then it has an $xy$-sequence. The proof of Theorem~8.4, which is approximately the converse of Theorem~8.1, will involve working from this sequence. It is convenient to prove first that we can get trails from certain parts of it, which will be done in Theorem~8.3. {\bf Theorem 8.2.} Suppose in an $xy$-sequence that $x_{p+1} = x'_{p+1} \beta$ and $y_{p+1} = \alpha y'_{p+1}$ where $\beta \alpha = u$, $\alpha \neq \lambda \neq \beta$. Then $x_{p+1} y_{p+1}$ is an LC (RC) successor of $x_p y_p$ implies that $\alpha$ is a left overlap ($\beta$ is a right overlap) of the system. (Note that Theorem~8.2 applies to the $x'_{p+1}$ and $y'_{p+1}$ of the definition of left and right successor as it is used to determine $x_{p+2} y_{p+2}$ from $x_{p+1} y_{p+1}$, whether $x_{p+2} y_{p+2}$ is a left successor or right successor.) {\em Proof:\/} If $x_{p+1} y_{p+1}$ is an LC successor then $y_{p+1} = v$ and so $\alpha$ is a nonnull prefix of $v$. Since $|\alpha | < |u| < |v|$, $\alpha$ is a proper prefix. It is also clear that $\alpha$ is a nonnull proper suffix of $u$. Hence $\alpha$ is a left overlap. If $x_{p+1} y_{p+1}$ is an RC successor then, similarly, $\beta$ is a right overlap.$\Box$ {\bf Definition (critical overlaps).} In an $xy$-sequence the word $\alpha$ is a {\em critical left overlap\/} for $p+1 \geq 2$ if $x_{p+2} y_{p+2}$ is an RC successor of $x_{p+1} y_{p+1}$ which is an LC successor of $x_p y_p$ and $y_{p+1} = \alpha y'_{p+1}$, as in the definition of RC successor. The word $\beta$ is a {\em critical right overlap\/} for $p+1$ if $x_{p+2} y_{p+2}$ is an LC successor of $x_{p+1} y_{p+1}$ which is an RC successor of $x_p y_p$ and $x_{p+1} = x'_{p+1} \beta$, as in the definition of LC successor. (Cf. Theorem~8.2). {\bf Theorem 8.3.} In an $xy$-sequence let $p \geq 1$ and $h \geq 1$, and suppose the following all hold: (1)~$x_{p+1} y_{p+1}$ is an LC (RC) successor of $x_p y_p$, (2)~$x_{p+i+1} y_{p+i+1}$ is an RC (LC) successor of $x_{p+i} y_{p+i}$ for $1 \leq i \leq h$, (3)~$x_{p+h+2} y_{p+h+2}$ is an LC (RC) successor of $x_{p+h+1} y_{p+h+1}$, (4)~$\alpha$ is the critical left (right) overlap for $p+1$ and (5)~ $\beta$ is the critical right (left) overlap for $p+h+1$. Then there is an LR~trail (an RL~trail) from $\alpha$ to $\beta$. {\em Proof:\/} Assume first the hypothesis of our theorem ignoring the words in parentheses. We must prove that there is an LR~trail from the left overlap $\alpha$ to the right overlap $\beta$. By Theorem~8.2, $v = y_{p+1} = \alpha y'_{p+1}$. Since $x_{p+2} y_{p+2}$ is an RC successor, $y_{p+2}$ is a prefix of $y'_{p+1}$. Thus there is a $z_1$ such that \[ (1)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ v = \alpha y_{p+2} z_1 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \] Case I: $h > 1$. The word $x_{p+3} y_{p+3}$ is an RC successor of $x_{p+2} y_{p+2}$. But now $y_{p+2}$ is a proper factor of $v$ and $x_{p+2} = v$. We have $x_{p+2} y_{p+2} = x'_{p+2} uy'_{p+2}$, $x'_{p+2}$ is a proper prefix of $x_{p+2}$, $y'_{p+2}$ is a proper suffix of $y_{p+2}$, and $y_{p+3}$ is a prefix of $y'_{p+2}$. Again there is a $z_2$ and a nonnull suffix $\alpha _2$ of $u$ such that \[ (2)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ y_{p+2} = \alpha _2 y_{p+3} z_2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \] Taking $u = \beta _2 \alpha _2$ (so that $v = x_{p+2} = x'_{p+2} \beta _2$) we find that $\beta _2$ is a right overlap and therefore $\alpha _2$ is a right phrase. From the above two paragraphs we get \[ (3)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ v = \alpha \alpha _2 y_{p+3} z_2 z_1 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \] where $\alpha$ is a left overlap and $\alpha_2$ is a right phrase. Since each of $y_{p+4} , \ldots , y_{p+h+1}$ is obtained from its predecessor in the same way that $y_{p+3}$ is obtained from $y_{p+2}$, we get (corresponding to (2)) \[ y_{p+3} = \alpha _3 y_{p+4} z_3 ,~~ y_{p+4} = \alpha _4 y_{p+5} z_4 ,~ \ldots ,~ y_{p+h} = \alpha _h y_{p+h+1} z_h \] where all these $\alpha _i$'s are also right phrases. We can combine these with (3) to get \[ (4)~~~~~~~~~~~~~~~~~~~~ v = \alpha \alpha _2 \cdots \alpha _h y_{p+h+1} z_h \cdots z_1 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \] We now go through the next step part way. We get $x_{p+h+1} y_{p+h+1} = x'_{p+h+1} uy'_{p+h+1}$ and $v = x_{p+h+1} = x'_{p+h+1} \beta$, where $\beta$ is the critical right overlap for $p+h+1$ as given by the hypothesis of our theorem. Furthermore, $y_{p+h+1} = \alpha _{h+1} y'_{p+h+1}$ and $\beta \alpha _{h+1} = u$, for some $\alpha _{h+1} \neq \lambda$. Replacing $y_{p+h+1}$ in (4) we get \[ (5)~~~~~~~~~~~~~~~~~~~~~~ v = \alpha \alpha _2 \cdots \alpha _{h+1} y'_{p+h+1} z_h \cdots z_1 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \] Since $\alpha _{h+1}$ is the companion right phrase to the right overlap $\beta$, we have completed our demonstration that there is an LR~trail from $\alpha$ to $\beta$. Case II: h = 1. The proof is like that of Case~II except that we go directly from (1) to (5), which becomes \[ (5')~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ v = \alpha \alpha _2 y'_{p+2} z_1 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \] As above, $\alpha _2$ is the companion right phrase to the right overlap $\beta$, and there is an LR~trail from $\alpha$ to $\beta$. This concludes the proof of Theorem~8.3 ignoring the terms in parentheses. The proof for the statement using the parenthesized terms is similar to the above.$\Box$ {\bf Theorem 8.4.} If the system $u \rightarrow v$ has an infinite well behaved derivation then it has a trail cycle. {\em Proof:\/} Assuming the hypothesis, Theorem~7.4 tells us that the system $u \rightarrow v$ has an $xy$-sequence. We note that in any such sequence, if $x_{n+1} y_{n+1}$ is an LC successor of $x_n y_n$ then $|x_{n+1} | < |x_n |$, and if it is an RC successor then $|y_{n+1} | < |y_n |$. Thus an $xy$-sequence has infinitely many LC successors and infinitely many RC successors. From this it follows that there are infinitely many lines having critical left overlaps and infinitely many having critical right overlaps. Let these overlaps be, in order beginning with some left overlap, $\alpha _1 , \beta _1 , \alpha _2 , \beta _2 , \ldots$ where each $\alpha _i$ is a left overlap and each $\beta _i$ is a right overlap. Since there are only finitely many distinct left overlaps there must exist positive integers $p$ and $q$ such that $\alpha _{p+q} = \alpha _p$. By Theorem~8.3, there must be an LR~trail from $\alpha _{p+i}$ to $\beta _{p+i}$, and an RL~trail from $\beta _{p+i}$ to $\alpha _{p+i+1}$ for each $i$, $0 \leq i \leq q-1$. Thus the system $u \rightarrow v$ has a trail cycle.$\Box$ {\bf Theorem 8.5 (Main Theorem).} A system $u \rightarrow v$ has an infinite well behaved derivation if and only if it has a trail cycle. {\em Proof:\/} The system has an infinite well behaved derivation if and only if its inhibition system has an infinite derivation, by definition of ``well behaved'' (Section~2). Hence Theorem~8.5 is a consequence of Theorems~8.1 and~8.4.$\Box$ \vspace{.5in} {\bf 9. Examples.} This section illustrates the main theorem of Section~8. {\bf Theorem 9.1.} If a one-rule semi-Thue system has a loop of length $2$ then it has an infinite well behaved derivation that is generated by such a loop. {\em Proof:\/} By Theorem~1 of \cite{ku3}, in such a system there exist words $\beta, \delta$, and nonnull words $\epsilon , \phi , \gamma , \eta$ such that $u = \epsilon \phi = \gamma \eta$ and $v = \beta \gamma \epsilon = \eta \phi \delta$. We see that $\eta$ is a left overlap with companion left phrase $\gamma$ and $\epsilon$ is a right overlap with companion right phrase $\phi$. It follows that that there is an LR~trail of length $1$ from $\eta$ to $\epsilon$ and an RL~trail of length $1$ from $\epsilon$ to $\eta$. By Theorem~8.1 and its proof, there is an infinite derivation in the inhibition system based on a loop of length $2$. By deleting $\iota$'s in this derivation, we get an infinite well behaved derivation in the original system based on a loop of length~$2$ (namely, $\gamma \underline{\epsilon \phi}$ $\rightarrow \underline{\gamma} \overline{\underline{\eta} \phi \delta}$ $\rightarrow \overline{\beta \gamma \epsilon} \phi \delta $).$\Box$ {\bf Example 1.} We now conclude our discussion of the system $ccb \rightarrow bbccc$, which we began in Section~2. With Theorem~8.5 we are in a position to show quite easily that this system has no infinite well behaved derivation. The system has one left overlap $b$ with the companion left phrase $cc$, and two right overlaps $c$ and $cc$ with the respective companion right phrases $cb$ and $b$. We first ask, how many ways can we parse $v = bbccc$ as $\alpha _1 \alpha _2 \cdots \alpha _h z$ with $h \geq 2$, $\alpha _1$ a left overlap and $\alpha _2 , \ldots , \alpha _h$ right phrases? The answer is just one: $h = 2, \alpha _1 = b$ and $\alpha _2 = b$. Next, how many ways can we parse $v$ as $z' \beta _k \cdots \beta _2 \beta _1$ with $k \geq 2$, $\beta _1$ a right overlap and $\beta _2 , \ldots , \beta _k$ left phrases. The answer again is just one: $k = 2$, $\beta _1 = c$, $\beta _2 = cc$. There is an LR~trail from the left overlap $b$ to the right overlap $cc$ (whose companion right phrase is $b$), and an RL~trail from the right overlap $c$ to the left overlap $b$ (whose companion left phrase is $cc$), but there are no other trails. Thus there is no trail cycle, and the system $ccb \rightarrow bbccc$ has no infinite well behaved derivation. This contrasts with our observation in Section~2 that it has an infinite ill behaved derivation. We generalize this example to {\bf Example 2.} The systems $c^m b^n \rightarrow b^p c^q$ for $p > n > 0$ and $q > m > 0$ (identical to Example~1 of Section~6). The left overlaps are $b, \ldots ,b^{n-1} , b^n$ with respective companion left phrases $c^m b^{n-1} , \ldots ,c^m b,c^m$; the right overlaps are $c, \ldots ,c^{m-1} ,c^m$ with respective companion right phrases $c^{m-1} b^n , \ldots , cb^n ,b^n$. Since the $v$ of this system has no $cb$ factor, the only left phrase that can contribute to an RL trail is $c^m$, whose companion left overlap is $b^n$; and the only right phrase contributing to an LR trail is $b^n$ whose companion right overlap is $c^m$. It follows that the only left (right) overlap that can be a destination of an RL~trail (an LR~trail) is $b^n$ ($c^m$). Since we are looking for trail cycles, we can ignore all the other overlaps. We obtain a useful LR~trail from $b^n$ to $c^m$ by considering a parsing $v = b^n \alpha _2 \cdots \alpha _h z$, where $\alpha _h = b^n$. Clearly, there is such an LR~trail if and only if $p \geq 2n$. Similarly there is an RL~trail from $c^m$ to $b^n$ if and only if $q \geq 2m$. Thus the system has an infinite well behaved derivation if and only if $p \geq 2n$ and $q \geq 2m$. One such derivation is based on the loop $c^{2m}b^n ~ \triangleright ^2 ~c^{2m} b^n$. {\bf Example 3.} The system $abb \rightarrow bbabaab$ (\cite{ku3}, p. 16, Example 1) has two left overlaps $b$ and $bb$ with respective companion left phrases $ab$ and $a$. It has one right overlap $ab$ with companion right phrase $b$. It has an LR~trail of length $1$ from the left overlap $b$ to the right overlap $ab$, seen as follows: $v = \alpha _1 \alpha _2 z$ with $\alpha _1 = b$, $\alpha _2 = b$, $\beta _1 = ab$ ($\beta _1 \alpha _2 = u$). And it has an RL~trail of length $2$ from $ab$ to $b$: $v = z' \beta _3 \beta _2 \beta _1$ with $\beta _1 = ab$, $\beta _2 = a$, $\beta _3 = ab$ and $\alpha _1 = b$ ($\beta _3 \alpha _1 = u$). We can use the construction of the proof of Theorem~8.1, and then delete $\iota$'s, to get an infinite well behaved derivation in the system based on a loop of length~$3$. That loop is as follows: \[ \beta _3 v = \underline{abb} babaab \] \[ \overline{bbaba} \underline{\overline{ab} b} abaab \] \[ bbab \underline{a \overline{bb}} \overline{abaab} abaab \] \[ bbab \overline{bbabaab} abaababaab = bb \beta _3 v abaababaab \] {\bf Example 4.} Kurth mentions that the system $abaaaba \rightarrow aaababaaab$ (p. 16, Example~2) has the following loop of length $3$: $abaaabaaa \triangleright ^3 abaaabaaa$. We leave it to the reader to verify that the infinite derivation based on this loop is ill behaved. The system has two left overlaps $a$ and $aaaba$ with respective companion left phrases $abaaab$ and $ab$. It has two right overlaps $ab$ and $abaaab$ with respective companion right phrases $aaaba$ and $a$. It has LR~trails of lengths~$1$ and~$2$ from $a$ to $abaaab$, and an RL~trail from $abaaab$ to $aaaba$, and no other trails. Thus it has no infinite well behaved derivation. {\bf Example 5.} For completeness we mention Kurth's Example~3 (also on p.~16 of \cite{ku3}): $ababab \rightarrow babaabab$. This system is like his Example~2 in that it has a loop of length~$3$, but it is left to the reader to verify that it has no infinite well behaved derivation. Kurth proves that every one-rule semi-Thue system having a loop of length~$3$ has one of three specified structures, typified by these last three examples. {\bf Example 6.} The system \[ cdcbab \rightarrow bab (dcbab)^{h-2} babcdc(cdcba)^{k-2} cdc \] for $h,k \geq 3$, has two left overlaps $b$ and $bab$ with respective companion left phrases $cdcba$ and $cdc$. It also has two right overlaps $c$ and $cdc$ with respective companion right phrases $dcbab$ and $bab$. There is one LR~trail of length $h-1$ from the left overlap $bab$ to the right overlap $cdc$, and one RL~trail of length $k-1$ from $cdc$ to $bab$. There are no LR~trails from the left overlap $b$ or RL~trails from the right overlap $c$, so the RL~trails to $b$ and the LR~trails to $c$ can be ignored. Therefore, there is exactly one trail cycle, which involves the left overlap $bab$ and the right overlap $cdc$. It gives us the derivation loop \[ cdcv \triangleright ^{h+k-2} cdcv \] This example proves that arbitrarily long trails are required to satisfy the condition of Theorem~8.5, and that the minimal-length derivation loops on which infinite well behaved derivations are based are arbitrarily long. Knowing that there are systems whose trail cycles require arbitrarily long trails, we have the {\bf Open question.} Are there one-rule semi-Thue systems requiring an arbitrarily large number of trails for the loop? I am unable to give an example of a system that has an infinite well behaved derivation where the only trail cycles have more than two trails. Nor can I prove the contradictory assertion that every system with an infinite well behaved derivation has a trail cycle with only two trails. There is one final open question. It was mentioned that, for the problem of whether a given system has an infinite well behaved derivation, the algorithm of this section is more efficient than the algorithm of Section~2. This is clearly true for certain simple examples, for which the former requires little effort but the latter would take much time. However, I cannot give a complexity analysis to make a more general assertion. I can only offer a {\bf Conjecture.} The algorithm of Section~8 is more efficient than the algorithm of Section~2 for the problem, does a given one-rule semi-Thue system have an infinite well behaved derivation? \vspace{.5in} \begin{thebibliography}{99} \bibitem{gkm} John V. Guttag, Deepak Kapur and David R. Musser, ``On proving uniform termination and restricted termination of rewriting systems,'' {\em Siam J. Computing,\/} vol.~12~(1983), pp.~189--214. \bibitem{d87} Nahum Dershowitz, ``Termination of rewriting,'' {\em J. Symbolic Computation,\/} vol.~3~(1987), pp. 69--115, and vol.~4~(1987), pp.~409--410. \bibitem{ja} Matthias Jantzen, {\em Confluent String Rewriting,\/} Monographs on Theoretical Computer Science, vol.~14, Springer-Verlag,~1988. \bibitem{ku1} Winfried Kurth, {\em Termination und Konfluenz von Semi-Thue-systemen mit nur einer Regel,\/} Dissertation, Technischen Universit\"{a}t Clausthal,~1990. \bibitem{ku2} Winfried Kurth, ``Explanations to the text,'' unpublished paper of five pages distributed by the author, summarizing~\cite{ku1}. \bibitem{bo} Ronald V. Book and Friedrich Otto, {\em String-rewriting systems,\/} Springer-Verlag,~1993. \bibitem{d93} Nahum Dershowitz and Charles Hoot, ``Topics in termination,'' in {\em Lecture Notes in Computer Science,\/} no. 690 {\em (Rewriting techniques and applications,\/} Claude Kirchner, ed.), Springer-Verlag,~1993. \bibitem{mcn} Robert McNaughton, ``The uniform halting problem for one-rule semi-Thue systems: progress report,'' Report 94-18, Department of Computer Science, Rensselaer Polytechnic Institute, 1994. \bibitem{zg} H. Zantema and A. Geser, ``A complete characterization of termination of $0^p 1^q \rightarrow 1^r 0^s$,'' presented at a conference in 1995. Appeared previously as Report UU-CS-1994-44, Computer Science, Universiteit Utrecht, Utrecht, The Netherlands,~1994. (This reference will be updated.) \bibitem{ku3} Winfried Kurth, ``One-rule semi-Thue systems with loops of length one, two or three,'' Report, Abteillung f\"{u}r forstliche Biometrie und Informatik, Universit\"{a}t G\"{o}ttingen,~1995. \end{thebibliography} \end{document}