compare -b -t "oct28relZ.tex" "oct31relJ.tex"
File #1: oct28relZ.tex
File #2: oct31relJ.tex

Nonmatching lines (File "oct28relZ.tex"; Line 1:19; File "oct31relJ.tex"; Line 1:32)
   1	\documentstyle[11pt]{article}
   2	%\documentstyle[fullpage,11pt,amssymbols]{article}
   3	%\input{BoxedEPS}
   4	%\HideDisplacementBoxes
   5	%\SetOzTeXEPSFSpecial
   6	%\marginparwidth 0pt
   7	%\oddsidemargin 0pt
   8	%\evensidemargin 0pt
   9	%\marginparsep 0pt
  10	
  11	\topmargin 0pt
  12	
  13	%\textwidth 6.5in
  14	%\textheight 8.5 in
  15	%\input{amssym.def}
  16	
  17	\input{diagrams} % Paul Taylor's Macro Package
  18	\begin{document}
  19	

   1	\documentclass{article}
   2	\textwidth 130mm
   3	\textheight 200mm
   4	\renewenvironment{abstract}{\section*{Abstract}\small}{}
   5	\newtheorem{definition}{Definition}
   6	\newtheorem{example}[definition]{Example}
   7	\newtheorem{application}[definition]{Application}
   8	\newtheorem{theorem}[definition]{Theorem}
   9	\newtheorem{exercise}[definition]{Exercise}
  10	\newtheorem{lemma}[definition]{Lemma}
  11	\newtheorem{notation}[definition]{Notation}
  12	\newtheorem{observation}[definition]{Observation}
  13	\newtheorem{proposition}[definition]{Proposition}
  14	\newtheorem{proposal}[definition]{Proposal}
  15	\newtheorem{remark}[definition]{Remark}
  16	\newtheorem{result}[definition]{Result}
  17	\newtheorem{conjecture}[definition]{Conjecture}
  18	\newtheorem{claim}[definition]{Claim}
  19	\newtheorem{assumption}[definition]{Assumption}
  20	\newtheorem{corollary}[definition]{Corollary}
  21	\makeatletter
  22	\renewcommand{\@begintheorem}[2]{ % not in italics
  23	 \trivlist\item[\hskip\labelsep{\bf #1\ #2}]}
  24	\renewcommand{\@opargbegintheorem}[3]{\trivlist
  25	 \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]}
  26	\makeatother
  27	\newtheorem{proof}{Proof}
  28	\renewcommand{\theproof}{} % no numbers on proofs
  29	% End of preamble
  30	\usepackage{latexsym}
  31	\input{diagrams} % Paul Taylor's Macro Package
  32	\begin{document}


Extra lines in 1st before 54 in 2nd (File "oct28relZ.tex"; Line 41; File "oct31relJ.tex"; Line Æ54)
  41	


Nonmatching lines (File "oct28relZ.tex"; Line 46:67; File "oct31relJ.tex"; Line 58:60)
  46	
  47	
  48	
  49	
  50	\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
  51	
  52	\newtheorem{thm}{Theorem}[section]
  53	\newtheorem{lem}[thm]{Lemma}% [section]
  54	\newtheorem{cor}[thm]{Corollary}% [section]
  55	\newtheorem{ex}[thm]{Example}% [section]
  56	\newtheorem{rem}[thm]{Remark}% [section]
  57	\newtheorem{nota}[thm]{Notation}% [section]
  58	\newtheorem{prop}[thm]{Proposition}% [section]
  59	\newtheorem{deff}[thm]{Definition}% [section]
  60	
  61	%%%%\newtheorem{proof}{Proof}
  62	%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
  63	\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
  64	\newenvironment{proof}{\noindent{\bf Proof }}{}
  65	
  66	
  67	\newcommand{\notation}{{\bf Notation }}

  58	\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
  59	
  60	\newcommand{\notationn}{{\bf Notation }}


Extra lines in 1st before 70 in 2nd (File "oct28relZ.tex"; Line 77:78; File "oct31relJ.tex"; Line Æ70)
  77	\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
  78	\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}


Extra lines in 1st before 81 in 2nd (File "oct28relZ.tex"; Line 90; File "oct31relJ.tex"; Line Æ81)
  90	\newcommand{\eclas}[1]{\mbox{$\langle{#1}\rangleÄ$}}


Extra lines in 1st before 114 in 2nd (File "oct28relZ.tex"; Line 124; File "oct31relJ.tex"; Line Æ114)
 124	


Nonmatching lines (File "oct28relZ.tex"; Line 131:149; File "oct31relJ.tex"; Line 120)
 131	\newcommand{\bd}{\begin{deff}\em}
 132	\newcommand{\bdl}[1]{\begin{deff}\em\label{#1}}
 133	\newcommand{\bl}{\begin{lem}\em}
 134	\newcommand{\bll}[1]{\begin{lem}\em\label{#1}}
 135	\newcommand{\bp}{\begin{prop}\em}
 136	\newcommand{\bpl}[1]{\begin{prop}\em\label{#1}}
 137	\newcommand{\bt}{\begin{thm}\em}
 138	\newcommand{\btl}[1]{\begin{thm}\em\label{#1}}
 139	\newcommand{\bel}[1]{\begin{ex}\em\label{#1}}
 140	\newcommand{\bc}{\begin{cor}\em}
 141	\newcommand{\bcl}[1]{\begin{cor}\em\label{#1}}
 142	\newcommand{\bproof}{\begin{proof}}
 143	\newcommand{\eproof}{\end{proof}}
 144	\newcommand{\ed}{\end{deff}}
 145	\newcommand{\el}{\end{lem}}
 146	\newcommand{\ep}{\end{prop}}
 147	\newcommand{\et}{\end{thm}}
 148	\newcommand{\ee}{\end{ex}}
 149	\newcommand{\ec}{\end{cor}}

 120	


Extra lines in 2nd before 163 in 1st (File "oct28relZ.tex"; Line Æ163; File "oct31relJ.tex"; Line 134)
 134	\newcommand{\richard}[1]{\{{\bf Zurab:~\sf #1}\}} % Highlight text.


Nonmatching lines (File "oct28relZ.tex"; Line 177:180; File "oct31relJ.tex"; Line 149:152)
 177	We impose on $\stab$ natural \emph{stability} conditions, that are
 178	\zurab{sufficient} for each term not in $\stab$ to have at least one
 179	$\stab$-needed redex, and for repeated
 180	contraction of $\stab$-needed redexes in a term $t$ to lead to a

 149	We impose natural \emph{stability} conditions on $\stab$, that
 150	guarantee that each term not in $\stab$ has at least one
 151	$\stab$-needed redex, such that repeated
 152	contraction of $\stab$-needed redexes in a term $t$ will lead to a


Nonmatching lines (File "oct28relZ.tex"; Line 185; File "oct31relJ.tex"; Line 157)
 185	head-normal-forms, and weak head-normal-forms, in the \lc, are all stable

 157	head-normal forms, and weak head-normal forms, in the \lc, are all stable


Nonmatching lines (File "oct28relZ.tex"; Line 214:215; File "oct31relJ.tex"; Line 186:187)
 214	-- a redex with at least one \zurab{contracted \emph{residual}} in
 215	any reduction to normal

 186	-- a redex with at least one contracted \emph{residual} in
 187	every reduction to normal


Nonmatching lines (File "oct28relZ.tex"; Line 218:220; File "oct31relJ.tex"; Line 190:192)
 218	to its normal form whenever there is one; we refer to it as the
 219	\emph{Normalization Theorem}. They also define the class of \emph{strongly
 220	sequential} OTRSs where a needed redex can efficiently be found in any

 190	to its normal form whenever there is one; we refer to this as the
 191	\emph{Normalization Theorem}. They also define the class of \emph{strongly
 192	sequential} OTRSs where a needed redex can be found efficiently in any


Nonmatching lines (File "oct28relZ.tex"; Line 238:253; File "oct31relJ.tex"; Line 210:225)
 238	defined \zurab{the \emph{essential} strategy} for the
 239	$\lambda$-calculus~\cite{[colog]}, OTRSs~\cite{[rta]}, and \emph{Expression
 240	Reduction Systems} (OERSs)~\cite{[caap]}. The strategy contracts
 241	\emph{essential} redexes -- the redexes that have \emph{descendants} under
 242	any reduction. The notion of descendant is a refinement of that of
 243	\emph{residual} -- the descendant of a contracted redex is its contractum,
 244	while it does not have residuals.\footnote{\zurab{Decsendants and residuals
 245	are sometimes used as synonyms, which we think is not justified.}}
 246	Hence, essentiality makes sense for all subterms, not only for redexes.
 247	In~\cite{[Mar]}, Maranget introduces a different notion of neededness,
 248	where a redex $u$ is needed if it has a residual under any reduction that
 249	does not contract the residuals of $u$. This neededness notion makes sense
 250	also for terms that do not have a normal form, and coincides with the
 251	notion of essentiality.
 252	
 253	 Sekar and Ramakrishnan~\cite{[SeRa]} study a normalizing

 210	defined the \emph{essential} strategy for the
 211	$\lambda$-calculus~\cite{[colog]}, OTRSs~\cite{[rta]}, and \emph{Expression
 212	Reduction Systems} (OERSs)~\cite{[caap]}. This strategy contracts
 213	\emph{essential} redexes -- the redexes that have \emph{descendants} under
 214	every reduction. The notion of descendant is a refinement of
 215	\emph{residual} -- the descendant of a contracted redex is its contractum,
 216	while it does not have residuals.\footnote{\john{Note that descendants and residuals
 217	are sometimes treated as synonymous in the literature.}}
 218	Essentiality makes sense for all subterms, not only redexes.
 219	In~\cite{[Mar]}, Maranget introduces a different notion of neededness,
 220	where a redex $u$ is needed if it has a residual under any reduction that
 221	does not contract residuals of $u$. This neededness notion makes sense
 222	even for terms that do not have a normal form, and coincides with the
 223	notion of essentiality.
 224	
 225	Sekar and Ramakrishnan~\cite{[SeRa]} study a normalizing


Nonmatching lines (File "oct28relZ.tex"; Line 260; File "oct31relJ.tex"; Line 232)
 260	inessential subterms (i.e., the garbage) in simply typable $\lambda$-terms.

 232	inessential subterms (i.e., the garbage) in simply typeable $\lambda$-terms.


Nonmatching lines (File "oct28relZ.tex"; Line 274:276; File "oct31relJ.tex"; Line 246:248)
 274	terms of different shapes (\zurab{e.g., weak-head-normal forms,
 275	constructor head-normal forms,} etc.) as the
 276	results, it is natural to ask what properties a set of terms must possess

 246	terms of different shapes (weak-head-normal forms,
 247	constructor head-normal forms, etc.) as the
 248	results of computation , it is natural to ask what properties a set of terms must possess


Extra lines in 2nd before 280 in 1st (File "oct28relZ.tex"; Line Æ280; File "oct31relJ.tex"; Line 252:253)
 252	\john{Would it open a can of worms to talk of infinite reductions? We can compute to whnf even when no nf exists.}
 253	


Nonmatching lines (File "oct28relZ.tex"; Line 293:304; File "oct31relJ.tex"; Line 267:276)
 293	We impose a natural condition on $\stab$, called \emph{stability}, which is
 294	\zurab{sufficient} for each term not in $\stab$-normal form (i.e.,
 295	not in $\stab$) to have at least one $\stab$-needed redex, and repeated
 296	contraction of $\stab$-needed redexes in a term $t$ to lead to an
 297	$\stab$-normal form of $t$ whenever there is one.
 298	A set $\stab$ of terms is stable if it is \emph{closed under parallel moves}:
 299	for any $t\not\in \stab$, any $P:t\doar o\in \stab$, and any $Q:t\doar e$
 300	not containing terms in $\stab$, the final term of $P/Q$, the
 301	\emph{residual} of $P$ under $Q$, is in $\stab$; and is \emph{closed under
 302	unneeded expansion}: for any $e\red{u}o$ such that $e\not\in \stab$ and
 303	$o\in \stab$, a residual of $u$ is contracted in any reduction from $e$ to
 304	a term in~$\stab$.\footnote{When the rewrite system is non-duplicating

 267	We impose a natural condition on $\stab$, \emph{stability}, which
 268	guarantees that each term not in $\stab$-normal form (i.e.,
 269	not in $\stab$) has at least one $\stab$-needed redex, such that repeated
 270	contraction of $\stab$-needed redexes in a term $t$ will lead to an
 271	$\stab$-normal form of $t$ whenever there is one.
 272	A set $\stab$ of terms is stable if it is \emph{closed under
 273	unneeded expansion}: for any $e\red{u}o$ such that $e\not\in \stab$ and
 274	$o\in \stab$, a residual of $u$ is contracted in any reduction from $e$ to
 275	a term in~$\stab$; and is \emph{closed under reduction}:
 276	for any $t\ar o$ where $t\in \stab$, then $o\in \stab$.\footnote{When the rewrite system is non-duplicating


Extra lines in 2nd before 325 in 1st (File "oct28relZ.tex"; Line Æ325; File "oct31relJ.tex"; Line 297:303)
 297	Although we claim that our definition of stability is the most natural that has been proposed, it is possible to weaken the conditions for stability and still retain the concept of relative neededness. For example, an alternative definition is explored in
 298	\emph{closed under parallel moves}:
 299	for any $t\not\in \stab$, any $P:t\doar o\in \stab$, and any $Q:t\doar e$
 300	not containing terms in $\stab$, the final term of $P/Q$, the
 301	\emph{residual} of $P$ under $Q$, is in $\stab$. \john{Is it necessary to say
 302	``not containing terms in $\stab$'' for Q?}
 303	


Nonmatching lines (File "oct28relZ.tex"; Line 423:429; File "oct31relJ.tex"; Line 402:408)
 423	The concepts introduced in Section~\ref{S.rel.need.} are taken
 424	from~\cite{[ctrs]}, but the definitions are different in that
 425	the new definitions use only the residual concept while the original
 426	definitions are based on a concept of descendants for subterms and
 427	components. \zurab{Furthermore, we have simplified the stability concept
 428	(by secrifying the generality). Our labelling system in Section~\ref{S.labels}
 429	is based on an unpublished work by Kennaway and Sleep~\cite{[K.S.]}.}

 402	The concepts introduced in Section~\ref{S.rel.need.} build
 403	on~\cite{[ctrs]}, but here the
 404	definitions use only the residual concept while the earlier
 405	definitions were based on a concept of descendants for subterms and
 406	components. The stability concept is simpler, and hence slightly less general.
 407	The labelling system in Section~\ref{S.labels}
 408	\john{presents} unpublished work by Kennaway and Sleep~\cite{[K.S.]}.


Extra lines in 2nd before 436 in 1st (File "oct28relZ.tex"; Line Æ436; File "oct31relJ.tex"; Line 415:416)
 415	\section{Orthogonal Expression Reduction Systems}
 416	\label{S.CRS}


Extra lines in 1st before 419 in 2nd (File "oct28relZ.tex"; Line 438:444; File "oct31relJ.tex"; Line Æ419)
 438	
 439	
 440	\section{Orthogonal Expression Reduction Systems}
 441	\label{S.CRS}
 442	
 443	
 444	


Nonmatching lines (File "oct28relZ.tex"; Line 465; File "oct31relJ.tex"; Line 439)
 465	\begin{deff}\em

 439	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 478; File "oct31relJ.tex"; Line 452)
 478	{\em metavariables} $A, B,\ldots$ that range over terms, but with an

 452	\emph{metavariables} $A, B,\ldots$ that range over terms, but with an


Nonmatching lines (File "oct28relZ.tex"; Line 484:485; File "oct31relJ.tex"; Line 458)
 484	is a metaterm and $\theta$ is an assignment, then the $\theta$-{\em
 485	instance} $t\theta$ of $t$ is the term obtained from $t$ by replacing

 458	is a metaterm and $\theta$ is an assignment, then the $\theta$-\emph{instance} $t\theta$ of $t$ is the term obtained from $t$ by replacing


Nonmatching lines (File "oct28relZ.tex"; Line 500; File "oct31relJ.tex"; Line 473)
 500	\end{deff}

 473	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 514; File "oct31relJ.tex"; Line 487)
 514	\begin{deff}\em

 487	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 545; File "oct31relJ.tex"; Line 518)
 545	\end{deff}

 518	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 548:549; File "oct31relJ.tex"; Line 521:522)
 548	\zurab{For the sake of simplicity, below we restrict ourselves to
 549	\emph{variable-capturte-free ERSs}, which are ERSs in which all

 521	\zurab{Begin (} For the sake of simplicity, below we restrict ourselves to
 522	\emph{variable-capture-free ERSs}, which are ERSs in which all


Nonmatching lines (File "oct28relZ.tex"; Line 552:553; File "oct31relJ.tex"; Line 525:526)
 552	CERSs}~\cite{[pun-ic]}. \footnote{\zurab{Roughly,
 553	full extendeedness means that an erasing step cannot turn a non-redex

 525	CERSs}~\cite{[pun-ic]}. Roughly,
 526	full extendedness means that an erasing step cannot turn a non-redex


Nonmatching lines (File "oct28relZ.tex"; Line 556:558; File "oct31relJ.tex"; Line 529:533)
 556	can create an $\eta$-redex above the contractum. The full extendeedness
 557	restriction is necessary for many important results in the theory
 558	of higher-order rewriting, see e.g.~\cite{[Raa.th],[Oos],[Oos97],[pun-ic]}.}}}

 529	can create an $\eta$-redex above the contractum. The full extendedness
 530	restriction is necessary for many important results in the theory
 531	of higher-order rewriting, see e.g.~\cite{[Raa.th],[Oos],[Oos97],[pun-ic]}
 532	\zurab{) End}.
 533	


Nonmatching lines (File "oct28relZ.tex"; Line 564:566; File "oct31relJ.tex"; Line 539:541)
 564	not really necessary -- free variables can be used instead, as in TRSs
 565	(since (free) variables in TRS rules play the role of metavariables in ERS
 566	rules). We will indeed do so at least when giving TRS examples.

 539	not really necessary -- free variables can be used instead, as in TRSs,
 540	since (free) variables in TRS rules play the role of metavariables in ERS
 541	rules. We will indeed do so at least when giving TRS examples.


Nonmatching lines (File "oct28relZ.tex"; Line 590; File "oct31relJ.tex"; Line 565)
 590	\begin{nota}\em

 565	\begin{notation}


Nonmatching lines (File "oct28relZ.tex"; Line 597; File "oct31relJ.tex"; Line 572)
 597	\end{nota}

 572	\end{notation}


Nonmatching lines (File "oct28relZ.tex"; Line 643; File "oct31relJ.tex"; Line 618)
 643	The following \emph{strong Church-Rosser (confluence)}

 618	The \emph{Strong Church-Rosser (confluence)}


Nonmatching lines (File "oct28relZ.tex"; Line 651:659; File "oct31relJ.tex"; Line 626:634)
 651	\begin{thm}\em
 652	\label{T.FD.}
 653	\zurab{All complete developments of a set of redexes in a term $t$, in an OERS,
 654	end at the same term $s$, and the residuals of any redex in $t$ along
 655	any complete development are the same redexes in~$s$.}
 656	\end{thm}
 657	
 658	
 659	\begin{thm}\em

 626	\begin{theorem}
 627	\label{T.FD.}
 628	All complete developments of a set of redexes in a term $t$, in an OERS,
 629	end at the same term $s$, and the residuals in~$s$ of any redex in $t$ along
 630	any complete development are the same.
 631	\end{theorem}
 632	
 633	
 634	\begin{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 663; File "oct31relJ.tex"; Line 638)
 663	\end{thm}

 638	\end{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 691; File "oct31relJ.tex"; Line 666)
 691	\bdl{D.exter.and.vanish.}

 666	\begin{definition}\label{D.exter.and.vanish.}


Nonmatching lines (File "oct28relZ.tex"; Line 694:713; File "oct31relJ.tex"; Line 669:688)
 694	\item[(1)] We call $P:t\doar o$ \emph{external} to a redex $u\subt t$
 695	if $P$ does not \zurab{contract residuals} of~$u$.
 696	
 697	\item[(2)] We call $P:t\doar o$ \emph{external} to a set of redexes
 698	$U\subt t$ if $P$ is external to all $u\in U$.
 699	
 700	\item[(3)] We say that $P$ \emph{$\stab$-suppresses} $u$ if $P$ is
 701	$\stab$-normalizing and is external to~$u$.
 702	
 703	\item[(4)] We say that $P$ \emph{erases} $u$ if $u/P=\emp$. Note that
 704	contracting a redex erases it.
 705	
 706	\item[(5)] We say that $P$ \emph{discards} $u$ if $P$ is external to $u$ and
 707	$u/P=\emp$.
 708	\end{enumerate}
 709	\ed
 710	
 711	
 712	
 713	\begin{deff}\em

 669	\item[(1)] $P:t\doar o$ is \emph{external} to a redex $u\subt t$
 670	if $P$ does not contract any residual of~$u$.
 671	
 672	\item[(2)] $P:t\doar o$ is \emph{external} to a set of redexes
 673	$U\subt t$ if $P$ is external to all $u\in U$.
 674	
 675	\item[(3)] $P$ \emph{$\stab$-suppresses} $u$ if $P$ is
 676	$\stab$-normalizing and is external to~$u$.
 677	
 678	\item[(4)] $P$ \emph{erases} $u$ if $u/P=\emp$. Note that
 679	contracting a redex erases it.
 680	
 681	\item[(5)] $P$ \emph{discards} $u$ if $P$ is external to $u$ and
 682	$u/P=\emp$.
 683	\end{enumerate}
 684	\end{definition}
 685	
 686	
 687	
 688	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 719:720; File "oct31relJ.tex"; Line 694:695)
 719	starting from $t$ at least one of its residuals is contracted,} and call
 720	\emph{$\Pi$-unneeded} otherwise.

 694	starting from $t$ at least one of its residuals is contracted,} \john{Or: no reduction in $\Pi$ is external to $u$} and call
 695	\emph{$\Pi$-unneeded} otherwise. \john{Or reverse the definition and say unneeded if some reduction is external to $u$.}


Nonmatching lines (File "oct28relZ.tex"; Line 724:726; File "oct31relJ.tex"; Line 699:701)
 724	denoted \emph{$\stab$-normalizing} reductions, \zurab{and we will call a term
 725	$t$ \emph{$\stab$-normalizing} if there is an $\stab$-normalizing reduction
 726	starting from $t$.}

 699	denoted \emph{$\stab$-normalizing} reductions. A term
 700	$t$ is denoted \emph{$\stab$-normalizing} if some $\stab$-normalizing reduction
 701	starts at $t$.


Nonmatching lines (File "oct28relZ.tex"; Line 731; File "oct31relJ.tex"; Line 706)
 731	\end{deff}

 706	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 747:749; File "oct31relJ.tex"; Line 722:724)
 747	We will state the definition of the property of sets of terms for which
 748	it is possible to generalise the Normalization Theorem and will then
 749	give some examples showing why some intuitively simpler definitions

 722	We will state conditions on sets of terms which guarantee that
 723	a generalization of the Normalization Theorem will be satisfied.
 724	We will give some examples showing why some intuitively simpler definitions


Nonmatching lines (File "oct28relZ.tex"; Line 753; File "oct31relJ.tex"; Line 728)
 753	\begin{deff}\em

 728	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 756:757; File "oct31relJ.tex"; Line 731:732)
 756	\item[(a)] $\stab$ \zurab{is \emph{closed under reduction}: if $t\in\stab$
 757	and $t\doar s$, then $s\in\stab$;} and

 731	\item[(a)] $\stab$ is \emph{closed under reduction}: if $t\in\stab$
 732	and $t\doar s$, \john{$t\ar s$,} then $s\in\stab$; and


Nonmatching lines (File "oct28relZ.tex"; Line 763; File "oct31relJ.tex"; Line 738)
 763	\end{deff}

 738	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 771:773; File "oct31relJ.tex"; Line 746:748)
 771	TRSs~\cite{[Nok.thi.]}, and the set of root-stable forms (which are terms
 772	that cannot be rewritten to a redex)~\cite{[Mid]}. All these sets are
 773	closed under reduction, which implies closure under parallel moves.

 746	TRSs~\cite{[Nok.thi.]}, and the set of root-stable forms (terms
 747	that cannot be rewritten to a redex)~\cite{[Mid]}. All these sets are
 748	closed under reduction \john{removed here: which implies closure under parallel moves}.


Nonmatching lines (File "oct28relZ.tex"; Line 868; File "oct31relJ.tex"; Line 843)
 868	\begin{ex}\em

 843	\begin{example}


Nonmatching lines (File "oct28relZ.tex"; Line 896; File "oct31relJ.tex"; Line 871)
 896	\end{ex}

 871	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 920:921; File "oct31relJ.tex"; Line 895:896)
 920	Let there be a set ${\cal L}_0$ of {\em atomic labels},
 921	and a set ${\cal C}$ of {\em label constructors} in $1-1$ correspondence with

 895	Let there be a set ${\cal L}_0$ of \emph{atomic labels},
 896	and a set ${\cal C}$ of \emph{label constructors} in $1-1$ correspondence with


Nonmatching lines (File "oct28relZ.tex"; Line 933; File "oct31relJ.tex"; Line 908)
 933	By a {\em labelled term} we mean any term which results from this

 908	By a \emph{labelled term} we mean any term which results from this


Nonmatching lines (File "oct28relZ.tex"; Line 949; File "oct31relJ.tex"; Line 924)
 949	We now construct the set of {\em labelled rules}.

 924	We now construct the set of \emph{labelled rules}.


Nonmatching lines (File "oct28relZ.tex"; Line 959; File "oct31relJ.tex"; Line 934)
 959	other than metasubstitutions,

 934	except metasubstitutions,


Nonmatching lines (File "oct28relZ.tex"; Line 964; File "oct31relJ.tex"; Line 939)
 964	(This tuple of labels is called the {\em signature} of $f(s)$.)

 939	(This tuple of labels is called the \emph{signature} of $f(s)$.)


Nonmatching lines (File "oct28relZ.tex"; Line 1020; File "oct31relJ.tex"; Line 995)
1020	\begin{prop}\em

 995	\begin{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1030:1036; File "oct31relJ.tex"; Line 1005:1011)
1030	\bproof
1031	Easy from definition of the labelling.
1032	\eproof
1033	\end{prop}
1034	
1035	
1036	\begin{cor}\em

1005	\begin{proof}
1006	Easy from definition of the labelling.
1007	\end{proof}
1008	\end{proposition}
1009	
1010	
1011	\begin{corollary}


Nonmatching lines (File "oct28relZ.tex"; Line 1043:1045; File "oct31relJ.tex"; Line 1018:1020)
1043	\end{cor}
1044	
1045	\begin{prop}\em

1018	\end{corollary}
1019	
1020	\begin{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1050:1053; File "oct31relJ.tex"; Line 1025:1028)
1050	\bproof
1051	See~\cite{[Kl.CRS],[Mel],[Oos97]}.
1052	\eproof
1053	\end{prop}

1025	\begin{proof}
1026	See~\cite{[Kl.CRS],[Mel],[Oos97]}.
1027	\end{proof}
1028	\end{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1086; File "oct31relJ.tex"; Line 1061)
1086	\bll{L.external.rem.ext.}

1061	\begin{lemma}\label{L.external.rem.ext.}


Nonmatching lines (File "oct28relZ.tex"; Line 1114; File "oct31relJ.tex"; Line 1089)
1114	\el

1089	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1117; File "oct31relJ.tex"; Line 1092)
1117	\begin{cor}\em

1092	\begin{corollary}


Nonmatching lines (File "oct28relZ.tex"; Line 1121; File "oct31relJ.tex"; Line 1096)
1121	\end{cor}

1096	\end{corollary}


Nonmatching lines (File "oct28relZ.tex"; Line 1128; File "oct31relJ.tex"; Line 1103)
1128	\begin{lem}\em

1103	\begin{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1139; File "oct31relJ.tex"; Line 1114)
1139	\end{lem}

1114	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1149; File "oct31relJ.tex"; Line 1124)
1149	\begin{thm}\em

1124	\begin{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1192; File "oct31relJ.tex"; Line 1167)
1192	\end{thm}

1167	\end{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1195; File "oct31relJ.tex"; Line 1170)
1195	\noindent\notation

1170	\noindent\notationn


Nonmatching lines (File "oct28relZ.tex"; Line 1201; File "oct31relJ.tex"; Line 1176)
1201	\begin{lem}\em

1176	\begin{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1212; File "oct31relJ.tex"; Line 1187)
1212	\end{lem}

1187	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1221; File "oct31relJ.tex"; Line 1196)
1221	\begin{prop}\em

1196	\begin{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1234; File "oct31relJ.tex"; Line 1209)
1234	\end{prop}

1209	\end{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1267; File "oct31relJ.tex"; Line 1242)
1267	\begin{ex}\em

1242	\begin{example}


Nonmatching lines (File "oct28relZ.tex"; Line 1277; File "oct31relJ.tex"; Line 1252)
1277	\end{ex}

1252	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 1293; File "oct31relJ.tex"; Line 1268)
1293	\bd

1268	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1296; File "oct31relJ.tex"; Line 1271)
1296	\ed

1271	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1311; File "oct31relJ.tex"; Line 1286)
1311	\begin{deff}\em

1286	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1320; File "oct31relJ.tex"; Line 1295)
1320	\end{deff}

1295	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1334; File "oct31relJ.tex"; Line 1309)
1334	\begin{deff}\em

1309	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1374; File "oct31relJ.tex"; Line 1349)
1374	\end{deff}

1349	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1377; File "oct31relJ.tex"; Line 1352)
1377	\begin{lem}\em

1352	\begin{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1399; File "oct31relJ.tex"; Line 1374)
1399	\end{lem}

1374	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1402; File "oct31relJ.tex"; Line 1377)
1402	\begin{lem}\em

1377	\begin{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1428; File "oct31relJ.tex"; Line 1403)
1428	\end{lem}

1403	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1433; File "oct31relJ.tex"; Line 1408)
1433	\begin{thm}\em

1408	\begin{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1452; File "oct31relJ.tex"; Line 1427)
1452	\end{thm}

1427	\end{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1483; File "oct31relJ.tex"; Line 1458)
1483	\begin{deff}\em

1458	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1496; File "oct31relJ.tex"; Line 1471)
1496	\end{deff}

1471	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1504; File "oct31relJ.tex"; Line 1479)
1504	\bel{E.nne.per.sec.con.}

1479	\begin{example}\label{E.nne.per.sec.con.}


Nonmatching lines (File "oct28relZ.tex"; Line 1562; File "oct31relJ.tex"; Line 1537)
1562	\ee

1537	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 1566; File "oct31relJ.tex"; Line 1541)
1566	\bll{L.prs.m-nee.sec.}

1541	\begin{lemma}\label{L.prs.m-nee.sec.}


Nonmatching lines (File "oct28relZ.tex"; Line 1571; File "oct31relJ.tex"; Line 1546)
1571	\bproof

1546	\begin{proof}


Nonmatching lines (File "oct28relZ.tex"; Line 1577:1578; File "oct31relJ.tex"; Line 1552:1553)
1577	\eproof
1578	\el

1552	\end{proof}
1553	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1588; File "oct31relJ.tex"; Line 1563)
1588	\begin{deff}\em

1563	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1596; File "oct31relJ.tex"; Line 1571)
1596	\end{deff}

1571	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1617; File "oct31relJ.tex"; Line 1592)
1617	\begin{lem}\em

1592	\begin{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1629; File "oct31relJ.tex"; Line 1604)
1629	\end{lem}

1604	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1643; File "oct31relJ.tex"; Line 1618)
1643	\begin{ex}\em

1618	\begin{example}


Nonmatching lines (File "oct28relZ.tex"; Line 1672; File "oct31relJ.tex"; Line 1647)
1672	\end{ex}

1647	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 1687; File "oct31relJ.tex"; Line 1662)
1687	\begin{deff}\em

1662	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1694; File "oct31relJ.tex"; Line 1669)
1694	\end{deff}

1669	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1697; File "oct31relJ.tex"; Line 1672)
1697	\begin{deff}\em

1672	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1716; File "oct31relJ.tex"; Line 1691)
1716	\end{deff}

1691	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1719; File "oct31relJ.tex"; Line 1694)
1719	\bel{E.abs.una.}

1694	\begin{example}\label{E.abs.una.}


Nonmatching lines (File "oct28relZ.tex"; Line 1729; File "oct31relJ.tex"; Line 1704)
1729	\ee

1704	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 1742; File "oct31relJ.tex"; Line 1717)
1742	\begin{prop}\em

1717	\begin{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1746; File "oct31relJ.tex"; Line 1721)
1746	\end{prop}

1721	\end{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1749; File "oct31relJ.tex"; Line 1724)
1749	\begin{lem}\em

1724	\begin{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1774; File "oct31relJ.tex"; Line 1749)
1774	\end{lem}

1749	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1790; File "oct31relJ.tex"; Line 1765)
1790	\begin{prop}\em

1765	\begin{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1809; File "oct31relJ.tex"; Line 1784)
1809	\end{prop}

1784	\end{proposition}


Nonmatching lines (File "oct28relZ.tex"; Line 1814; File "oct31relJ.tex"; Line 1789)
1814	\btl{T.qpmn.gen.min.str.}

1789	\begin{theorem}\label{T.qpmn.gen.min.str.}


Nonmatching lines (File "oct28relZ.tex"; Line 1824; File "oct31relJ.tex"; Line 1799)
1824	\bproof

1799	\begin{proof}


Nonmatching lines (File "oct28relZ.tex"; Line 1831:1832; File "oct31relJ.tex"; Line 1806:1807)
1831	\eproof
1832	\et

1806	\end{proof}
1807	\end{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1860; File "oct31relJ.tex"; Line 1835)
1860	\bd

1835	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1863; File "oct31relJ.tex"; Line 1838)
1863	\ed

1838	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1875; File "oct31relJ.tex"; Line 1850)
1875	\bt

1850	\begin{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1880; File "oct31relJ.tex"; Line 1855)
1880	\et

1855	\end{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1899; File "oct31relJ.tex"; Line 1874)
1899	\begin{deff}\em

1874	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1905; File "oct31relJ.tex"; Line 1880)
1905	\end{deff}

1880	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1909; File "oct31relJ.tex"; Line 1884)
1909	\begin{deff}\em

1884	\begin{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1919; File "oct31relJ.tex"; Line 1894)
1919	\end{deff}

1894	\end{definition}


Nonmatching lines (File "oct28relZ.tex"; Line 1923; File "oct31relJ.tex"; Line 1898)
1923	\noindent\notation Below $FAM(P)$ will denote the set of families

1898	\noindent\notationn Below $FAM(P)$ will denote the set of families


Nonmatching lines (File "oct28relZ.tex"; Line 1929:1931; File "oct31relJ.tex"; Line 1904:1906)
1929	\begin{lem}\em
1930	\label{L.fam.compl.}
1931	Every family is contracted at most once in any complete

1904	\begin{lemma}
1905	\label{L.fam.compl.}
1906	Every family is contracted at most once in a complete


Nonmatching lines (File "oct28relZ.tex"; Line 1954; File "oct31relJ.tex"; Line 1929)
1954	\end{lem}

1929	\end{lemma}


Nonmatching lines (File "oct28relZ.tex"; Line 1959; File "oct31relJ.tex"; Line 1934)
1959	\begin{thm}\em

1934	\begin{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 1981; File "oct31relJ.tex"; Line 1956)
1981	\end{thm}

1956	\end{theorem}


Nonmatching lines (File "oct28relZ.tex"; Line 2006; File "oct31relJ.tex"; Line 1981)
2006	$\reg$-minimal $\reg$-optimal semi-complete family-reduction.

1981	$\reg$-minimal $\reg$-optimal semi-complete family-reduction:


Nonmatching lines (File "oct28relZ.tex"; Line 2009:2012; File "oct31relJ.tex"; Line 1984:1987)
2009	\begin{ex}\em
2010	\label{E.ers.min.opt.}
2011	Consider the OERS $R=\{\sigma x A B\ar \delta x
2012	(((A/x)B/x)A),\,\, f(A)\ar g(A,A)\}$, and let $\reg$ be the set of terms

1984	\begin{example}
1985	\label{E.ers.min.opt.}
1986	For the OERS $R=\{\sigma x A B\ar \delta x
1987	(((A/x)B/x)A),\,\, f(A)\ar g(A,A)\}$, let $\reg$ be the set of terms


Nonmatching lines (File "oct28relZ.tex"; Line 2018; File "oct31relJ.tex"; Line 1993)
2018	left-spine redex, which do not exist in terms from $\reg$. Thus $\reg$

1993	left-spine redex, which does not exist in terms from $\reg$. Thus $\reg$


Nonmatching lines (File "oct28relZ.tex"; Line 2038; File "oct31relJ.tex"; Line 2013)
2038	\end{ex}

2013	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 2047; File "oct31relJ.tex"; Line 2022)
2047	\begin{ex}\em

2022	\begin{example}


Nonmatching lines (File "oct28relZ.tex"; Line 2077; File "oct31relJ.tex"; Line 2052)
2077	\end{ex}

2052	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 2080; File "oct31relJ.tex"; Line 2055)
2080	\begin{ex}\em

2055	\begin{example}


Nonmatching lines (File "oct28relZ.tex"; Line 2092; File "oct31relJ.tex"; Line 2067)
2092	\end{ex}

2067	\end{example}


Nonmatching lines (File "oct28relZ.tex"; Line 2109; File "oct31relJ.tex"; Line 2084)
2109	`(partial) results' should posses in order for the

2084	`(partial) results' should possess in order for the


Nonmatching lines (File "oct28relZ.tex"; Line 2161:2162; File "oct31relJ.tex"; Line 2136)
2161	%\begin{akn}
2162	\section*{Acknowledgements}

2136	\section*{Acknowledgments}


Nonmatching lines (File "oct28relZ.tex"; Line 2166:2170; File "oct31relJ.tex"; Line 2140:2141)
2166	discussions. \zurab{The annonymous referees provided valuable suggestions.}
2167	 The diagrams were drawn using P.~Taylor's diagram package.
2168	
2169	%\end{akn}
2170	

2140	discussions. The referees provided valuable suggestions.
2141	The diagrams were drawn using P.~Taylor's diagram package.


Nonmatching lines (File "oct28relZ.tex"; Line 2358:2359; File "oct31relJ.tex"; Line 2329:2330)
2358	normalization in orthogonal rewrite systems. \zurab{Information and
2359	Computation (to appear).}

2329	normalization in orthogonal rewrite systems.
2330	Information and Computation (to appear).


Nonmatching lines (File "oct28relZ.tex"; Line 2362:2364; File "oct31relJ.tex"; Line 2333:2334)
2362	
2363	\bibitem[{KP99}]{[KP99]}
2364	Khasidashvili Z., Piperno A. Normalization of typable terms by

2333	\bibitem[{KP99}]{[KP99]}
2334	Khasidashvili Z., Piperno A. Normalization of typeable terms by


Extra lines in 1st file (File "oct28relZ.tex"; Line 2492:2494; File "oct31relJ.tex"; Line 2461Æ)
2492	
2493	
2494	

*** EOF on both files ***