\documentclass[11pt,twoside]{article}	% Fontsize 11 point
\usepackage{hyperref}
\usepackage{latexsym}              	% load symbols like \Box
\bibliographystyle{plain}		% actually the vG-style is used
\textwidth    		6.5 in		% paper 8.5x11in
\textheight   		9   in          % text  6.5x 9in
\advance\textheight     -30 pt		% make space for footer
\oddsidemargin		0   pt          % 1 inch margin comes for free
\evensidemargin 	0   pt          % 1 inch margin comes for free
\topmargin      	0   pt          % 4 margins of 1in each
\headheight     	0   pt          % default 12pt = 0.42cm       
\headsep        	0   pt          % default 25pt = 0.88cm    

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			            Title		         	  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter
\def\@maketitle{%
  \newpage
  \null
  %\vskip 2em%				a bit of space removed (< 2em)
  \begin{center}%
  \let \footnote \thanks
    {\LARGE\bf \@title \par}%		\bf added
    \vskip 2em%				was: 1.5em
    {\large
      \lineskip .5em%
      \begin{tabular}[t]{c}%
        \@author
      \end{tabular}}%
    \vskip .3em%			\date and extra space removed
  \end{center}%
  \par}
\makeatother

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			Theorem-like environments			  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}
\newtheorem{obse}{Observation}

\newenvironment{definition}[1]{\begin{defi} \rm \label{df-#1} }{\end{defi}}
\newenvironment{theorem}[1]{\begin{theo} \rm \label{thm-#1} }{\end{theo}}
\newenvironment{proposition}[1]{\begin{prop} \rm \label{pr-#1} }{\end{prop}}
\newenvironment{lemma}[1]{\begin{lemm} \rm \label{lem-#1} }{\end{lemm}}
\newenvironment{corollary}[1]{\begin{coro} \rm \label{cor-#1} }{\end{coro}}
\newenvironment{example}[1]{\begin{exam} \rm \label{ex-#1} }{\end{exam}}
\newenvironment{observation}[1]{\begin{obse} \rm \label{obs-#1} }{\end{obse}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\Box$\end{trivlist}}

\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\thm}[1]{Theorem~\ref{thm-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Corollary~\ref{cor-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}
\newcommand{\obs}[1]{Observation~\ref{obs-#1}}

\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}
\newenvironment{itemise2}{\begin{list}{{\bf --}}{\leftmargin 15pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 2pt \itemsep 1pt \parsep 1pt}}{\end{list}}

\renewenvironment{abstract}{\begin{list}{}
			{\rightmargin\leftmargin
			\listparindent 1.5em
			\parsep 0pt plus 1pt}
			\small\item}{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dcup}{\stackrel{\mbox{\huge .}}{\cup}}	% disjoint union
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}}	% openface letter
\newcommand{\IT}{\mbox{\sf T\hspace{-5.5pt}T}}          % openface T (terms)
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}}	% transition
\newcommand{\gonotto}[1]{\hspace{4pt}\not\hspace{-4pt}	% no transition
	\stackrel{#1\ }{\longrightarrow}}
\newcommand{\dto}{\Longrightarrow}               	% silent transitions
\newcommand{\bis}[1]{\;\raisebox{.3ex}{$\underline	% bisimulation
{\makebox[.7em]{$\leftrightarrow$}}$}\,_{#1}\,}
\newcommand{\nobis}[1]{\mbox{$\,\not\hspace{-2.5pt}	% no bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,$}}
\newcommand{\var}{{\it var}}				% variables in a term
\newcommand{\opt}[1]{\mbox{\tiny(}#1\mbox{\tiny)}}      % optional action
\newcommand{\leftmerge}{\|\hspace{-1.06ex}\raisebox{-1.17ex}{$-$}}% left merge

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%				Abbreviations			          %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}}			        % natural numbers
\newcommand{\GL}{{\cal L}}			        % a GSOS language
\newcommand{\rel}{{\cal R}}			        % a bisimulation
\newcommand{\names}{\mathcal{N}}		        % action names in CCS

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{On Cool Congruence Formats for Weak Bisimulations\thanks{An
    extended abstract of this paper appeared in: D.V. Hung \& M. Wirsing,
    editors: Proceedings International Colloquium on Theoretical Aspects of Computing,
    ICTAC'05, Hanoi, LNCS 3722, Springer, 2005, pp. 318-333.}}
\author{R.J. van Glabbeek\\[-1pt]
 \footnotesize National ICT Australia\\[-3pt]
 \footnotesize and School of Computer Science and Engineering\\[-3pt]
 \footnotesize The University of New South Wales\\[-3pt]
 \footnotesize \tt rvg@cs.stanford.edu}

\begin{document}
\maketitle

\begin{abstract}
In TCS 146, Bard Bloom presented rule formats for four main notions of
bisimulation with silent moves. He proved that weak bisimulation
equivalence is a congruence for any process algebra defined by
\emph{WB cool rules}, and established similar results for rooted weak
bisimulation (Milner's ``observational congruence''), branching
bisimulation and rooted branching bisimulation. This study
reformulates Bloom's results in a more accessible form and contributes
analogues for (rooted) $\eta$-bisimulation and (rooted) delay
bisimulation. Moreover, finite equational axiomatisations of rooted
weak bisimulation equivalence are provided that are sound and complete
for finite processes in any RWB cool process algebra.  These require
the introduction of auxiliary operators with lookahead, and an
extension of Bloom's formats for this type of operator with lookahead.
Finally, a challenge is presented for which Bloom's formats fall short
and further improvement is called for.
\end{abstract}

\section{Introduction}

\emph{Structural Operational Semantics} \cite{Mi90ccs,Pl04} is one of
the main methods for defining the meaning of operators in system
description languages like CCS \cite{Mi90ccs}.  A system behaviour, or
\emph{process}, is represented by a closed term built from a
collection of operators, and the behaviour of a process is given by
its collection of (outgoing) transitions, each specifying the action
the process performs by taking this transition, and the process that
results after doing so. For each $n$-ary operator $f$ in the language,
a number of \emph{transition rules} are specified that generate the
transitions of a term $f(p_1,\ldots,p_n)$ from the transitions (or the
absence thereof) of its arguments $p_1,\ldots,p_n$.

For purposes of representation and verification, several behavioural
equivalence relations have been defined on processes, of which the
most well-known is \emph{strong bisimulation equivalence}
\cite{Mi90ccs}, and its variants \emph{weak} and \emph{branching}
bisimulation equivalence \cite{Mi90ccs,GW96}, that feature abstraction
from internal actions. In order to allow compositional system
verification, such equivalence relations need to be \emph{congruences}
for the operators under consideration, meaning that the equivalence
class of an $n$-ary operator $f$ applied to arguments $p_1,\ldots,p_n$
is completely determined by the equivalence classes of these
arguments.  Although strong bisimulation equivalence is a congruence
for the operators of CCS and many other languages found in the
literature, weak bisimulation equivalence fails to be a congruence for
the \emph{choice} or \emph{alternative composition} operator $+$ of
CCS\@.  To bypass this problem one uses the coarsest congruence
relation for $+$ that is finer than weak bisimulation equivalence,
characterised as \emph{rooted weak bisimulation equivalence}
\cite{Mi90ccs,BK85,vG05}, which turns out to be a minor variation of weak
bisimulation equivalence, and a congruence for all of CCS and many
other languages. Analogously, \emph{rooted branching bisimulation} is
the coarsest congruence for CCS and many other languages that is finer
than branching bisimulation equivalence \cite{GW96}.

\advance\textheight 3pt
In order to streamline the process of proving that a certain
equivalence is a congruence for certain operators, and to guide
sensible language definitions, syntactic criteria (\emph{rule
formats}) for the transition rules in structural operational semantics
have been developed, ensuring that the equivalence is a congruence for
any operator specified by rules that meet these criteria.  One of
these is the \emph{GSOS format} of {\sc Bloom, Istrail \& Meyer}
\cite{BIM95}, generalising an earlier format by {\sc De Simone}
\cite{dS85}.  When adhering to this format, all processes are
computably finitely branching, and strong bisimulation equivalence is
a congruence \cite{BIM95}. {\sc Bloom} \cite{Bl95} defines congruence
formats for (rooted) weak and branching bisimulation equivalence by
imposing additional restrictions on the GSOS format. As is customary
in this field, finer equivalences have wider formats, so Bloom's
\emph{BB cool} GSOS format, which guarantees that branching
bisimulation equivalence is a congruence, is more general than his
\emph{WB cool} GSOS format, which suits weak bisimulation equivalence;
also his \emph{RWB cool} GSOS format, suiting rooted weak
bisimulation, is more general than the WB cool GSOS format, and his
\emph{RBB cool} GSOS format, guaranteeing that rooted branching
bisimulation equivalence is a congruence, is the most general of all.
The prime motivating example for these formats is the structural
operational semantics of CCS \cite{Mi90ccs}.  All CCS operators are
RWB cool, and the CCS operators other than the + are even WB cool.
\advance\textheight -3pt

Bloom's formats involve a fast bookkeeping effort of names of
variables, used to precisely formulate the \emph{bifurcation rules}
that his formats require. To make his work more accessible, Bloom also
presents simpler but less general versions of his formats, obtained by
imposing an additional syntactic restriction.  This restriction makes
it possible to simplify the bifurcation rules to \mbox{\emph{patience
rules}}, which do not require such an extensive bookkeeping. {\sc
Fokkink} \cite{Fok00b} generalises Bloom's \mbox{\emph{simply RBB cool}}
format to a format he calls \emph{RBB safe}, and writes ``The
definition of bifurcation rules is deplorably complicated, and we do
not know of any examples from the literature that are RBB cool but not
simply RBB cool. Therefore, we refrain from this generalisation
here.'' {\sc Ulidowski} \cite{Ul92,UP02,UY00} studies congruence
formats for variations of the semantic equivalences mentioned above
with a different treatment of divergence.  Ulidowski's formats form
the counterparts of Bloom's simply cool formats only.

The main aim of the present study is to simplify and further clarify
Bloom's work, so as to make it more accessible for the development of
applications, variations and extensions.  In passing, analogous
results are obtained for two equivalences, and their rooted variants,
that bridge the gap between weak and branching bisimulation.
Moreover, the method of {\sc Aceto, Bloom \& Vaandrager} \cite{ABV94}
to extract from any GSOS language a finite equational axiomatisation
that is sound and complete for strong bisimulation equivalence on
finite processes, is adapted to rooted weak bisimulation equivalence.
In the construction fresh function symbols may need to be added whose
transition rules have \emph{lookahead} and thereby fall outside the
GSOS format. To this end, I extend the RWB cool format with a form of
lookahead.

One of the simplifications of Bloom's formats presented here stems
from the observation that the operators in any of the cool formats can
be partitioned in \emph{principal operators} and \emph{abbreviations},
such that the abbreviations can be regarded as syntactic sugar, adding
nothing that could not be expressed with principal operators. For any
abbreviation $f$ there exists a principal operator $f^\star$ that
typically takes more arguments. For instance, $f(x_1,x_2)$ could be an
abbreviation of $f^\star(x_1,x_1,x_2)$. The rules for the
abbreviations are completely determined by the rules for the principal
operators, and for principal operators patience rules suffice, i.e.\
one does not need the full generality of bifurcation rules.  Moreover,
the simply cool formats can be characterised by the requirement that
all operators are principal. These observations make it possible to
define the cool formats of Bloom without mentioning bifurcation rules
altogether. It also enables a drastic simplification of the congruence
proofs, namely by establishing the congruence results for the simply
cool formats first, and reducing the general case to the simple case
by means of some general insights in abbreviation expansion. 

In fact, I will present a general algorithm that given any rule format,
guaranteeing that a certain equivalence, coarser than or equal to
strong bisimulation equivalence, is a congruence, extends this format
with a mechanism for abbreviation expansion. Bloom's general formats
can then be obtained by applying this algorithm to his simple formats.

Even though any operation that fits the cool formats can also be
defined using merely the simply cool formats, in practice it may be
handy to work with the full generality of the cool formats. The unary
copying operator $\sf cp$ of \cite{BIM95} (page 257) for instance does
not fit the cool formats directly, but can be made to fit by adding an
auxiliary binary copying operator to the language, of which the unary
one is an abbreviation. Dumping the abbreviation from the language
would appear unnatural here, as the unary operator motivates the rules
for both itself and its binary expansion, the latter being needed
merely to make it work.

Another simplification contributed here is in the description of the
RWB cool format.  Bloom requires for every operational rule with
target $t$ the existence of two terms $t_1$ and $t_2$, and seven types
of derived operational rules. I show that without limitation of
generality it is always possible to choose $t_2=t$, thereby making
four of those seven types of rules redundant. Thus, the same format is
obtained by requiring only $t_1$ and two types of derived rules (the
third being a bifurcation rule, that was already required for its own sake).

After defining the basic concepts in Section~\ref{preliminaries}, I
present the congruence proofs for the simply cool languages in
Section~\ref{proofs}.  To that end, I first prove the result from
\cite{BIM95} that strong bisimulation equivalence is a congruence for
all GSOS operators.  Then I change this proof in minimal ways so as to
obtain the congruence results for the simply cool languages. In doing
so, for each simply cool format I state a lemma that tells exactly
what is needed to make the congruence proof work. Section~\ref{simply
cool} defines the simply cool formats for the unrooted case, in such a
way that the lemmas hold.  As an example I show a version of the
language CSP \cite{BHR84,OH86} to be simply WB cool, implying that
weak and branching bisimulation equivalence are congruences on this
language.  Section~\ref{cool} presents the theory of abbreviations
that lifts the results from the simple to the general congruence
formats, and Section~\ref{rooted} deals with the rooted congruence
formats. Section~\ref{Bloom} compares my definitions of the cool
formats with the ones of Bloom.  In Section~\ref{lookahead} I
generalise the RWB cool format to what I call \emph{GSOS languages
with lookahead}.  Section~\ref{sec-equations} recapitulates the method
of \cite{ABV94} to provide finite equational axiomatisations of strong
bisimulation equivalence that are sound and complete for finite
processes on an augmentation of any given GSOS language, and
Section~\ref{sec-cool-equations} extends this work to the rooted weak
equivalences. Section~\ref{further} discusses extensions of Bloom's
formats that occur in the literature.  Finally,
Section~\ref{challenge} presents a fairly intuitive GSOS language for
which the existing congruence formats fall short and further
improvement is called for.\vspace{-1em}

\paragraph{Acknowledgements.} My thanks to Simone Tini for inspiration,
and to the referees for their proposals of improvements in presentation.

\section{Preliminaries}\label{preliminaries}

In this paper $V=\{x_1, x_2, \dots \}$ and $Act$ are two sets of {\em
  variables} and {\em actions}.

\begin{definition}{signature}
A {\em signature} is a collection $\Sigma$ of {\em function symbols}
$f \not\in V$ equipped with a function $ar: \Sigma \rightarrow \IN$.
The set $\IT(\Sigma)$ of {\em terms} over a signature $\Sigma$ is
defined recursively by:
\begin{itemise}
\item $V \subseteq \IT(\Sigma)$,
\item if $f \in \Sigma$ and $t_1,\ldots,t_{ar(f)} \in
\IT(\Sigma)$ then $f(t_1,\ldots,t_{ar(f)}) \in \IT(\Sigma)$.
\end{itemise}
A term $c()$ is abbreviated as $c$.  For $t\in \IT(\Sigma)$,
$\var(t)$ denotes the set of variables that occur in $t$.
$T(\Sigma)$ is the set of closed terms over $\Sigma$, i.e.\
the terms $p \in \IT(\Sigma)$ with $\var(p)=\emptyset$.
A {\em $\Sigma$-substitution} $\sigma$ is a partial function from $V$
to $\IT(\Sigma)$. If $\sigma$ is a substitution and $S$ is any syntactic
object, then $\sigma(S)$ denotes the object obtained from $S$ by
replacing, for $x$ in the domain of $\sigma$, every occurrence of $x$
in $S$ by $\sigma(x)$. In that case $\sigma(S)$ is called a {\em
substitution instance} of $S$. A $\Sigma$-substitution is {\em closed} if
it is a total function from $V$ to $T(\Sigma)$.
\end{definition}

\begin{definition}{TSS}
Let $\Sigma$ be a signature. A {\em positive $\Sigma$-literal} is an
expression $t \goto{a} t'$ and a {\em negative $\Sigma$-literal} an
expression $t \gonotto{a}$ with $t,t'\in \IT(\Sigma)$ and $a \in Act$.
A {\em transition rule} over $\Sigma$ is an expression of the form
$\frac{H}{\alpha}$ with $H$ a set of $\Sigma$-literals (the {\em
premises} of the rule) and $\alpha$ a positive $\Sigma$-literal (the
{\em conclusion}). The left- and right-hand side of $\alpha$ are
called the {\em source} and the {\em target} of the rule,
respectively. A rule $\frac{H}{\alpha}$ with $H=\emptyset$ is also
written $\alpha$.  A \emph{transition system specification}
(\emph{TSS}), written $(\Sigma,R)$, consists of a signature $\Sigma$
and a collection $R$ of transition rules over $\Sigma$.  A TSS is {\em
positive} if the premises of its rules are positive.
\end{definition}

\begin{definition}{GSOS}\cite{BIM95}
A \emph{GSOS} rule is a transition rule such that
\begin{itemise}
\item its source has the form $f(x_1,\ldots,x_{ar(f)})$ with $f\in
 \Sigma$ and $x_i \in V$,
\item the left-hand sides of its premises are variables $x_i$ with
  $1\leq i\leq ar(f)$,
\item the right-hand sides of its positive premises are variables that
  that are all distinct, and that do not occur in its source,
\item its target only contains variables that also occur in its source
  or premises.
\end{itemise}
A \emph{GSOS language}, or TSS in GSOS format, is a TSS whose rules
are GSOS rules.
\end{definition}

\begin{definition}{transition}
A \emph{transition} over a signature $\Sigma$ is a closed positive
$\Sigma$-literal.  With structural recursion on $p$ one defines when a
GSOS language $\GL$ generates a transition $p\goto{a}p'$ (notation
$p\goto{a}_\GL p'$):\vspace{4pt}

$f(p_1,\ldots,p_n)\goto{a}_\GL q$ iff $\GL$ has a transition rule
$\frac{H}{f(x_1,...,x_n)\goto{a}t}$ and there is a closed substitution
$\sigma$ with $\sigma(x_i)=p_i$ for $i=1,...,n$ and $\sigma(t)=q$,
such that $p_i\goto{c}_\GL\sigma(y)$ for $(x_i\goto{c}y)\in H$ and
$\neg\exists r(p_i\goto{c}_\GL r)$ for $(x_i\gonotto{c})\in H$.
\end{definition}
Henceforth a GSOS language $\GL$ over a signature $\Sigma$ is assumed,
and closed $\Sigma$-terms will be called \emph{processes}. The
subscript $\GL$ will often be suppressed.  Moreover, $Act=A\dcup\{\tau\}$
with $\tau$ the \emph{silent move} or \emph{hidden action}.

\begin{definition}{bisimulation}
Two processes $t$ and $u$ are {\em weak bisimulation equivalent} or
{\em weakly bisimilar} ($t \bis{w} u$) if $t\rel u$ for a symmetric
binary relation $\rel$ on processes (a \emph{weak bisimulation})
satisfying, for $a\in Act$,
\begin{center}\hfill
if $p\rel q$ and $p \goto{a} p'$ then there are $q_1, q_2, q'$ such
that $q\dto q_1\goto{\opt{a}}q_2\dto q'$ and $p' \rel q'$.
\hfill(*)
\end{center}
Here $p \dto p'$ abbreviates $p=p_0 \goto{\tau} p_1 \goto{\tau} \cdots
\goto{\tau} p_n = p'$ for some $n\geq 0$, whereas
$p\goto{\opt{a}}p'$ abbreviates $(p\goto{a}p') \vee
(a=\tau\wedge p=p')$.

$t$ and $u$ are {\em $\eta$-bisimilar} ($t \bis{\eta} u$) if in (*)
one additionally requires $p \rel q_1$;

$t$ and $u$ are {\em delay bisimilar} ($t \bis{d} u$) if in (*)
one additionally requires $q_2=q'$;

$t$ and $u$ are {\em branching bisimilar} ($t \bis{b} u$) if in (*)
one requires both $p \rel q_1$ and $q_2=q'$;

$t$ and $u$  are {\em strongly bisimilar} ($t \bis{} u$) if in (*) one
simply requires $q\goto{a}q'$.
\\
Two processes $t$ and $u$ are {\em rooted weak bisimulation
equivalent} ($t \bis{rw} u$), if they satisfy
\begin{center}\vspace{-1pt}
\begin{tabular}{@{}l@{}}
if $t \goto{a} t'$ then there are $u_1, u_2, u$ such
that $u\dto u_1\goto{a}u_2\dto u'$ and $t' \bis{w}
u'$, and\\
if $u \goto{a} u'$ then there are $t_1, t_2, t$ such
that $t\dto t_1\goto{a}t_2\dto t'$ and $t' \bis{w} u'$.
\end{tabular}\vspace{-1pt}
\end{center}
They are {\em rooted $\eta$-bisimilar} ($t \bis{r\eta} u$) if above
one additionally requires $u_1=u$, $t_1=t$, and $t'\bis{\eta}u'$, they
are {\em rooted delay bisimilar} ($t \bis{rd} u$) if one requires
$u_2=u'$, $t_2=t'$ and $t'\bis{d}u'$, and they are {\em rooted
branching bisimilar} ($t \bis{rb} u$) if one requires $u_1=u$,
$u_2=u'$, $t_1=t$, $t_2=t'$ and $t'\bis{b}u'$.
\end{definition}
It is well known and easy to check that the nine relations on
processes defined above are equivalence relations indeed
\cite{Bas96,GW96}, and that, for $x \in \{$weak, $\eta$, delay,
branching, strong$\}$, $x$-bisimulation equivalence is the largest
$x$-bisimulation relation on processes \cite{Mi90ccs,BK85,vG05,GW96}.
Moreover, $p\bis{rx}q$ implies $p\bis{x}q$.

\begin{definition}{congruence}
An equivalence relation $\sim$ on processes is a \emph{congruence} if
for all $f\in\Sigma$
$$p_i \sim q_i \mbox{ for } i=1,\dots,ar(f) ~~\Rightarrow~~
f(p_1,\ldots,p_{ar(f)})\sim f(q_1,\ldots,q_{ar(f)}).$$
\end{definition}
This is equivalent to the requirement that for all $t \in \IT(\Sigma)$
and closed substitutions $\sigma, \nu: V \rightarrow T(\Sigma)$
$$\sigma(x) = \nu(x) \mbox{ for } x\in \var(t)
~~\Rightarrow~~ \sigma(t) = \nu(t).$$
This note, and {\sc Bloom} \cite{Bl95}, deal with syntactic conditions
on GSOS languages that guarantee that the equivalence notions of
\df{bisimulation} are congruences.

\section{The congruence proofs for the simply cool rule formats}\label{proofs}

In this section I first prove the result from \cite{BIM95} that strong
bisimulation equivalence is a congruence for all GSOS operators.  Then
I change this proof in minimal ways so as to obtain the congruence
results for the simply cool GSOS languages. In doing so, for each simply
cool GSOS format I state a lemma that tells exactly what is needed to make
the congruence proof work. Later on, the simply cool congruence
formats will be defined in such a way that these lemmas hold.

\begin{theorem}{strong}\cite{BIM95}
On any GSOS language, strong bisimulation equivalence is a congruence.
\end{theorem}

\begin{proof}
Let $\rel$ be the smallest relation on processes satisfying
\begin{itemise} 
\item if $p \bis{} q$ then $p \rel q$, and
\item if $p_i \rel q_i \mbox{ for } i=1,\ldots,ar(f)$ then
      $f(p_1,\ldots,p_{ar(f)})\rel f(q_1,\ldots,q_{ar(f)})$.
\end{itemise}
It suffices to show that $\rel$ is a strong bisimulation, because this
implies that $\rel$ equals $\bis{}$, and by construction $\rel$ is a
congruence. Because $\bis{}$ is symmetric, so is $\rel$. So it remains
to show that
\begin{center}
if $p\rel q$ and $p \goto{a} p'$, with $a\in Act$, then there is a
$q'$ such that $q\goto{a}q'$ and $p' \rel q'$.
\end{center}
This I will do with induction on the number of applications of the second
clause in the definition of $\rel$ above in establishing that $p\rel q$.
Note that this number is the same for $q\rel p$.

{\em Base case:} Let $p\bis{} q$ and $p\goto{a} p'$. Using that
$\bis{}$ is a strong bisimulation, there must be a process $q'$ such
that $q \goto{a}q'$ and $p'\bis{}q'$, hence $p' \rel q'$.

{\em Induction step:} Let $p=f(p_1,\ldots,p_n)$ and
$q=f(q_1,\ldots,q_n)$ where $p_i \rel q_i$ for $i=1,\ldots,n$, and
$p_i \rel q_i$ is established in less
applications of the second step than $p\rel q$. By induction, one may assume
\begin{eqnarray}
\mbox{if $p_i \goto{c} p'$ then there is a $q'$ such
that $q_i\goto{c} q'$ and $p' \rel q'$}\label{transfer1}
\\
\mbox{if $q_i \goto{c} q'$ then there is a $p'$ such
that $p_i\goto{c} p'$ and $p' \rel q'$}\label{transfer2}
\end{eqnarray}
for $i = 1,...,n$ and $c\in Act$.
Let $p\goto{a}p'$.  By \df{transition}, there must be a rule
$\frac{H}{f(x_1,...,x_n)\goto{a}t}$ in $\GL$ and a closed substitution
$\sigma$ with $\sigma(x_i)=p_i$ for $i=1,...,n$ and $\sigma(t)=p'$,
such that $p_i\goto{c}\sigma(y)$ for $(x_i\goto{c}y)\in H$ and
$\neg\exists r(p_i\goto{c} r)$ for $(x_i\gonotto{c})\in H$.

For $(x_i\goto{c}y)\in H$, using that $p_i\goto{c}\sigma(y)$, by
(\ref{transfer1}) there is a $q_y$ such that $q_i\goto{c}q_y$ and
$\sigma(y)\rel q_y$.

For $(x_i\gonotto{c})\in H$, using that $\neg\exists r(p_i\goto{c}r)$,
by (\ref{transfer2}) there can not be a $s\in T(\Sigma)$ with $q_i\goto{c}s$.
Let $\nu$ be a substitution with $\nu(x_i)=q_i$ for
$i=1,\ldots,n$ and $\nu(y)=q_y$ if $y$ is the right-hand side of a
premise in $H$, taking $\nu(z)=\sigma(z)$ for all other variables $z$;
by the third clause of \df{GSOS} such a substitution $\nu$ does
indeed exist. I now have $\sigma(x)\rel \nu(x)$ for all $x\in V$,
and hence $\sigma(t)\rel\nu(t)$ by the definition of $\rel$.
Take $q'=\nu(t)$. So $p'\rel q'$.
Moreover, $q_i\goto{c}\nu(y)$ for $(x_i\goto{c}y)\in H$ and
$\neg\exists r(q_i\goto{c} r)$ for $(x_i\gonotto{c})\in H$.  Thus, by
\df{transition}, $q=f(q_1,\ldots,q_n) \goto{a} \nu(t)=q'$.
\end{proof}
In Sections~\ref{simply cool} and~\ref{rooted} I define 8 simply cool
formats in such a way that the following theorem holds.

\begin{theorem}{simply cool}
On any simply WB cool GSOS language, $\bis{w}$ is a congruence.

On any simply RWB cool GSOS language, $\bis{rw}$ is a congruence.

On any simply DB cool GSOS language, $\bis{d}$ is a congruence.

On any simply RDB cool GSOS language, $\bis{rd}$ is a congruence.

On any simply HB cool GSOS language, $\bis{\eta}$ is a congruence.

On any simply RHB cool GSOS language, $\bis{r\eta}$ is a congruence.

On any simply BB cool GSOS language, $\bis{b}$ is a congruence.

On any simply RBB cool GSOS language, $\bis{rb}$ is a congruence.
\end{theorem}
The proofs are simple variations of the proof of \thm{strong} that
merely require the following lemmas.  These lemmas could have been
taken as definitions of the simply cool rule formats, albeit not very
syntactic ones. The real definitions will consist of the simplest
syntactic requirements that guarantee these lemmas to hold.  For now,
all one needs to know about the cool formats is that
\begin{itemise}
\item (simply) WB, RWB, DB, RDB, HB and BB cool GSOS languages are
  required to be positive---hence  one doesn't need a counterpart of
  equation (\ref{transfer2}) above,
\item the targets of all rules in simply RXB languages
  (X$\in\{$W,D,H,B$\}$) belong to a simply XB cool sublanguage,
\item the simply XB cool languages only have rules of the form
  \plat{\frac{\{x_i \goto{c_i} y_i\mid i\in I\}}
  {f(x_1,\ldots,x_n)\goto{a}t}$ for $I\subseteq \{1,\ldots,n\}}.
\end{itemise}\vspace{7pt}
I write $p \dto\goto{a} p'$ for $\exists p^{pre} (p \dto p^{pre} \goto{a} p')$,
and similarly for other relation compositions.

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma WB]
Let $\GL$ be simply WB cool, let $\frac{H}{s\goto{a}t}$ be a rule in $\GL$,
and let $\nu$ be a closed substitution.
If for each premise $x\goto{c}y$ in $H$ one has
$\nu(x)\dto \goto{\opt{c}} \dto \nu(y)$, then
$\nu(s)\dto \goto{\opt{a}} \dto \nu(t)$.
\end{trivlist}

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma RWB]
Let $\GL$ be simply RWB cool, let $\frac{H}{s\goto{a}t}$ be a rule in
$\GL$, and let $\nu$ be a closed substitution.
If for each premise $x\goto{c}y$ in $H$ one has
$\nu(x)\dto \goto{{c}} \dto \nu(y)$, then
$\nu(s)\dto \goto{{a}} \dto \nu(t)$.
\end{trivlist}

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma DB]
Let $\GL$ be simply DB cool, let $\frac{H}{s\goto{a}t}$ be a rule in $\GL$,
and let $\nu$ be a closed substitution.
If for each premise $x\goto{c}y$ in $H$ one has
$\nu(x)\dto \goto{\opt{c}} \nu(y)$, then
$\nu(s)\dto \goto{\opt{a}} \nu(t)$.
\end{trivlist}

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma RDB]
Let $\GL$ be simply RDB cool, let $\frac{H}{s\goto{a}t}$ be a rule in
$\GL$, and let $\nu$ be a closed substitution.
If for each premise $x\goto{c}y$ in $H$ one has
$\nu(x)\dto \goto{{c}} \nu(y)$, then
$\nu(s)\dto \goto{{a}} \nu(t)$.
\end{trivlist}

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma HB]
Let $\GL$ be simply HB cool, let $\frac{\{x_i \goto{c_i} y_i\mid i\in I\}}
{f(x_1,\ldots,x_n)\goto{a}t}$ be a rule in $\GL$, and let $\rho,\nu$
be closed substitutions satisfying $\rho(x_i)\dto \nu(x_i) \goto{\opt{c_i}}
\dto \nu(y_i)$ for $i\!\in\! I$ and $\rho(x_i)=\nu(x_i)$ for $i\!\not\in\! I$.
Then $\rho(f(x_1,...,x_n))\dto \nu(f(x_1,...,x_n)) \goto{\opt{a}} \dto \nu(t)$.
\end{trivlist}

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma RHB]
Let $\GL$ be simply RHB cool, let $\frac{H}{s\goto{a}t}$ be a rule in
$\GL$, and let $\nu$ be a closed substitution such that
$\nu(x) \goto{{c}} \dto \nu(y)$ for each positive premise $x\goto{c}y$ in $H$
and $\neg\exists r\, (\nu(x) \gonotto{c} r)$ for each negative premise
$x\gonotto{c}$ in $H$. Then $\nu(s) \goto{{a}} \dto \nu(t)$.
\end{trivlist}

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma BB]
Let $\GL$ be simply BB cool, let $\frac{\{x_i \goto{c_i} y_i\mid i\in I\}}
{f(x_1,\ldots,x_n)\goto{a}t}$ be a rule in $\GL$, and let $\rho,\nu$
be closed substitutions satisfying $\rho(x_i)\dto \nu(x_i) \goto{\opt{c_i}}
\nu(y_i)$ for $i\!\in\! I$ and $\rho(x_i)=\nu(x_i)$ for $i\!\not\in\! I$.
Then $\rho(f(x_1,...,x_n))\dto \nu(f(x_1,...,x_n)) \goto{\opt{a}} \nu(t)$.
\end{trivlist}

\begin{trivlist} \item[\hspace{\labelsep}\bf Lemma RBB]
Let $\GL$ be simply RBB cool, let $\frac{H}{s\goto{a}t}$ be a rule in
$\GL$, and let $\nu$ be a closed substitution such that
$\nu(x) \goto{{c}} \nu(y)$ for each positive premise $x\goto{c}y$ in $H$
and $\neg\exists r\, (\nu(x) \gonotto{c} r)$ for each negative premise
$x\gonotto{c}$ in $H$.  Then $\nu(s) \goto{{a}} \nu(t)$.
\end{trivlist}
By \df{transition}, the last lemma holds trivially. The others will be
obtained in Sections~\ref{simply cool} and~\ref{rooted}. With these
lemmas the proof of \thm{simply cool} is easy. I will only present the
representative cases of (rooted) weak and branching bisimulation
equivalence.

\begin{trivlist} \item[\hspace{\labelsep}\bf \thm{simply cool}WB]
On any simply WB cool GSOS language, $\bis{w}$ is a congruence.
\end{trivlist}

\begin{proof}
Let $\rel$ be the smallest relation on processes satisfying
\begin{itemise} 
\item if $p \bis{w} q$ then $p \rel q$, and
\item if $p_i \rel q_i \mbox{ for } i=1,\ldots,ar(f)$ then
      $f(p_1,\ldots,p_{ar(f)})\rel f(q_1,\ldots,q_{ar(f)})$.
\end{itemise}
It suffices to show that $\rel$ is a weak bisimulation, because this
implies that $\rel$ equals $\bis{w}$, and by construction $\rel$ is a
congruence. Because $\bis{w}$ is symmetric, so is $\rel$. So it remains
to show that
\begin{center}
if $p\rel q$ and $p \goto{a} p'$, then there is a $q'$ such
that \plat{q\dto \goto{\opt{a}}\dto q'} and $p' \rel q'$.
\end{center}
This I will do with induction on the number of applications of the second
clause in the definition of $\rel$ above in establishing $p\rel q$.

{\em Base case:} Let $p\bis{w} q$ and $p\goto{a} p'$. Using that
$\bis{w}$ is a weak bisimulation, there must be a process $q'$ such
that \plat{q\dto\goto{\opt{a}}\dto q'} and $p'\bis{w}q'$, hence $p'\rel q'$.

{\em Induction step:} Let $p=f(p_1,\ldots,p_n)$ and
$q=f(q_1,\ldots,q_n)$ where $p_i \rel q_i$ for $i=1,\ldots,n$, and
$p_i \rel q_i$ is established in less applications of the second step
than $p\rel q$. By induction, one may assume
\begin{equation}
\mbox{if $p_i \goto{c_i} p'_i$ then there is a $q'_i$ such that
\plat{q_i\dto \goto{\opt{c_i}}\dto q'_i} and $p'_i\rel q'_i$}\label{Wtransfer}
\end{equation}
for $i=1,...,n$ and $c_i\in Act$.  Let $p\goto{a}p'$.  By
\df{transition}, there must be a rule $\frac{\{x_i \goto{c_i} y_i\mid
i\in I\}} {f(x_1,...,x_n)\goto{a}t}$ in $\GL$ and a closed
substitution $\sigma$ with $\sigma(x_i)=p_i$ for $i=1,\dots,n$ and
$\sigma(t)=p'$, such that $p_i\goto{c_i}\sigma(y_i)$ for $i\!\in\!I$.
So by (\ref{Wtransfer}), for $i\!\in\!I$ there is a $q'_i$ such
that \plat{q_i\dto\goto{\opt{c_i}}\dto q'_i} and $\sigma(y_i)\rel q'_i$.
Let $\nu$ be a substitution with $\nu(x_i)=q_i$ for $i=1,\ldots,n$ and
$\nu(y_i)=q'_i$ for $i\in I$, taking $\nu(z)=\sigma(z)$ for all other
variables $z$. I now have $\sigma(x)\rel \nu(x)$ for all $x\in V$, and
hence $\sigma(t)\rel\nu(t)$ by the definition of $\rel$.
Take $q'=\nu(t)$. Then $p'\rel q'$.
Moreover, \plat{\nu(x_i)\dto\goto{\opt{c_i}}\dto\nu(y_i)} for each
$i\!\in\!I$. Thus, by Lemma~WB,
\plat{q=\nu(f(x_1,\ldots,x_n))\dto\goto{\opt{a}}\dto\nu(t)=q'}.
\end{proof}

\begin{trivlist} \item[\hspace{\labelsep}\bf \thm{simply cool}RWB]
On any simply RWB cool GSOS language, $\bis{rw}$ is a congruence.
\end{trivlist}

\begin{proof}
Let $f$ be an operator of arity $n$, and let $p_i \bis{rw} q_i$ for
$i=1,\ldots,n$.  I have to show that
$f(p_1,\ldots,p_n)\bis{rw}f(q_1,\ldots,q_n)$.  Let
$f(p_1,\ldots,p_n)\goto{a}p'$.  By \df{transition}, there must be a
rule $\frac{H}{f(x_1,...,x_n)\goto{a}t}$ in $\GL$ and a closed
substitution $\sigma$ with $\sigma(x_i)=p_i$ for $i=1,...,n$ and
$\sigma(t)=p'$, such that $p_i\goto{c}\sigma(y)$ for
$(x_i\goto{c}y)\in H$.  For any $(x_i\goto{c}y)\in H$, using that
$p_i\bis{rw}q_i$, there is a $q_y$ such that \plat{q_i\dto\goto{c}\dto
q_y} and $\sigma(y)\bis{w} q_y$.  Let $\nu$ be a substitution with
$\nu(x_i)=q_i$ for $i=1,\ldots,n$ and $\nu(y)=q_y$ if $y$ is the
right-hand side of a premise in $H$, taking $\nu(z)=\sigma(z)$ for all
other variables $z$; by the last clause of \df{GSOS} such a
substitution $\nu$ does indeed exist. I now have $\sigma(x)\bis{w}
\nu(x)$ for all $x\in V$, and hence $\sigma(t)\bis{w}\nu(t)$ by
\thm{simply cool}WB\@.  Take $q'=\nu(t)$. So $p'\bis{w} q'$.
Moreover, \plat{\nu(x_i)\dto\goto{c}\dto\nu(y)} for each premise
$(x_i\goto{c}y)\in H$. Thus, by Lemma~RWB,
\plat{f(q_1,\ldots,q_n)=\nu(f(x_1,\ldots,x_n))\dto\goto{a}\dto\nu(t)=q'}.

The case assuming $f(q_1,\ldots,q_n)\goto{a}q'$ follows by symmetry.
\end{proof}

\begin{trivlist} \item[\hspace{\labelsep}\bf \thm{simply cool}BB]
On any simply BB cool GSOS language, $\bis{b}$ is a congruence.
\end{trivlist}

\begin{proof}
Let $\rel$ be the smallest relation on processes satisfying
\begin{itemise} 
\item if $p \bis{b} q$ then $p \rel q$, and
\item if $p_i \rel q_i \mbox{ for } i=1,\ldots,ar(f)$ then
      $f(p_1,\ldots,p_{ar(f)})\rel f(q_1,\ldots,q_{ar(f)})$.
\end{itemise}
It suffices to show that $\rel$ is a branching bisimulation, because this
implies that $\rel$ equals $\bis{b}$, and by construction $\rel$ is a
congruence. Because $\bis{b}$ is symmetric, so is $\rel$. So it remains
to show that
\begin{center}
if $p\rel q$ and $p \goto{a} p'$ then there are $q^{pre}, q'$ such
that $q\dto q^{pre}\goto{\opt{a}} q'$, $p \rel q^{pre}$ and $p' \rel q'$.
\end{center}
This I will do with induction on the number of applications of the second
clause in the definition of $\rel$ above in establishing $p\rel q$.

{\em Base case:} Let $p\bis{b} q$ and $p\goto{a} p'$. Using that
$\bis{b}$ is a branching bisimulation, there must be processes
$q^{pre},q'$ such that \plat{q \dto q^{pre}\goto{\opt{a}} q'},
$p\bis{b}q^{pre}$ and $p'\bis{b}q'$, hence $p \rel q^{pre}$ and $p' \rel q'$.

{\em Induction step:} Let $p=f(p_1,\ldots,p_n)$ and
$q=f(q_1,\ldots,q_n)$ where $p_i \rel q_i$ for $i=1,\ldots,n$, and
$p_i \rel q_i$ is established in less applications of the second step
than $p\rel q$. By induction, one may assume
\begin{equation}\label{Btransfer}
\mbox{if $p_i \goto{c_i} p'_i$ then there are $q^{pre}_i, q'_i$ such that
$q_i\dto q^{pre}_i\goto{\opt{c_i}} q'_i$, $p_i \rel q^{pre}_i$ and
$p'_i \rel q'_i$}
\end{equation}
for $i=1,...,n$ and $c_i\in Act$.  Let $p\goto{a}p'$.  By
\df{transition}, there must be a rule $\frac{\{x_i \goto{c_i} y_i\mid
i\in I\}} {f(x_1,...,x_n)\goto{a}t}$ in $\GL$ and a closed
substitution $\sigma$ with $\sigma(x_i)=p_i$ for $i=1,\dots,n$ and
$\sigma(t)=p'$, such that $p_i\goto{c_i}\sigma(y_i)$ for $i\!\in\!I$.
So by (\ref{Btransfer}), for $i\!\in\!I$ there are $q^{pre}_i,q'_i$
such that \plat{q_i\dto q^{pre}_i\goto{\opt{c_i}}q'_i}, $p_i\rel
q^{pre}_i$ and $\sigma(y_i)\rel q'_i$. Let $\nu$ be a substitution
with $\nu(x_i)=q^{pre}_i$ and $\nu(y_i)=q'_i$ for $i\!\in\!I$ and
$\nu(x_i)=q_i$ for $i\!\not\in\!I$, taking $\nu(z)=\sigma(z)$ for all
other variables $z$. I now have $\sigma(x)\rel \nu(x)$ for all $x\in
V$, and hence $\sigma(t)\rel\nu(t)$ and
$\sigma(f(x_1,\ldots,x_n)\rel\nu(f(x_1,\ldots,x_n)$ by the definition
of $\rel$.  Take $q^{pre}=\nu(f(x_1,\ldots,x_n))$ and $q'=\nu(t)$.  So
$p\rel q^{pre}$ and $p'\rel q'$.  Moreover,
\plat{q_i\dto\nu(x_i)\goto{\opt{c_i}}\nu(y)} for each
$i\!\in\!I$. Thus Lemma~BB, taking $\rho$ to be a closed substitution
with $\rho(x_i)=q_i$, yields \plat{q\dto q^{pre}\goto{\opt{a}}q'}.
\end{proof}

\begin{trivlist} \item[\hspace{\labelsep}\bf \thm{simply cool}RBB]
On any simply RBB cool GSOS language, $\bis{rb}$ is a congruence.
\end{trivlist}

\begin{proof}
Let $f$ be an operator of arity $n$, and let $p_i \bis{rb} q_i$ for
$i=1,\ldots,n$.  I have to show that
$f(p_1,\ldots,p_n)\bis{rb}f(q_1,\ldots,q_n)$.  Let
$f(p_1,\ldots,p_n)\goto{a}p'$.  By \df{transition}, there must be a
rule $\frac{H}{f(x_1,...,x_n)\goto{a}t}$ in $\GL$ and a closed
substitution $\sigma$ with $\sigma(x_i)=p_i$ for $i=1,...,n$ and
$\sigma(t)=p'$, such that $p_i\goto{c}\sigma(y)$ for
$(x_i\goto{c}y)\in H$ and $\neg\exists r(p_i\goto{c} r)$ for
$(x_i\gonotto{c})\in H$.

For any $(x_i\goto{c}y)\in H$, using that $p_i\bis{rb}q_i$, there is a
$q_y$ such that \plat{q_i\goto{c}q_y} and $\sigma(y)\bis{b} q_y$.

For any $(x_i\gonotto{c})\in H$, using that $p_i\bis{rb}q_i$,
there can not be a $s\in T(\Sigma)$ with $q_i\goto{c}s$.
\\
Let $\nu$ be a substitution with $\nu(x_i)=q_i$ for $i=1,\ldots,n$ and
$\nu(y)=q_y$ if $y$ is the right-hand side of a premise in $H$, taking
$\nu(z)=\sigma(z)$ for all other variables $z$; by the last clause of
\df{GSOS} such a substitution $\nu$ does indeed exist. I now have
$\sigma(x)\bis{b} \nu(x)$ for all $x\in V$, and hence
$\sigma(t)\bis{b}\nu(t)$ by \thm{simply cool}BB\@.  Take $q'=\nu(t)$.
So $p'\bis{b} q'$.  Moreover, \plat{\nu(x_i)\goto{c}\nu(y)} for each
premise $x_i\goto{c}y$ in $H$ and $\neg\exists r(\nu(x_i)\goto{c} r)$
for each premise $x_i\gonotto{c}$ in $H$. Thus, by Lemma~RBB, or
\df{transition},
\plat{f(q_1,\ldots,q_n)=\nu(f(x_1,\ldots,x_n))\goto{a}\nu(t)=q'}.

The case assuming $f(q_1,\ldots,q_n)\goto{a}q'$ follows by symmetry.
\end{proof}

\section{Simply cool GSOS languages}\label{simply cool}

In this section I will define the simply XB cool rule formats
(X$\in\{$W,D,H,B$\}$) and show that they satisfy Lemma XB\@.
Let $\GL$ be a positive GSOS language.

\begin{definition}{straight}
For an operator $f$ in $\GL$, the \emph{rules of $f$}
are the rules in $\GL$ with source $f(x_1,...,x_{ar(f)})$.
\begin{itemise}
\item An operator in $\GL$ is \emph{straight} if it has no rules in
  which a variable occurs multiple times in the left-hand side of
  its premises.  A operator is \emph{smooth} if moreover it has no
  rules in which a variable occurs both in the target and in the
  left-hand side of a premise.
\item An argument $i\in\IN$ of an operator $f$ is \emph{active} if
  $f$ has a rule in which $x_i$ appears as left-hand side of a premise.
\item A variable $x$ occurring in a term $t$ is \emph{receiving} in
  $t$ if $t$ is the target of a rule in $\GL$ in which $x$ is the
  right-hand side of a premise.  An argument $i\in\IN$ of an operator
  $f$ is \emph{receiving} if a variable $x$ is receiving in a term $t$
  that has a subterm $f(v_1,\ldots,v_n)$ with $x$ occurring in $v_i$.
\item A rule of the form $\displaystyle
  \frac{x_i\goto{\tau}y}{f(x_1,\ldots,x_n)\goto{\tau}f(x_1,\ldots,x_n)[y/x_i]}$
  with $1\leq i\leq n$ is called a \emph{patience rule} for the
  $i^{th}$ argument of $f$. Here $t[y/x]$ denotes term $t$ with all
  occurrences of $x$ replaced by $y$.
\end{itemise}
\end{definition}
Non-straight operators in positive GSOS languages rarely occur in the literature.

\begin{definition}{simply cool}
A GSOS language $\GL$ is \emph{simply WB cool} if it is positive and
\begin{itemise}
\item[1.] all operators in $\GL$ are straight,
\item[2.] patience rules are the only rules in $\GL$ with $\tau$-premises,
\item[3.] every active argument of an operator has a patience rule,
\item[4.] every receiving argument of an operator has a patience rule,
\item[5.] all operators in $\GL$ are smooth.
\end{itemise}
The formats \emph{simply DB cool}, \emph{simply HB cool} and
\emph{simply BB cool} are defined likewise, but skipping Clause 4 for
DB and BB, and Clause 5 for HB and BB\@.
\end{definition}
The simply WB and BB cool formats above coincide with the ones of
\cite{Bl95}, whereas the simply DB cool format coincides with the {\tt
eb} format of \cite{UP02}.

\begin{example}{CSP}
\newcommand{\fP}{{\cal P}}
Consider the following fragment of the language \emph{Communicating
Sequential Processes} (CSP), for a given set $A$ of visible actions.
The set $\fP$ of CSP expressions is defined inductively by
$$\begin{array}{l@{~\in\fP~~~}lll}
\hline
0 && (\mbox{inaction})\\
a.P              &\mbox{for}~ a\in A
		    \mbox{ and } P \in \fP  & (\mbox{action prefix})\\
P\sqcap Q	 &\mbox{for}~ P,Q \in \fP & (\mbox{internal choice})\\
P\mathbin\Box Q	 &\mbox{for}~ P,Q \in \fP & (\mbox{external choice})\\
P\|_S Q	         &\mbox{for}~ P,Q \in \fP \mbox{ and } S \subseteq A
                   & (\mbox{parallel composition})\\
P\backslash a    &\mbox{for}~ P \in \fP \mbox{ and } a \in A
                         & (\mbox{abstraction})\\
\hline
\end{array}$$
Roughly, the meaning of these process constructions is as follows.
The process $0$ never performs any actions.  $a.P$ denotes a process
which first performs the action $a$ and then behaves as $P$.
$P\sqcap Q$ is a process that first makes a choice between $P$ and $Q$
and subsequently behaves like the chosen process.
$P\mathbin\Box Q$ is a process that behaves either like $P$ or like
$Q$, the choice being made by the occurrence of any visible action of
either $P$ or $Q$, which in turn may be influenced by the environment.
$P\|_S Q$ denotes the parallel composition of processes $P$ and $Q$.
Actions $a\mathbin\in S$ enforce synchronisation between $P$ and $Q$; they can
only happen when both arguments can partake in performing them.
Actions $a \mathbin{\not\in} S$ of either $P$ and $Q$ will be interleaved.
$P\backslash a$ behaves like $P$, but with the action $a$ made
invisible or internal.

The following operational semantics of CSP stems from {\sc
Olderog and Hoare} \cite{OH86}; it is shown to be consistent with the
original denotational semantics of {\sc Hoare, Brookes \& Roscoe}~\cite{BHR84}.
It models the making of an internal choice through an internal
action $\tau \mathbin{\not\in} A$ and captures the interplay between internal
and external choice by assuming that in $P\mathbin\Box Q$, as long as
no visible actions occurs, the internal actions of $P$ and $Q$
happen in parallel.  Below, $a$ and $b$ range over $Act =
A\dcup \{\tau\}$.
$$\begin{array}{@{}c@{}}\displaystyle
  a.x_1 \goto{a} x_1~~~~~~~~~~~~~~~
  x_1\sqcap x_2 \goto{\tau} x_1~~~~~~~~~~~~~~~
  x_1\sqcap x_2 \goto{\tau} x_2
\\[12pt]\displaystyle
  \frac{x_1 \goto{a} y_1}{x_1\mathbin\Box x_2 \goto{a} y_1}~(a\neq\tau)~~~~~
  \frac{x_2 \goto{a} y_2}{x_1\mathbin\Box x_2 \goto{a} y_2}~(a\neq\tau)~~~~~
  \frac{x_1 \goto{\tau} y_1}{x_1\mathbin\Box x_2 \goto{\tau} y_1\mathbin\Box x_2}~~~~~
  \frac{x_2 \goto{\tau} y_2}{x_1\mathbin\Box x_2 \goto{\tau} x_1\mathbin\Box y_2}
\\[12pt]\displaystyle
  \frac{x_1 \goto{a} y_1}{x_1 \|_S x_2 \goto{a} y_1\|_S x_2}~(a\not\in S)~~~~~
  \frac{x_2 \goto{a} y_2}{x_1 \|_S x_2 \goto{a} x_1\|_S y_2}~(a\not\in S)~~~~~
  \frac{x_1 \goto{a} y_1~~~x_2 \goto{a} y_2}{x_1 \|_S x_2 \goto{a}
  y_1\|_S y_2}~(a\in S)
\\[12pt]\displaystyle
  \frac{x_1 \goto{a} y_1}{x_1 \backslash a \goto{\tau} y_1\backslash a}~~~~~~~~~~
  \frac{x_1 \goto{b} y_1}{x_1 \backslash a \goto{b} y_1\backslash a}~(b\neq a)
  \end{array}$$
This makes CSP into a WB cool GSOS language. Hence, $\bis{w}$,
$\bis{d}$, $\bis{\eta}$ and $\bis{b}$ are congruences on this language.
\end{example}

\begin{example}{negative}
The GSOS language with $0$, action prefix operators $a.P$ for $a
\mathbin\in Act$ and the unary operator $n$ with rules
$\frac{x_1 \goto{\tau} y_1}{n(x_1) \goto{\tau} n(y_1)}$ and
$\frac{x_1\gonotto{a}}{n(x_1)\goto{c} 0}$ (for a specific action $a$) is
not positive, but otherwise meets the requirements of \df{simply
cool}.  Yet, $\bis{w}$, $\bis{d}$, $\bis{\eta}$ and $\bis{b}$ fail to
be congruences on this language.  Namely $a.0 \bis{b} \tau.a.0$ yet
$n(a.0) \nobis{w} n(\tau.a.0)$, as only the latter process can perform
a $c$-transition. (Here I use that $\bis{b}$ is the finest equivalence
of $\bis{w}$, $\bis{d}$, $\bis{\eta}$ and $\bis{b}$, and  $\bis{w}$ the
coarsest. Thus we have $a.0 \bis{x} \tau.a.0$ yet $n(a.0) \nobis{x}
n(\tau.a.0)$ for any $x\in\{w,d,\eta,b\}$.) This shows that the
requirement that $\GL$ be positive cannot simply be skipped.
\end{example}

\begin{example}{non-straight}
An operator $q$ with a rules $\frac{x_1 \goto{\tau} y_1}{q(x_1)
\goto{\tau} q(y_1)}$ and $\frac{x_1\goto{a}y,~~x_1\goto{b}z}{q(x_1)\goto{c}
q(y)}$ (for three specific actions $a,b,c\in A$) would not be
straight, although it satisfies the other requirements of \df{simply
cool}. A process $p$ with $p \goto{a} q$ and $p \goto{b}r$ (and no
other outgoing transitions) is branching bisimilar to processes $p'$
as well as $p''$ with $p' \goto{\tau} p''$, $p'' \goto{\tau} p'$, $p'
\goto{a} q$ and $p'' \goto{b}r$ (and $p'$ and $p''$ having no other
outgoing transitions).  Yet $q(p)$ can do a $c$-action, whereas
$q(p')$ cannot.  This shows that in general $\bis{w}$, $\bis{d}$,
$\bis{\eta}$ and $\bis{b}$ fail to be congruences on languages
incorporating this operator. Hence requirement 1 of \df{simply cool}
cannot be skipped.
\end{example}

\begin{example}{non-patient}
The GSOS language with $0$, action prefix operators $a.P$ for $a
\mathbin\in Act$ and the unary operator $m$ with rules
$\frac{x_1 \goto{\tau} y_1}{m(x_1) \goto{\tau} m(y_1)}$ and
$\frac{x_1\goto{\tau}y_1}{m(x)\goto{c} m(y_1)}$ fails requirement 2 of
\df{simply cool} only. As $0 \bis{b} \tau.0$ but $m(0) \nobis{w}
m(\tau.0)$, given that only the latter process can do a
$c$-transition, $\bis{w}$, $\bis{d}$, $\bis{\eta}$ and $\bis{b}$ fail to
be congruences on this language. Thus also requirement 2 cannot be skipped.
\end{example}

\begin{example}{active}
The GSOS language with $0$, action prefix operators $a.P$ for $a
\mathbin\in Act$ and the unary operator $i$ with rule
$\frac{x_1\goto{a}y_1}{i(x)\goto{c} 0}$, and no patience rule, fails
requirement 3 of \df{simply cool} only, considering that the argument
of $i$ is active but not receiving. As $a.0 \bis{b} \tau.a.0$ but
$i(a.0) \nobis{w} i(\tau.a.0)$, given that only the former process can
ever do a $c$-transition, $\bis{w}$, $\bis{d}$, $\bis{\eta}$ and
$\bis{b}$ fail to be congruences on this language. Thus also
requirement 3 cannot be skipped.
\end{example}

\begin{example}{receiving}
The GSOS language with $0$, $\Box$, $\sqcap$, action prefix operators
$a.P$ for $a \mathbin\in Act$ and the unary operators $f,g$ with rules
$\frac{x_1 \goto{\tau} y_1}{f(x_1) \goto{\tau} f(y_1)}$, $\frac{x_1
  \goto{a} y_1}{f(x_1) \goto{a} g(y_1)}$ and $g(x) \goto{c} x$, fails
requirement 4 of \df{simply cool} only, considering that the argument
of $g$ is receiving but not active. Hence $\bis{d}$ and $\bis{b}$ are
congruences on this language. One has
$a.(b.0 \sqcap d.0) \bis{\eta} a.(b.0 \sqcap d.0) \mathbin\Box a.b.0$, yet
$$f(a.(b.0 \sqcap d.0)) \bis{}
  a.c.(b.0 \sqcap d.0) \nobis{w}
  a.c.(b.0 \sqcap d.0) \mathbin\Box a.c.b.0 \bis{}
  f(a.(b.0 \sqcap d.0) \mathbin\Box a.b.0)$$
given that only the right-hand process can do an $a$-transition
(possibly followed or preceded by internal actions) and reach a state
in which the possibility to ever do a $d$-transition is ruled out.
Hence $\bis{w}$ and $\bis{\eta}$ fail to be congruences on this language.
Thus also requirement 4 cannot be skipped for the simply WB and HB
cool formats.
\end{example}

\begin{example}{non-smooth}
An example of a straight but not smooth operator is the operator $s$
of \cite[Section 10(4)]{GW96} that allows a process (its argument) to
proceed normally, but in addition can report that the process is ready
to perform a visible action, without actually doing it.  It supposes
an alphabet $Act = {\cal L} \dcup \{\mbox{\footnotesize Can do `$a$'}
\mid a \in {\cal L}\} \dcup \{\tau\}$, and its rules are
$$\frac{x \goto{a} y}{s(x) \goto{a} s(y)}~(a\in Act)
~~~~~~~~~~
  \frac{x \goto{a} y}{s(x) \stackrel{\raisebox{-2pt}[0pt][0pt]
  {\tiny Can do	`$a$'}}
  {-\!\!\!-\!\!\!-\!\!\!\longrightarrow} s(x)}~(a\in {\cal L})$$
It is not smooth because in the latter rule $x$ occurs in the target
as well as in the left-hand side of its premise.
The GSOS language that combines this operator with $0$,
action prefix operators $a.P$ for $a \mathbin\in Act$, and constants
$p$ and $q$ with rules
$p \goto{a} 0$, $p \goto{\tau} b.0$,
$q \goto{a} 0$, $q \goto{\tau} b.0$ and $q \goto{b} 0$, 
satisfies requirements 1--4 of \df{simply cool} but not requirement 5.
Hence  $\bis{\eta}$ and $\bis{b}$ are congruences on this language.
Yet $\bis{d}$ and $\bis{w}$ are not, for $p \bis{d} q$ whereas
$s(p) \nobis{w} s(q)$. Namely only $s(q)$ can report ``can do
{`$b$'}'' and then do $a$ (see Figure~7 in \cite{GW96}). Thus also 
requirement 5 cannot be skipped for the simply WB and DB cool formats.
\end{example}

\begin{lemma}{receiving}
Suppose $\GL$ satisfies Clause 4 in the definition of simply WB cool
above, and let $\mu,\nu$ be closed substitutions.  If
$\mu(y)\dto\nu(y)$ for every $y\in\var(t)$ that is receiving in
$t$, and $\mu(x)=\nu(x)$ for every $x\in\var(t)$ that is not
receiving in $t$, then $\mu(t)\dto\nu(t)$.
\end{lemma}

\begin{proof} By structural induction on $t$.
If $t$ is a variable, the statement follows by assumption.
\\
Otherwise, $t=f(t_1,\ldots,t_n)$. It suffices to show that for
$i=1,\ldots,n$ one has
\begin{equation}\label{receiving}
f(\nu(t_1),...,\nu(t_{i-1}),\mu(t_i),
\mu(t_{i+1}),...,\mu(t_n)) \dto f(\nu(t_1),...
\nu(t_{i-1}),\nu(t_i),\mu(t_{i+1}),...,\mu(t_n)).
\end{equation}
If $t_i$ contains no variable that is receiving in $t$, then
$\mu(t_i)=\nu(t_i)$ by assumption, which yields (\ref{receiving}).
If $t_i$ does contain such a variable, then, by definition, $i$ is a
receiving argument of $f$.  By induction, $\mu(t_i)\dto\nu(t_i)$,
and the patience rule for the $i^{th}$ argument of $f$ yields
(\ref{receiving}).
\end{proof}

\begin{trivlist}\vspace*{-16pt}
\item[\hspace{\labelsep}\bf Proof of Lemma WB:]
Let $\GL$ be simply WB cool, let \plat{r=
\frac{\{x_i \goto{c_i} y_i\mid i\in I\}}{f(x_1,\ldots,x_n)\goto{a}t}}
be a rule in $\GL$ and let $\mu,\nu$ be closed substitutions such that
\begin{itemise}\topsep 0pt \itemsep 0pt \parsep 0pt
\item $\nu(x_i)\dto \mu(x_i) \goto{\opt{c_i}}\mu(y_i)\dto\nu(y_i)$ for
  $i\!\in\!I$,
\item $\nu(x) = \mu(x)$ for all variables $x$ that do not occur in the
  premises of $r$.
\end{itemise}
I need to show that $\nu(f(x_1,\ldots,x_n))\dto\goto{\opt{a}}\dto \nu(t)$.

In case $r$ is a patience rule---so $I=\{k\}$, $c_k=\tau$ and
$t=f(x_1,\ldots,x_n)[y_k/x_k]$ with $1\leq k\leq n$---one has
$\nu(f(x_1,...,x_n))\dto \mu(f(x_1,...,x_n))
\goto{\opt{\tau}}\mu(f(x_1,...,x_n)[y_k/x_k])\dto\nu(f(x_1,...,x_n)[y_k/x_k])$
by repeated application of $r$.

Otherwise, $\goto{\opt{c}} \,=\, \goto{c}$ by Clause 2 of \df{simply cool}.
Now $\nu(f(x_1,\ldots,x_n))\dto\mu(f(x_1,\ldots,x_n))$ by Clause 3, and
$\mu(f(x_1,\ldots,x_n))\goto{a}\mu(t)$ by application of $r$. Clause 5
yields that $\mu(x)=\nu(x)$ for all variables $x\in \var(t)$ that are not
  receiving in $t$, so $\mu(t)\dto\nu(t)$ by \lem{receiving}.\hfill$\Box$
\end{trivlist}
The {\bf Proof of Lemma DB} proceeds likewise, but taking
$\mu(x)=\nu(x)$ for all variables $x$ that do not occur in the
left-hand side of premises. Clause 5 now implies that $\mu(t)=\nu(t)$.
\hfill$\Box$

\begin{trivlist}
\item[\hspace{\labelsep}\bf Proof of Lemma HB:]
Let $\GL$ be simply HB cool, let \plat{r=
\frac{\{x_i \goto{c_i} y_i\mid i\in I\}}{f(x_1,\ldots,x_n)\goto{a}t}}
be a rule in $\GL$ and let $\rho,\mu,\nu$ be closed substitutions such that
\begin{itemise}\topsep 0pt \itemsep 0pt \parsep 0pt
\item $\rho(x_i)\dto \nu(x_i) \goto{\opt{c_i}}\mu(y_i)\dto\nu(y_i)$ for
  $i\!\in\!I$,
\item $\rho(x_i) = \nu(x_i) = \mu(x_i)$ for $i\!\not\in\!I$, and
\item $\nu(x) = \mu(x)$ for all variables $x$ that do not occur as
  right-hand sides of premises in $H$.
\end{itemise}
I need to show that $\rho(f(x_1,\ldots,x_n))\dto\nu(f(x_1,\ldots,x_n))
\goto{\opt{a}}\dto \nu(t)$.\\
Note that $\nu(f(x_1,\ldots,x_n))=\mu(f(x_1,\ldots,x_n))$.

In case $r$ is a patience rule---so $I=\{k\}$, $c_k=\tau$ and
$t=f(x_1,\ldots,x_n)[y_k/x_k]$ with $1\leq k\leq n$---one has
$\rho(f(x_1,...,x_n))\dto \nu(f(x_1,...,x_n))
\goto{\opt{\tau}}\mu(f(x_1,...,x_n)[y_k/x_k])\dto\nu(f(x_1,...,x_n)[y_k/x_k])$
by repeated application of $r$.

Otherwise, $\goto{\opt{c}} \,=\, \goto{c}$ by Clause 2 of \df{simply cool}.
Now $\rho(f(x_1,\ldots,x_n))\dto\nu(f(x_1,\ldots,x_n))$ by Clause 3,
$\nu(f(x_1,\ldots,x_n))\goto{a}\mu(t)$ by application of $r$;
and $\mu(t)\dto\nu(t)$ by \lem{receiving}.\hfill$\Box$
\end{trivlist}
The {\bf Proof of Lemma BB} proceeds likewise, but omitting $\mu$.\hfill$\Box$

\section{Cool GSOS languages}\label{cool}

In this section I will extend the simply XB cool rule formats to XB
cool rule formats and establish the associated congruence theorems
(X$\in\{$W,D,H,B$\}$).

\begin{definition}{two-tiered}
A GSOS language is \emph{two-tiered} if its operators are
partitioned into \emph{abbreviations} and \emph{principal operators},
and for every abbreviation $f$ a principal operator $f^\star$ is
specified, together with a substitution
$\sigma\!_f:\{x_1,\ldots,x_{ar(f^\star)}\}\rightarrow\{x_1,\ldots,x_{ar(f)}\}$,
such that the rules of $f$ are $$\left\{
\frac{\sigma\!_f(H)}{f(x_1,\ldots,x_{ar(f)})\goto{a}\sigma\!_f(t)} \;\left|\;
\frac{H}{f^\star(x_1,\ldots,x_{ar(f^\star)})\goto{a}t} \mbox{ is a rule of
} f^\star\right.\right\}.$$
Write $f(i)$ for the $j$ such that $\sigma\!_f(x_i)=x_j$;
take $f^\star=f$ and $f(i)=i$ in case $f$ is a principal operator.
\end{definition}
Trivially, any positive GSOS language can be extended (\emph{straightened}) to
a two-tiered GSOS language whose principal operators are (straight and)
smooth \cite{ABV94}.

\begin{example}{straightening}\vspace*{-4pt}
Let $\GL$ have a binary operator $f$ with as only rule \plat{
\frac{x_1\goto{a}y,~~x_1\goto{b}z}{f(x_1,x_2)\goto{a}f(x_1,(f(y,x_2))}}.\\[1em]
Then $\GL$ can be straightened by adding a operator $f^\star$
with rule \plat{\frac{x_1\goto{a}y,~~x_2\goto{b}z}
{f^\star(x_1,x_2,x_3,x_4)\goto{a}f(x_3,f(y,x_4))}}.\\ In this case
$\sigma\!_f(x_4)=x_2$ and $\sigma\!_f(x_1)=\sigma\!_f(x_2)=\sigma\!_f(x_3)=x_1$.
\end{example}
Equally trivial, $f(p_1,...,p_{ar(f)})\goto{a}t$ iff
$f^\star(p_{f(1)},...,p_{f(ar(f^\star))})\goto{a}t$;\\
so $f(p_1,...,p_{ar(f)})\bis{}f^\star(p_{f(1)},...,p_{f(ar(f^\star))})$.

\begin{definition}{cool}
A two-tiered GSOS language $\GL$ is \emph{WB cool} if it is positive and
\begin{itemise}
\item[1.] all principal operators in $\GL$ are straight,
\item[2.] patience rules are the only rules of principal operators
  with $\tau$-premises,
\item[3.] every active argument of a principal operator has a patience rule,
\item[4.] if argument $f(i)$ of operator $f$ is receiving, then
  argument $i$ of $f^\star$ has a patience rule,
\item[5.] all principal operators in $\GL$ are smooth.
\end{itemise}
The formats \emph{DB cool}, \emph{HB cool} and \emph{BB cool} are
defined likewise, but skipping Clause 4 for DB and BB, and Clause 5
for HB and BB\@. Clause 4 may be weakened slightly; see
Section~\ref{extension}.
\end{definition}
Note that the simply cool formats defined before are exactly the cool formats
with the extra restriction that all operators are principal.

\begin{theorem}{cool}
On any WB cool GSOS language, weak bisimulation
equivalence is a congruence.

On any DB cool GSOS language, delay bisimulation
equivalence is a congruence.

On any HB cool GSOS language, $\eta$-bisimulation
equivalence is a congruence.

On any BB cool GSOS language, branching bisimulation
equivalence is a congruence.
\end{theorem}
Given that the cool GSOS languages differ from the simply cool GSOS
languages only by the addition of operators that can be regarded as
syntactic sugar, the theorems above are a simple consequence of the
corresponding theorems for simply cool GSOS languages. Below I go
through the details.

\begin{definition}{translation}
Let $\GL$ be a two-tiered GSOS language, with signature $\Sigma$.  Let
$\Sigma^\star$ be the subcollection of principal operators in
$\Sigma$, and $\Sigma^*=\{f^*\mid f \in \Sigma^\star\}$ be a
collection of fresh names for the latter. For $f\in \Sigma$ an
abbreviation, write $f^*$ for $(f^\star)^*$.  Define the translation
$^*:T(\Sigma)\rightarrow T(\Sigma^*)$ recursively by $x^*=x$ for $x\in V$ and
$(f(t_1,\ldots,t_{ar(f)}))^* = f^*(t_{f(1)}^*,\ldots,t_{f(ar(f^*))}^*)$.
Let $\GL^*$ be the GSOS language with signature $\Sigma^*$ and
rules $\frac{H}{f^*(x_1,\ldots,x_{ar(f)})\goto{a}t^*}$
for $f\in\Sigma^\star$ and \plat{
\frac{H}{f(x_1,\ldots,x_{ar(f)})\goto{a}t}}\vspace{-8pt} a rule of $\GL$.
\end{definition}

\begin{observation}{cool}
Let $\GL$ be XB cool, with X$\in\{$W,D,H,B$\}$.
Then $\GL^*$ is simply XB cool.
\end{observation}
Any equivalence relation $\sim$ on processes defined in terms of the
transitions between them, naturally extends to an equivalence relation
on the disjoint union of $T(\Sigma)$ and $T(\Sigma^*)$, with $\GL$
generating the transitions between processes from $T(\Sigma)$ and
$\GL^*$ generating the transitions between processes from
$T(\Sigma)^*$ (see \df{transition}).

\begin{lemma}{two-tiered}
Let $\GL$ be a two-tiered GSOS language, with signature $\Sigma$. Then
$p^* \goto{a}_{\GL^*} p'_{\rm next}$ iff $\exists p_{\rm next}
(p'_{\rm next}=p_{\rm next}^* \wedge p \goto{a}_\GL p_{\rm next})$.
\vspace*{-4pt}
\end{lemma}

\begin{proof}
Note that any term in $\GL^*$ has the form $t^*$, with $t$
a term in $\GL$, uniquely determined by $t^*$. Using this, the
statement of the lemma can be simplified to
$p^* \goto{a}_{\GL^*} p^*_{\rm next}$ iff $p \goto{a}_\GL p_{\rm next}$.

``If'':  Suppose $p^* \goto{a}_{\GL^*} p^*_{\rm next}$.
Let $p^* := f^*(p^*_1,...,p^*_n)$.
By \df{transition}, $\GL^*$ has a transition rule
$\frac{H}{f^*(x_1,...,x_n)\goto{a}t^*}$ and there is a closed substitution
$\sigma^*:V\rightarrow\IT(\Sigma^*)$ with $\sigma^*(x_i)=p^*_i$ for
$i=1,...,n$ and $\sigma^*(t^*)=p^*_{\rm next}$,
such that $p^*_i\goto{c}_\GL\sigma^*(y)$ for $(x_i\goto{c}y)\mathbin\in H$ and
$\neg\exists r^*(p^*_i\goto{c}_\GL r^*)$ for $(x_i\gonotto{c})\mathbin\in H$.
Let $\sigma: V\rightarrow \IT(\Sigma)$ be the closed substitution
with $\sigma^*(x)\mathbin=\sigma(x)^*$ for all $x\mathbin\in V$. Then
$\sigma(t)\mathbin=p_{\rm next}$.
By induction, $p_i\goto{c}_\GL\sigma(y)$ for $(x_i\goto{c}y)\in H$ and
$\neg\exists r(p_i\goto{c}_\GL r)$ for $(x_i\gonotto{c})\in H$.
Using \df{translation}, $\GL$ must have a transition rule
\plat{\frac{H}{f(x_1,...,x_n)\goto{a}t}}. So by \df{transition},
$p = f(p_1,...,p_n) \goto{a}_\GL p_{\rm next}$.

``Only if'': Suppose $p \goto{a}_{\GL} p_{\rm next}$.
Let $p := f(p_1,...,p_n)$. I first deal with the case that $f\in\Sigma^\star$.
By \df{transition}, $\GL$ has a transition rule
$\frac{H}{f(x_1,...,x_n)\goto{a}t}$ and there is a closed substitution
$\sigma:V\rightarrow\IT(\Sigma)$ with $\sigma(x_i)=p_i$ for
$i=1,...,n$ and $\sigma(t)=p_{\rm next}$,
such that $p_i\goto{c}_\GL\sigma(y)$ for $(x_i\goto{c}y)\mathbin\in H$ and
$\neg\exists r(p_i\goto{c}_\GL r)$ for $(x_i\gonotto{c})\mathbin\in H$.
Let $\sigma^*: V\rightarrow \IT(\Sigma^*)$ be the closed substitution
with $\sigma^*(x)=\sigma(x)^*$ for all $x\mathbin\in V$. Then
$\sigma^*(t^*)=p^*_{\rm next}$.
By induction, $p^*_i\goto{c}_\GL\sigma^*(y)$ for $(x_i\goto{c}y)\in H$ and
$\neg\exists r^*(p^*_i\goto{c}_\GL r^*)$ for $(x_i\gonotto{c})\in H$.
Using \df{translation}, $\GL^*$ must have a transition rule
$\frac{H}{f^*(x_1,...,x_n)\goto{a}t^*}$. So by \df{transition},
$p^* = f^*(p^*_1,...,p^*_n) \goto{a}_{\GL^*} p^*_{\rm next}$.

Next, consider the case that $f\not\in\Sigma^\star$. Then
$q \goto{a}_\GL p_{\rm next}$ with
$q := f^\star(p_{f(1)},...,p_{f(ar(f^\star))})$.
As $f^\star \in \Sigma^\star$, the previous case of this proof yields
$q^* \goto{a}_{\GL^*} p^*_{\rm next}$.
But $p^* = f^*(t_{f(1)}^*,\ldots,t_{f(ar(f^*))}^*)=q^*$, by \df{translation}.
\end{proof}

\begin{corollary}{two-tiered}
Let $\GL$ be a two-tired GSOS language, and $\sim$ be any equivalence
relation on processes satisfying $p \bis{} q \Rightarrow p \sim q$.
Then $p^* \sim q^*$ iff $p \sim q$.
\end{corollary}

\begin{proof}
We have $p\bis{}p^*$ for all $p\in T(\Sigma)$, because the relation
$\{(p,p^*),(p^*,p)\mid p \in T(\Sigma)\}$ is a strong bisimulation by
\lem{two-tiered}. Hence if $p\sim q$ then $p^* \bis{} p \sim q \bis{}
q*$, implying $p^*\sim q^*$, and if $p^*\sim q^*$ then $p \bis{} p^*
\sim q^* \bis{} q$, implying $p\sim q$.
\end{proof}

\begin{corollary}{two-tiered congruence}
Let $\GL$ be a two-tiered GSOS language such that $\sim$ is a
congruence on $\GL^*$, for $\sim$ an equivalence relation satisfying
$p \bis{} q \Rightarrow p \sim q$. Then $\sim$ is a congruence on $\GL$.
\end{corollary}
\begin{proof}
Let $ar(f)=n$.  Suppose $p_i \sim q_i$ for $i=1,...,n$.  By
\cor{two-tiered}, $p_i^* \sim q_i^*$ for $i=1,...,n$.  By
assumption, $(f(p_1,...,p_n))^* \sim (f(q_1,...,q_n))^*$.  Thus,
by \cor{two-tiered}, $f(p_1,...,p_n) \sim f(q_1,...,q_n)$.
\end{proof}

\begin{trivlist}
\item[\hspace{\labelsep}\bf Proof of \thm{cool}:]
Let $\GL$ be XB cool, with X$\in\{$W,D,H,B$\}$.
By \obs{cool}, $\GL^*$ is simply XB cool.
So by \thm{simply cool}, $\bis{X}$ is a congruence on $\GL^*$.
Apply \cor{two-tiered congruence}.\hfill$\Box$
\end{trivlist}

In fact, \thm{cool} can be obtained as an instance of a more general
theorem.

\begin{theorem}{two-tiered}
Let $\sim$ be any equivalence relation on processes defined
in terms of the transitions between them, satisfying $p \bis{} q
\Rightarrow p \sim q$, and let $F$ be a format on transition system
specifications, so that on any language in $F$-format, $\sim$ is a
congruence. Define a two-tiered language $\GL$ to be in
the \emph{two-tiered} $F$-format iff $\GL^*$ is in $F$-format.
Now $\sim$ is a congruence on any language in the two-tiered $F$-format.
\end{theorem}
This follows by the very same proof as of \thm{cool}.
Note that the XB cool format is exactly the two-tiered simply XB cool
format, for $X \in \{W,D,B,H\}$.


\subsection{Bifurcation rules}\label{bifurcation}

Let $\GL$ be BB cool.
If argument $f(i)$ of operator $f$ is active, then argument $i$ of
$f^\star$ must also be active, so Clause 3 of \df{cool} says
that $f^\star$ has a patience rule $\frac{x_i\goto{\tau}y}
{f^\star(x_1,\ldots,x_n)\goto{\tau}f^\star(x_1,\ldots,x_n)[y/x_i]}$.
By \df{two-tiered} this implies that $f$ must have a rule
\raisebox{0pt}[16pt][0pt]{$\frac{x_{f(i)}\goto{\tau}y}
{f(x_1,\ldots,x_{ar(f)})\goto{\tau}\sigma\!_f(
f^\star(x_1,\ldots,x_n)[y/x_i])}$}.\\
This rule is called a \emph{bifurcation rule} of $f$ \cite{Bl95}.\\
By Clause 2 of \df{cool}, bifurcation rules are the only rules of $f$
with $\tau$-premises.

\subsection{A small extension}\label{extension}

Say that an argument $i$ of an operator $f$ is \emph{ignored} if
$f^\star$ has no argument $k$ with $f(k)=i$. In that case there can be
no rule with source $f(x_1,\ldots,x_{ar(f)})$ with $x_i$ in its
premises or in its target. A subterm $u$ of a term $t$ is
\emph{irrelevant} if occurs within an ignored argument $v_i$ of a
subterm $f(v_1,\ldots,v_{ar(f)})$ of $t$.  Now \df{straight} of an
argument of an operator being receiving may be strengthened by
replacing ``a subterm $f(v_1,\ldots,v_n)$ with $x$ occurring in
$v_i$'' by ``a relevant subterm $f(v_1,\ldots,v_n)$ with $x$ a
relevant subterm of $v_i$''. This yields a slight weakening of Clause 4
in \df{cool}. The weakened clause is still sufficient to obtain
\obs{cool} and hence \thm{cool}.

\begin{example}{ignored variables}
Let $\GL$ have a rule
$\displaystyle\frac{x_1\goto{a}y}{g(x_1)\goto{a}f(h(f(x_1,y)),k(y))}$.
By \df{straight} both the arguments of $h$ and $k$ are receiving, so
Clause 4 in \df{cool} demands patience rules for both $h^\star$ and
$k^\star$.  Now suppose that $h^\star=h$, $k^\star=k$, $ar(f^\star)=1$
and $\sigma\!_f(x_1)=x_1$.  This means that $f(x_1,x_2)$ is an
abbreviation for $f^\star(x_1)$ and the second argument of $f$ is
ignored. In such a case one has $f(p,q) \bis{} f(p,r)$ for all closed
terms $p$, $q$ and $r$.  Now the weakened Clause 4 does not demand a
patience rule for either $h^\star$ or $k^\star$, since the arguments
of $h$ and $k$ are no longer receiving.  Namely, $y$ is an irrelevant
subterm of $f(x_1,y)$ and $k(y)$ is an irrelevant subterm of
$f(h(f(x_1,y)),k(y))$.
\end{example}
The remainder of this section establishes a result that helps to relate
my formulation of the cool formats to Bloom's \cite{Bl95}; for all other
purposes it can be skipped. \pr{cool} below uses the concept of a
\emph{ruloid}; please consult \df{ruloid} and \ex{ruloid} in the next
section first.

Above a definition of an argument of an operator being
receiving was proposed that is more restrictive than \df{straight}.
This definition can be rephrased as follows.

\begin{definition}{truly receiving}
Let $\GL$ be a two-tiered GSOS language.  Define the translation
$^\star:T(\Sigma)\rightarrow T(\Sigma)$ recursively by $x^\star=x$ for
$x\in V$ and $(f(t_1,\ldots,t_n))^\star =
f^\star(t_{f(1)}^\star,\ldots,t_{f(n)}^\star)$.

An argument $i\in\IN$ of an operator $f$ is \emph{truly receiving} if
a variable $x$ is receiving in a term $t$ that has a subterm
$v=f(v_1,\ldots,v_n)$ with $v^\star$ a subterm of $t^\star$ and
$x\in\var(v_i^\star)$.
\end{definition}
Here the requirement ``$v^\star$ is a subterm of $t^\star$'' is
equivalent to ``$v$ is a relevant subterm of $t$'' and
``$x\in\var(v_i^\star)$'' to ``$x$ is a relevant subterm of $v_i$''.
Note that for any term $u$ one has $\var(u^\star) \subseteq \var(u)$,
but not always $\var(u^\star)=\var(u)$. In \ex{ignored variables}, $y
\not\in\var(f(x_1,y)^\star)=\var(f^\star(x_1))=\{x_1\}$ and
$k(y)^\star=k(y)$ is not a subterm of $f(h(f(x_1,y)),k(y))^\star =
f^\star(h(f(x_1,y))^\star)$.

The weakened version of Clause 4 of \df{cool} that was proposed above reads:
\begin{itemise}
\item[\mbox{4\makebox[0in][l]{$^{\rm\scriptscriptstyle G}$}~.}] 
  if argument $f(i)$ of operator $f$ is truly receiving, then
  argument $i$ of $f^\star$ has a patience rule.
\end{itemise}
Here I reformulate this clause in such a way that it resembles the
corresponding requirement in {\sc Bloom} \cite{Bl95}.

\begin{definition}{univariate}
A term $u\in \IT(\Sigma)$ is \emph{univariate} if no variable occurs
more than once in $u$.
\end{definition}
Trivially, any term can be written as $\sigma(u)$ with $u$ a
univariate term and $\sigma:V\rightarrow V$.

\begin{proposition}{cool}
In the definition of WB and HB cool GSOS languages,
Clause $4^{\rm\scriptscriptstyle G}$ is equivalent to
\begin{itemise}
\item[\mbox{4\makebox[0in][l]{$^{\rm\scriptscriptstyle B}$}~.}]
  if $x\in \var(t)$ is receiving in
  $t$, $u$ is a univariate term, $y\in\var(u)$, and
  $\sigma:V\rightarrow V$ is a substitution such that
  $\sigma(u)=t^\star$ and $\sigma(y)=x$, then there is an $\GL$-ruloid
  $\frac{y\goto{\tau}z}{u\goto{\tau}u[z/y]}$.
\end{itemise}
\end{proposition}

\begin{proof}
$4^{\rm\scriptscriptstyle G} \Rightarrow 4^{\rm\scriptscriptstyle B}$:
Suppose $\GL$ satisfies Clause $4^{\rm\scriptscriptstyle G}$,
$x\in\var(t)$ is receiving in $t$, $u$ is a univariate term,
$y\in\var(u)$, and $\sigma:V\rightarrow V$ is a substitution such that
$\sigma(u)=t^\star$ and $\sigma(y)=x$. With structural induction on
subterms $w$ of $u$ that contain $y$, I show that there is an
$\GL$-ruloid ${\frac{y\goto{\tau}z}{w\goto{\tau}w[z/y]}}$.  For every
such $w$ there is a subterm $v$ of $t$ with $\sigma(w)=v^\star$ a
subterm of $t^\star$ and $x \in \var(t^\star)$.
\\\emph{Base case:} $w=y$. By definition, there is a ruloid
$\frac{y\goto{\tau}z}{y\goto{\tau}z}$.
\\\emph{Induction step:} Let $v=f(v_1,\ldots,v_{ar(f)})$ and
$w=f^\star(w_1,\ldots,w_n)$, and let $i\in\{1,\ldots,n\}$
be the unique argument of $f^\star$ with $y\in\var(w_i)$.
Then \plat{\sigma(w_i)=v^\star_{f(i)}}, so
\plat{x\in\var(v^\star_{f(i)})\subseteq \var(v_{f(i)})}.
Thus $f(i)$ is a truly receiving argument of $f$, and
$\GL$ has a patience rule $\frac{x_i\goto{\tau}z'}
{f^\star(x_1,\ldots,x_n)\goto{\tau}f^\star(x_1,\ldots,x_n)[z'/x_i]}$.
By induction, there is an $\GL$-ruloid
\plat{\frac{y\goto{\tau}z}{w_i\goto{\tau}w_i[z/y]}}, so
by \df{ruloid} one obtains the required $\GL$-ruloid $\frac{y\goto{\tau}z}
{f^\star(w_1,\ldots,w_n)\goto{\tau}f^\star(w_1,\ldots,w_n)[z/y]}$.

$4^{\rm\scriptscriptstyle B} \Rightarrow 4^{\rm\scriptscriptstyle G}$:
Suppose $\GL$ satisfies Clause $4^{\rm\scriptscriptstyle B}$, and
argument $f(i)$ of operator $f$ is truly receiving. Then there must be
a term $t$ with a subterm $v=f(v_1,\ldots,v_{ar(f)})$ such that
$v^\star$ is a subterm of $t^\star$ and variable
$x\in\var(v^\star_{f(i)})$ is receiving in $t$.  Let $u$ be a
univariate term, and $\sigma:V\rightarrow V$ a substitution such that
$\sigma(u)=t^\star$. Let $w=f^\star(w_1,\ldots,w_n)$ be the subterm of
$u$ with $\sigma(w)=v^\star$. Then \plat{\sigma(w_i)=v^\star_{f(i)}}, and
$w_i$ (and hence $u$) must contain a variable $y$ with
$\sigma(y)=x$. By Clause $4^{\rm\scriptscriptstyle B}$ there is an $\GL$-ruloid
$\frac{y\goto{\tau}z}{u\goto{\tau}u[z/y]}$.  By Clause 2 of \df{cool},
patience rules are the only rules for the operators of $u$ with
$\tau$-premises. Hence, by \df{ruloid}, this ruloid can only be
obtained by stacking patience rules. As $u$ is univariate, its subterm
$w_i$ contains the only occurrence of $y$ in $u$, so one of the
patience rules applied must be the one for argument $i$ of $f^\star$.
\end{proof}

\section{Rooted cool GSOS languages}\label{rooted}

In this section I will define the (simply) RWB, RDB, RHB and RBB cool
rule formats and establish the associated congruence theorems.
In order to formulate the requirements for the RWB and RDB cool GSOS
languages I need the concept of a \emph{ruloid}, this being a kind of
derived GSOS rule.

\begin{definition}{ruloid}
For $r$ transition rule, let RHS($r$) denote the set of right-hand sides
of its premises. Let $\GL$ be a positive GSOS language.
The class of \emph{$\GL$-ruloids} is the smallest set of rules such that
\begin{itemise}
\item $\frac{x\goto{a}y}{x\goto{a}y}$ is an $\GL$-ruloid, for every
  $x,y\in V$ and $a\in Act$;
\item if $\sigma$ is a substitution, $\GL$ has a rule $\frac{H}{s\goto{a}t}$,
  and for every premise $x\goto{c}y$ in $H$ there is an $\GL$-ruloid
  \plat{r_y=\frac{H_y}{\sigma(x)\goto{c}\sigma(y)}}
  such that the sets RHS($r_y$) are pairwise disjoint and
  each RHS($r_y$) is disjoint with $\var(\sigma(s))$, then the
  transition rule $\frac{\bigcup_{y\in H}H_y} 
  {\sigma(s)\goto{a}\sigma(t)}$ is an $\GL$-ruloid.
\end{itemise}
\end{definition}
Note that a transition $\alpha$, seen as a rule
\plat{\frac{\emptyset}{\alpha}}, is an $\GL$-ruloid iff it is generated by
$\GL$ in the sense of \df{transition}.  The left-hand sides of
premises of a ruloid are variables that occur in its source, and the
right-hand sides are variables that are all distinct and do
not occur in its source. Its target only contains variables that also
occur elsewhere in the rule.\vspace{-7pt}

\begin{example}{ruloid}
Let $\GL$ contain the rule $\displaystyle
\frac{x_1\goto{a}y_1~~~x_2\goto{b}y_2}{f(x_1,x_2)\goto{a}g(x_1,y_1)}$.
\\
Then $\GL$ has ruloids $\displaystyle
\frac{x\goto{a}x'~~~y\goto{b}y'}{f(x,y)\goto{a}g(x,x')}$
~~and~~
$\displaystyle\frac{x\goto{a}x'~~~y\goto{b}y'~~~z\goto{b}z'}
{f(f(x,y),z)\goto{a}g(f(x,y),g(x,x'))}$.
\end{example}

\begin{lemma}{ruloid receiving}
Suppose an $\GL$-ruloid has a premise with right-hand side $x$ and a
target $t$ containing a subterm $f(t_1,\ldots,t_n)$ with
$x\in\var(t_i)$. Then $i$ is a receiving argument of $f$.
\end{lemma}

\begin{proof}
By \df{ruloid} there must be terms $w_1,\ldots,w_n$, variables
$y_1,\ldots,y_n$, and substitutions $\sigma_1,\ldots,\sigma_n$, such
that $t\!=\!\sigma_1(w_1)$, $y_i$ is receiving in $w_i$
($i\!=\!1,...,n$), $\sigma_i(y_i)\!=\!\sigma_{i+1}(w_{i+1})$
($i\!=\!1,...,n-1$), and $\sigma_n(y_n)=x$; and moreover one of the
$w_k$ has a subterm $f(w_k^1,\ldots,w_k^m)$ with $y_k\in\var(w_k^i)$.
It follows that $i$ is an receiving argument of $f$.
\end{proof}

\begin{definition}{RWB cool}
A GSOS language $\GL$ is \emph{RWB cool} if
the operators can be partitioned in \emph{tame} and \emph{wild} ones,
such that
\begin{itemise}
\item[1.] the target of every rule contains only tame operations;
\item[2.] the sublanguage $\GL^{tame}$ of tame operators in $\GL$ is WB cool;
\item[3.] $\GL$ is positive, and for each rule
  \plat{\frac{H}{s\goto{a}t}} there is a term $u$ and
  a substitution $\sigma:\var(u)\rightarrow \var(s)$ such that\vspace{-2pt}
  \begin{itemise2}
  \item there is an $\GL$-ruloid \plat{\frac{K}{u\goto{a}v}} with
    $\sigma(K)=H$ and $\sigma(v)=t$,
  \item and for every premise $x \goto{c} y$ in $K$, $\GL$ has a rule
    \plat{\frac{\sigma(x)\goto{\tau}y}
    {s\goto{\tau}\sigma(u[y/x])}};
  \end{itemise2}
\item[(4.] 
  if argument $f(i)$ of operator $f$ is receiving in $\GL$, then
  argument $i$ of $f^\star$ has a patience rule.)
\end{itemise}
The formats \emph{RDB cool}, \emph{RHB cool} and \emph{RBB cool} are
defined likewise, adapting ``WB cool'' in the second clause
appropriately, but skipping the third clause for RHB and RBB, and the
last one for RDB and RBB\@. The last clause cannot be skipped for
RHB. The \emph{simply RXB cool} rule formats
(X$\in\!\!\{$W,D,H,B\hspace{-.4pt}$\}$\hspace{-1pt}) are obtained by
requiring the sublanguage of tame operators to be simply \hspace{-1pt}XB cool.
\end{definition}
Note that in the third clause, $u$, $\sigma$ and the ruloid can always
be chosen in such a way that $v=t$.  The instance of this clause with
$s=f(x_1,\ldots,x_{ar(f)})$ for a tame operator $f$ is redundant, as
it vacuously holds when taking
$u^\star=f^\star(x_1,\ldots,x_{ar(f^\star)})$ and $\sigma=\sigma\!_f$;
the rule required in the second subclause is then the bifurcation rule
derived in Section~\ref{bifurcation}.

The last clause above appeared before as Clause 4 in \df{cool} of the
WB and HB cool formats. Given that a term with a receiving variable
cannot contain wild operators, this clause is almost implied by Clause
2 above.  All it adds, is that the requirement of Clause 4 for the
sublanguage of tame operators applies to ``receiving in $\GL$''
instead of merely ``receiving in $\GL^{tame}$\,''.
Thus, the rules for the wild operators help determine which variables
in a term $t$ count as receiving.

\begin{proposition}{RWB cool}
In the definition of the RWB cool format above, the last clause is redundant.
\end{proposition}

\begin{proof}
Let argument $i$ of operator $f$ be $\GL$-receiving.  I will show that
it is already $\GL^{tame}$-receiving.  Let $t$ be a term with a
subterm $f(t_1,\ldots,t_n)$ such that $y\in\var(t_i)$ and $y$ is
$\GL$-receiving in $t$.  So there is a rule
$r=\frac{H}{f(x_1,\ldots,x_n)\goto{a}t}$ in $\GL$ with $y$ occurring
as the right-hand side of a premise in $H$.  Let $u$ and $\sigma$ be
the term and substitution that must exists for $r$ by the third clause
of \df{RWB cool}. \df{RWB cool} implies that the operators in $u$ are
tame, and there is an $\GL$-ruloid, hence an $\GL^{tame}$-ruloid,
\plat{\frac{K}{u\goto{a}v}} with $\sigma(K)=H$ and $\sigma(v)=t$.  Let
$f(v_1,\ldots,v_n)$ be the subterm of $v$ with $\sigma(v_i)=t_i$ for
$i=1,\ldots,n$.  By the third clause of \df{GSOS}, $y\not\in
range(\sigma)$. Hence, as $y\in\var(\sigma(v_i))$, $y \in \var(v_i)$.
Given that $dom(\sigma)=\var(u)$, $\sigma$ does not effect the
right-hand sides of $K$, so $y$ is the right-hand side of a premise in
$K$. By \lem{ruloid receiving}, $i$ is an $\GL^{tame}$-receiving
argument of $f$.
\end{proof}
When working with the slightly stronger definition of receiving
contemplated in Section~\ref{extension}, the proof above remains valid
with trivial adaptations.

Now I will prove the remaining lemmas of Section~\ref{proofs}, thereby
completing the proof of \thm{simply cool}.

\begin{trivlist}
\item[\hspace{\labelsep}\bf Proof of Lemma RHB:] Let $\GL$ be simply
RHB cool, let $r=\frac{H}{s\goto{a}t}$ be a rule in $\GL$, and let
$\nu$ be a closed substitution such that $\nu(x) \goto{{c}} \dto
\nu(y)$ for each positive premise $x\goto{c}y$ in $H$ and $\neg\exists
r\, (\nu(x) \gonotto{c} r)$ for each negative premise $x\gonotto{c}$
in $H$. I need to show that $\nu(s) \goto{{a}} \dto \nu(t)$.
\\
By assumption, there is a closed substitution $\mu$ such that
\begin{itemise}\topsep 0pt \itemsep 0pt \parsep 0pt
\item $\nu(x) \goto{c}\mu(y)\dto\nu(y)$ for each premise $x\goto{c}y$
  in $H$, and
\item $\nu(x) = \mu(x)$ for all variables $x$ that do not occur as
  right-hand sides of premises in $H$.
\end{itemise}
Thus $\nu(s)=\mu(s) \goto{a} \mu(t)$ by application of $r$, and
$\mu(t)\dto\nu(t)$ by \lem{receiving}.\hfill$\Box$
\end{trivlist}

\begin{lemma}{simply WB cool}
Let $\GL$ be simply WB cool, let $r=\frac{H}{s\goto{a}t}$ be an
$\GL$-ruloid, and let $\nu$ be a closed substitution.
If for each premise $x\goto{c}y$ in $H$ one has
$\nu(x)\dto \goto{{c}} \dto \nu(y)$, then
$\nu(s)\dto \goto{{a}} \dto \nu(t)$.
\end{lemma}

\begin{proof}
The case that $r$ is a rule in $\GL$ is proven exactly as in Lemma WB,
just writing $a$ for $\mbox{\footnotesize (}a\mbox{\footnotesize )}$,
etc.  The general case now follows by a straightforward structural
induction on $s$.
\end{proof}

\begin{trivlist}
\item[\hspace{\labelsep}\bf Proof of Lemma RWB:] Let $\GL$ be simply
RWB cool, let $r=\frac{H}{s\goto{a}t}$ be a rule in $\GL$, and let
$\nu$ be a closed substitution such that $\nu(x)\dto \goto{{c}} \dto
\nu(y)$ for each premise $x\goto{c}y$ in $H$.
I need to show that $\nu(s)\dto\goto{a}\dto \nu(t)$.
\\\emph{Case 1:}
Suppose that there is a closed substitution $\mu$ such that
\begin{itemise}\topsep 0pt \itemsep 0pt \parsep 0pt
\item $\nu(x) \goto{c}\mu(y)\dto\nu(y)$ for each premise $x\goto{c}y$
  in $H$, and
\item $\nu(x) = \mu(x)$ for all variables $x$ that do not occur as
  right-hand sides of premises in $H$.
\end{itemise}
Then $\nu(s)=\mu(s) \goto{a} \mu(t)$ by application of $r$, and
$\mu(t)\dto\nu(t)$ by \lem{receiving}.
\\\emph{Case 2:} Suppose that there is a premise $x^0\goto{c}y^0$ in
$H$ such that $\nu(x^0)\goto{\tau}p\dto\goto{c}\dto\nu(y^0)$ for a
closed term $p$.  Let $u$, $\sigma$ and $r'=\frac{K}{u\goto{a}v}$ be
the term, substitution and ruloid that exists for $r$ by the third
clause of \df{RWB cool}, and let $x^1$ be the unique variable in $u$
such that $K$ has a premise $x^1\goto{c}y^0$ (using that
$\sigma(y^0)=y^0$). Hence $\sigma(x^1)=x^0$.  Let $\mu$ be the closed
substitution with $\mu(y^0)=p$ and $\mu(z)=\nu(z)$ for all variables
$z\neq y^0$. Now $\mu(\sigma(x^1))=\mu(x^0)=\nu(x^0)\goto{\tau}\mu(y^0)$.
By Clause 3 of \df{RWB cool}, $\GL$ has a rule
$\frac{\sigma(x^1)\goto{\tau}y^0}{s\goto{\tau}\sigma(u[y^0/x^1])}$;
hence $\nu(s)=\mu(s)\goto{\tau} \mu(\sigma(u[y^0/x^1]))$.  Let $\rho$
be the closed substitution with $\rho(x^1)=p$ and $\rho(z)=\nu(\sigma(z))$
for all variables $z\neq x^1$. Then $\mu(\sigma(u[y^0/x^1])=\rho(u)$,
the operators in $u$ are tame, and $\rho(x)\dto \goto{{c}} \dto
\rho(y)$ for each premise $x\goto{c}y$ in $K$. \lem{simply WB cool}
yields $\rho(u)\dto\goto{a}\dto\rho(v)$. By Clause 5 of \df{simply cool},
$x^1 \not\in \var(v)$, so $\rho(v)=\nu(\sigma(v))=\nu(t)$.
Thus $\nu(s)=\mu(s)\goto{\tau} \mu(\sigma(u[y^0/x^1])) = \rho(u) \dto
\goto{{a}} \dto \rho(v)= \nu(t)$.\hfill$\Box$
\end{trivlist}
The {\bf Proof of Lemma RDB} proceeds likewise, using a DB cool
counterpart of \lem{simply WB cool}.
\hfill$\Box$

\begin{trivlist}
\item[\hspace{\labelsep}This completes the \bf Proof of \thm{simply cool}.]
\hfill$\Box$
\end{trivlist}

\begin{example}{CCS}
The following fragment of CCS has the constant 0, unary operators
$a.\_\,$, binary operators + and $\|$ (usually written $|\,$), and
instances of the GSOS rules below. Here $a$ ranges over \plat{Act =
\names \dcup \overline\names \dcup \{\tau\}} with $\names$ a set of
\emph{names} and $\overline\names=\{\overline a \mid a\in\names\}$ the
set of \emph{co-names}. The function $\overline \cdot$ extends to
$\names \cup \overline\names$ (but not to $Act$) by
$\overline{\overline a}=a$.\vspace{-5pt}
$$\begin{array}{c}\displaystyle
  \frac{x_1 \goto{a} y_1}{x_1+x_2 \goto{a} y_1}~~~~~
  \frac{x_2 \goto{a} y_2}{x_1+x_2 \goto{a} y_2}~~~~~
  a.x_1 \goto{a} x_1
\\[12pt]\displaystyle
  \frac{x_1 \goto{a} y_1}{x_1 \| x_2 \goto{a} y_1\|x_2}~~~~~
  \frac{x_2 \goto{a} y_2}{x_1 \| x_2 \goto{a} x_1\|y_2}~~~~~
  \frac{x_1 \goto{a} y_1~~~x_2 \goto{\overline a} y_2}{x_1 \| x_2
  \goto{\tau} y_1\|y_2}
\end{array}$$
The sublanguage without the + is simply WB cool, and the entire GSOS
language is simply RWB cool.  Clause 3 of \df{RWB cool} applied to the
$i^{th}$ rule for the $+$ is satisfied by taking $u=x$, $\sigma(x)=x_i$,
and the ruloid \plat{\;\frac{x\goto{a}y_i}{x\goto{a}y_i}}; indeed the
language has a ruloid $\frac{x_i \goto{\tau} y_i}{x_1+x_2\goto{\tau}y_i}$.
\end{example}

\begin{example}{left-merge}
Extend the GSOS language of \ex{CCS} with the binary operators
\vspace{-1ex}
$\leftmerge$ and $|$ with rules
$\displaystyle\frac{x_1 \goto{a} y_1}{x_1\leftmerge x_2 \goto{a} y_1\|y_2}$ and
$\displaystyle\frac{x_1 \goto{a} y_1~~~
x_2 \goto{\overline a} y_2}{x_1|x_2 \goto{\tau} y_1\|y_2}$ with $a$
ranging over $Act$.  These are the \emph{left merge} and the
\emph{communication merge} of {\sc Bergstra \& Klop} \cite{BK86a} but
adapted to fit (the communication format of) CCS rather then ACP\@.
(I wrote $\|$ for the CCS parallel composition to avoid name clashes
with this communication merge.) In \cite{BK86a} these operators are
introduced in order to give a finite complete equational
axiomatisation of strong bisimulation equivalence on the language ACP,
and the same approach works for CCS.

The first argument of $\leftmerge$ and both arguments of $|$ are
active, whereas no arguments of $\leftmerge$ and $|$ are receiving.
Since the active arguments of $\leftmerge$ and $|$ do not have
patience rules, both operators need to be classified as wild.
Requirements 1, 2 and 4 of \df{RWB cool} are clearly satisfied.
Hence this GSOS language is RHB cool, and $\bis{r\eta}$ and $\bis{rb}$
are congruences on the entire language.

Requirement 3 applied to the rule for the $\leftmerge$ is satisfied by
\vspace{-1ex}
taking $u=x\|x_2$, $\sigma(x)=x_1$, $\sigma(x_2)=x_2$ and the ruloid
$\displaystyle\frac{x \goto{a} y_1}{x\| x_2 \goto{a} y_1\|x_2}$.
Indeed the language has a ruloid $\displaystyle\frac{x_1 \goto{\tau} y_1}
{x_1\leftmerge x_2\goto{\tau}y_1\|x_2}$. Hence the language with
$\leftmerge$ but without $|$ is RWB cool, guaranteeing that also
$\bis{rw}$ and $\bis{rd}$ are congruences.
However, requirement 3 applied to either rule of the communication
merge is not satisfied. In fact $\bis{rw}$ and $\bis{rd}$ fail to be
congruences for this operator: one has $\tau.a.0 \bis{rd}
\tau.a.0+a.0$ but $$0 \bis{} (\tau.a.0 | \overline{a}.b.0) \nobis{rw}
((\tau.a.0+a.0)|\overline a.b.0) \bis{} \tau.b.0.$$
This shows that this part of requirement 3 of \df{RWB cool} cannot be skipped.
\end{example}

\begin{example}{negative2}
The GSOS language with $0$, action prefix operators $a.P$ for $a
\mathbin\in Act$ and the unary operator $np$ with the rule
$\frac{x_1\gonotto{a}}{np(x_1)\goto{c} 0}$ (for specific actions $a,c$) is
not positive, but otherwise meets the requirements of \df{RWB
cool}.  Yet, $\bis{rw}$ and $\bis{rd}$ fail to
be congruences on this language.  Namely $\tau.a.0 \bis{rd} \tau.a.0 + a.0$ yet
$np(\tau.a.0) \bis{} c.0 \nobis{w} 0 \bis{} np(\tau.a.0 + a.0)$.
This shows that the requirement that $\GL$ be
positive cannot simply be skipped in the RWB and RDB cool formats.
\end{example}
Negative premises of wild operators are allowed in the RHB and RBB
cool formats. This is possible because the first transitions of rooted
branching (or $\eta$-)bisimilar processes need to be matched without
preceding $\tau$-transitions, just as for strong bisimulation.
A good example of an RBB cool GSOS operator with negative premises is
the initial priority operator of \cite{Fok00b}.

\begin{example}{receiving2}
The GSOS language $\GL$ with $0$, $\Box$, $\sqcap$, action prefix operators
$a.P$ for $a \mathbin\in Act$ and the unary operators $f,g$ with rules
$\frac{x_1 \goto{a} y_1}{f(x_1) \goto{a} g(y_1)}$ and $g(x) \goto{c} x$
(for specific actions $a,c$) satisfies requirements 1 and 2 of \df{RWB cool},
provided one classifies the argument of $f$ as wild and that of $g$ as tame.
Hence $\bis{rb}$ is a congruence on $\GL$.
However, $\GL$ fails requirements 3 and 4. Here the argument of $g$ is
receiving in $\GL$ as a whole, although not in $\GL^{tame}$.
In fact, $\bis{rw}$(, $\bis{rd}$) and $\bis{r\eta}$ fail to be
congruences on $\GL$. One has
$a.(b.0 \sqcap d.0) \bis{\eta} a.(b.0 \sqcap d.0) \mathbin\Box a.b.0$,
yet
$$f(a.(b.0 \sqcap d.0)) \bis{}
  a.c.(b.0 \sqcap d.0) \nobis{w}
  a.c.(b.0 \sqcap d.0) \mathbin\Box a.c.b.0 \bis{}
  f(a.(b.0 \sqcap d.0) \mathbin\Box a.b.0)$$
as in \ex{receiving}.
Thus requirement 4 cannot be skipped for the RHB cool format.
\end{example}

\begin{theorem}{rooted weak}
On any RWB cool GSOS language, $\bis{rw}$ is a congruence.

On any RDB cool GSOS language, $\bis{rd}$ is a congruence.

On any RHB cool GSOS language, $\bis{r\eta}$ is a congruence.

On any RBB cool GSOS language, $\bis{rb}$ is a congruence.
\end{theorem}

\begin{proof}
Let $\GL$ be RBB cool. Regard $\GL$ as a two-tiered GSOS languages by
classifying all wild operators as principal ones. The GSOS language
$\GL^*$ constructed in \df{translation} is simply RBB cool, by
\obs{cool}, so by \thm{simply cool}RBB $\bis{rb}$ is a
congruence on $\GL^*$. Apply \cor{two-tiered congruence}.

The other cases go likewise, except that in checking that $\GL^*$ is
simply RWB or RDB cool, one has to check that Clause 3 of \df{RWB
cool} is satisfied.  Let $u$ and $\sigma$ be a term and substitution
that satisfy Clause 3 for a rule
$\frac{H}{f(x_1,\ldots,x_n)\goto{a}t}$ with $f$ wild.  I claim that
$u^*$ and $\sigma$ are appropriate for the rule
$\frac{H}{f(x_1,\ldots,x_n)\goto{a}t^*}$, existing in $\GL^*$.
Namely, by a straightforward structural induction on $u$, if
\plat{\frac{K}{u\goto{a}v}} is an $\GL$-ruloid then
\plat{\frac{K}{u^*\goto{a}v^*}} is an $\GL^*$-ruloid. Moreover,
$\sigma(v)=t$ implies $\sigma(v^*)=t^*$. By construction, for every
premise $x \goto{c} y$ in $K$, $\GL^*$ has a rule
$\frac{\sigma(x)\goto{\tau}y}
{f(x_1,\ldots,x_n)\goto{\tau}\sigma(u^*[y/x])}$.
\end{proof}
As the above shows, for $X \mathbin\in \{W,D,B,H\}$, the RXB cool format is
exactly the two-tiered simply RXB cool format, so \thm{rooted weak}
is obtained as an application of \thm{two-tiered} to \thm{simply cool}.

\section{Comparison with Bloom's formats}\label{Bloom}

Not counting a host of notational differences, Bloom's definitions of the
cool formats differ in five ways from mine.

First of all Bloom requires \emph{bifurcation rules} for all operators
in $\GL^{tame}$, whereas I merely require patience rules for the
principal operators.  As principal operators in $\GL^{tame}$ are
straight, and bifurcation rules for straight operators are exactly
patience rules, the difference is that I dropped the bifurcation
requirement for abbreviations (non-principal operators). This is
possible, because by \df{two-tiered}, which corresponds to Definition
3.5.5 in \cite{Bl95}, the rules for the abbreviations are completely
determined by the rules for their straightenings, and it turns out
that a bifurcation rule of an abbreviation $f$ is exactly what is
determined by the corresponding patience rule for its straightening
$f^\star$.

Bloom's WB cool format requires the existence of bifurcation/patience
ruloids for receiving variables in any term, whereas I require them
for receiving arguments of operators, which is a more syntactic and
easy to check requirement.  The two approaches are shown equivalent
in \pr{cool} when using the extension of my formats of
Section~\ref{extension}, this being the reason behind that extension.

Bloom's WB and RWB cool formats use a so-called
\emph{$\varepsilon$-presentation}.  This entails that rules may have
premises of the form $x \goto{\varepsilon} y$. In terms of
\df{transition}, the meaning of such premises is given by the
requirement that $\sigma(x)=\sigma(y)$ for
\plat{(x\goto{\varepsilon}y)\in H}. By using $\varepsilon$-premises,
any rule can be given a form in which the target is a univariate term,
having no variables in common with the source. This allows a
simplification of the statement of the bifurcation ruloids. Any
$\varepsilon$-presented GSOS language can be converted to
$\varepsilon$-free form by substitution, in each rule $r$, $x$ for $y$
for every premise $x\goto{\varepsilon}y$ of $r$.

%\input{diagram}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \graphtemp=.5ex\advance\graphtemp by 0.085in
    \rlap{\kern 0.300in\lower\graphtemp\hbox to 0pt{\hss $s$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.085in
    \rlap{\kern 0.800in\lower\graphtemp\hbox to 0pt{\hss $t$\hss}}%
    \special{pn 8}%
    \special{ar 180 635 130 130 0 6.28319}%
    \special{sh 0.000}%
    \special{ia 300 585 85 85 0 6.28319}%
    \special{ar 920 635 130 130 0 6.28319}%
    \special{sh 0.000}%
    \special{ia 800 585 85 85 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.585in
    \rlap{\kern 0.300in\lower\graphtemp\hbox to 0pt{\hss $t_1$\hss}}%
    \special{pa 150 510}%
    \special{pa 245 520}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 148 485}%
    \special{pa 245 520}%
    \special{pa 143 534}%
    \special{pa 148 485}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.585in
    \rlap{\kern 0.800in\lower\graphtemp\hbox to 0pt{\hss $t_2$\hss}}%
    \special{pa 950 510}%
    \special{pa 855 520}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 957 534}%
    \special{pa 855 520}%
    \special{pa 952 485}%
    \special{pa 957 534}%
    \special{fp}%
    \special{pa 300 170}%
    \special{pa 300 500}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 325 400}%
    \special{pa 300 500}%
    \special{pa 275 400}%
    \special{pa 325 400}%
    \special{fp}%
    \special{pa 800 170}%
    \special{pa 800 500}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 825 400}%
    \special{pa 800 500}%
    \special{pa 775 400}%
    \special{pa 825 400}%
    \special{fp}%
    \special{pa 385 85}%
    \special{pa 715 85}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 615 60}%
    \special{pa 715 85}%
    \special{pa 615 110}%
    \special{pa 615 60}%
    \special{fp}%
    \special{pa 360 145}%
    \special{pa 740 525}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 687 437}%
    \special{pa 740 525}%
    \special{pa 652 472}%
    \special{pa 687 437}%
    \special{fp}%
    \special{pa 360 525}%
    \special{pa 740 145}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 652 198}%
    \special{pa 740 145}%
    \special{pa 687 233}%
    \special{pa 652 198}%
    \special{fp}%
    \special{pa 385 585}%
    \special{pa 715 585}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 615 560}%
    \special{pa 715 585}%
    \special{pa 615 610}%
    \special{pa 615 560}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.020in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.195in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.640in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.465in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.285in
    \rlap{\kern 0.240in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.285in
    \rlap{\kern 0.860in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.635in
    \rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.635in
    \rlap{\kern 1.100in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
    \hbox{\vrule depth0.765in width0pt height 0pt}%
    \kern 1.100in
  }%
}%
\noindent
\begin{minipage}[t]{5.2in}
\hspace{1.5em}%
Bloom's rendering of the RWB cool format doesn't feature Clause 4
(and in view of \pr{RWB cool}, neither does mine), but Clause 3 is
much more involved. For every rule with conclusion $s\goto{a}t$ Bloom
requires the existence of two terms $t_1$ and $t_2$ and seven types of
derived operational rules, such that the diagram\linebreak[2]\mbox{}
\end{minipage}
\vspace{-8pt}\hfill\raisebox{1.5em}[0pt][0pt]{\box\graph\,}
on the right commutes. My Clause 3 stems from the observation that,
given Bloom's other restrictions, $t$ necessarily has the rules
required for $t_2$, so that one may always choose $t_2=t$. This leaves
only $t_1$ (called $u$ in \df{RWB cool}) and three types of rules, one
of which (the $t_1$-loop in the diagram above) is in fact a
bifurcation rule whose existence is already implied by the
requirements of \df{cool}.

In Clause 3 of \df{RWB cool}, Bloom requires that
\begin{equation}\label{var(u)}
\var(u)=\{y'\mid y\!\in\!\var(t)\}\mbox{ and }
\sigma(y')=\left\{\begin{array}{@{}l@{}}x\mbox{ if $H$ contains
a premise \plat{x\goto{c}y}}\\y\mbox{ otherwise.}
\end{array}\right.
\end{equation}
In order to match Bloom's format I
could have done the same, but this condition is not needed in the
proof and reduces the generality of the format.

\begin{example}{bloom restrictive}
Consider the following GSOS language, with unary operators $f$
and $g$ and constant $0$.
$${f(x_1) \goto{b} x_1}~~~~~
  \frac{x_1 \goto{a} y_1}{f(x_1) \goto{a} 0}~~~~~
  \frac{x_1 \goto{\tau} y_1}{f(x_1) \goto{\tau} g(y_1)}~~~~~
  \frac{x_1 \goto{a} y_1}{g(x_1) \goto{a} 0}~~~~~
  \frac{x_1 \goto{\tau} y_1}{g(x_1) \goto{\tau} g(y_1)}$$
The sublanguage without $f$ is simply WB cool, and the entire language
simply RWB cool. In fulfilling Clause 3 of \df{RWB cool} take
for the first rule $u := f(x_1)$ and for the second and third rules
$u:= g(x_1)$, in each case with $\sigma$ the identity.

However, this language is not RWB cool in the sense of Bloom, as the
restriction above forbids rules $\frac{H}{s\goto{a}t}$ with
$H\neq\emptyset$ and $\var(t)=\emptyset$, where the operator in $s$ is wild.
\end{example}

\begin{proposition}{bloom}
A GSOS language is WB cool, respectively RWB, BB or RBB cool, as
defined here, with the extension of Section~\ref{extension} and the
restriction \mbox{\rm (\ref{var(u)})} above, iff it is WB cool, resp.\
RWB, BB or RBB cool, as defined in {\sc Bloom \cite{Bl95}}.
\end{proposition}
The proof consists of converting Bloom's rule formats to
$\varepsilon$-free form and eliminating a number of other notational
differences, together with the issues addressed above.\hfill$\Box$\vspace{1em}

Moreover, my proofs that cool languages are compositional for bisimulation
equivalences greatly simplify the ones of Bloom \cite{Bl95} by using a
reduction of the general case to the simple case, instead of treating
the general formats directly.

\section{Cool GSOS languages with lookahead}\label{lookahead}

The RWB cool format can be extended by allowing wild operators $f$,
besides GSOS rules satisfying Clause 3 of \df{RWB cool}, also to have
rules of which all premises have the form $x \dto\goto{c}y$ with $c\in
A$.  For such rules Clause 3 is not required, but in fulfilling
Clause 4, they do count in determining which arguments are
receiving. A similar extension applies to the RDB cool format.

\begin{definition}{GSOS with lookahead}
Let $\Sigma$ be a signature.  A \emph{GSOS rule with lookahead} is an
expression of the form \plat{\frac{H}{\alpha}} with $\alpha$ a
positive $\Sigma$-literal (the \emph{conclusion}) and $H$ a set of
expressions of the form \mbox{$x \dto\goto{a} y$} (the \emph{premises}
of the rule), satisfying the four conditions of \df{GSOS}. A
\emph{GSOS language with lookahead} is a TSS whose rules are either
GSOS rules or GSOS rules with lookahead. The transitions generated by
a GSOS language with lookahead $\GL$ are defined exactly as in
\df{transition}, where a premise $(x_i\dto\goto{c}y)\in H$ gives rise
to a hypothesis $p_i\dto_\GL\goto{c}_\GL \sigma(y)$, using the
relational composition of $\dto_\GL$ and $\goto{c}_\GL$.
The notion of a \emph{receiving} variable in term of \df{straight}
extends straightforwardly to GSOS languages with lookahead.
\end{definition}

\begin{definition}{RWB cool with lookahead}
A GSOS language with lookahead $\GL$ is \emph{RWB cool} if the
operators can be partitioned in \emph{tame} and \emph{wild} ones, such that
\begin{itemise}
\item[1.] the target of every rule contains only tame operations;
\item[2.] the sublanguage $\GL^{tame}$ of tame operators in $\GL$ is a
  WB cool GSOS language (without lookahead);
\item[3.] $\GL$ is positive, and for each GSOS rule
  \plat{\frac{H}{s\goto{a}t}} (without lookahead) there is a term $u$ and
  a substitution $\sigma:\var(u)\rightarrow \var(s)$ such that\vspace{-2pt}
  \begin{itemise2}
  \item there is an $\GL$-ruloid \plat{\frac{K}{u\goto{a}v}} with
    $\sigma(K)=H$ and $\sigma(v)=t$,
  \item and for every premise $x \goto{c} y$ in $K$, $\GL$ has a rule
    \plat{\frac{\sigma(x)\goto{\tau}y}
    {s\goto{\tau}\sigma(u[y/x])}};
  \end{itemise2}
\item[4.]
  if argument $f(i)$ of operator $f$ is receiving in $\GL$, then
  argument $i$ of $f^\star$ has a patience rule.
\end{itemise}
The format \emph{RDB cool} is defined likewise, adapting ``WB cool''
in the second clause to ``DB cool'', but skipping the last clause. The
\emph{simply RXB cool} rule formats (X$\in\!\!\{$W,D$\}$) are obtained by
requiring the sublanguage of tame operators to be simply XB cool.
\end{definition}
With these definitions, Lemmas RWB and RDB extend to the case that
$\GL$ is a GSOS language with lookahead, using premises
$x\dto\goto{x}y$ in case of GSOS rules with lookahead. Namely, the
statements quantify over rules in $\GL$; when such a rule is a GSOS
rule, the proof given in Section~\ref{rooted} applies, and when it is
a GSOS rule with lookahead, the statement follows from \df{GSOS with
lookahead} and \lem{receiving}.

\begin{theorem}{cool with lookahead}
On any RWB cool GSOS language with lookahead, $\bis{rw}$ is a congruence.

On any RDB cool GSOS language with lookahead, $\bis{rd}$ is a congruence.
\end{theorem}

\begin{proof}
Using the same argument as in the proof of \thm{cool} I may restrict
attention to simply RWB or RDB cool GSOS languages with lookahead.
Here the proof of Section~\ref{proofs} applies again.
\end{proof}

\begin{example}{communication merge}
Extend the GSOS language of \ex{CCS} with the binary operator $|$
\vspace{-3pt}
and the single rule $\frac{x_1 \dto\goto{a} y_1~~~
x_2 \dto\goto{\overline a} y_2}{x_1|x_2 \goto{\tau} y_1\|y_2}$.
This is the variant of the \emph{communication merge} of \cite{BK86a}
(cf.\ \ex{left-merge}), given in {\sc Bergstra \& Klop} \cite{BK85}
(and here again adapted to fit CCS rather then ACP$_\tau$).
The result is a GSOS language with lookahead, that moreover is RWB
cool. Thus $\bis{rw}$ and $\bis{rd}$ are congruences on this language.
In \cite{BK85} this variant of the communication merge is used as an
auxiliary operator in giving a finite complete equational
axiomatisation of $\bis{rw}$ on a language with $\|$; this is not
known to be possible using only auxiliary GSOS operators.
\end{example}

\section{Turning GSOS Rules into Equations}
\label{sec-equations}

This section recapitulates the method of \cite{ABV94} to provide
finite equational axiomatisations of $\bis{}$ on an augmentation of
any given GSOS language.

\begin{definition}{finite}
A process $p$, being a closed term in a GSOS language, is
\emph{finite} if there are only finitely many sequences of transitions
$p \goto{a_1} p_1 \goto{a_2} \cdots \goto{a_n} p_n$.
The length $n$ of the longest sequence of this form is called the
\emph{depth} of $p$.
\end{definition}

\begin{definition}{completeness}
An \emph{equational axiomatisation} Ax over a signature $\Sigma$ is
a set of equations $t=u$, called \emph{axioms}, with $t,u\in
\IT(\Sigma)$. It \emph{respects} an equivalence relation $\sim$ on
$T(\Sigma)$ if $\sigma(t)\sim\sigma(u)$ for any closed substitution
$\sigma:V\rightarrow T(\Sigma)$.

An \emph{instance} of axiom $t=u$ is an equation
$\sigma(C[t/x])=\sigma(C[u/x])$ where $\sigma$ is a substitution and
$C$ a term with $\var(C)\!=\!\{x\}$, and $x$ occurring only once in $C$.
An equation $p=q$ is \emph{derivable} from Ax, notation $p=_{\rm Ax}q$,
if there is a sequence $p_0,\ldots,p_n$ of terms with $n\geq 0$ such
that $p=p_0$, $q=p_n$ and for $i=1,\ldots,n$ the equation
$p_{i-1}=p_i$ is an instance of one of the axioms.

Ax is \emph{sound} for $\sim$ if $p=_{\rm Ax}q$ implies $p\sim q$
for $p,q\in T(\Sigma)$.
Ax is \emph{complete for $\sim$ on finite processes} if $p\sim q$
implies $p=_{\rm Ax}q$ for finite processes $p$ and $q$.
\end{definition}
Note that Ax is sound for $\sim$ iff Ax respects $\sim$ and $\sim$ is a
congruence.

\begin{definition}{basic}
A GSOS language $\GL$ \emph{extends BCCS} (\emph{basic} CCS) if it contains
the operators 0, $a.\_\,$ and $+$ of \ex{CCS}.
A \emph{basic process} is a closed term
build from the operators mentioned above only.
A \emph{head normal form} is a closed term
of the form $0 + a_1.p_1 + \cdots + a_n.p_n$ for $n\geq 0$.
An axiomatisation on $\GL$ is \emph{head normalising} if any term
$f(p_1,\ldots,p_{ar(f)})$ with the $p_i$ basic processes
can be converted into head normal form.
\end{definition}

\begin{proposition}{completeness}
\begin{table}[b]
\vspace{-.7em}
$$\begin{array}{@{}rcl@{~~~}l@{~~~~~~~~~}r@{~=~}l@{~~~{\rm CM}}c@{}}
x+(y+z)&=&(x+y)+z &{\rm A1}& x\|y  & \plat{x\leftmerge y + y\leftmerge x + x|y} &1\\
 x+y   &=& y+x    &{\rm A2}& \plat{a.x\leftmerge y} & a.(x\| y)        &2\\
 x+x   &=& x	  &{\rm A3}& \plat{0\leftmerge y}     & 0                       &3\\
 x+0   &=& x	  &{\rm A4}&\plat{(x+y)\leftmerge z}  &\plat{x\leftmerge z+y\leftmerge z}&4\\
        &&	  &        & a.x | \overline a.y & \tau.(x\|y)           &5\\
a.(\tau.(x+y)+x)&=&a.(x+y)&{\rm T1}& a.x|b.y  &
                        0~~~~~~~~~~~(\mbox{if }b\neq\overline a)&6\\
\tau.x+x&=&\tau.x &{\rm T2}& 0|x  & x|0 ~=~ 0                            &7\\
a.(\tau.x+y)+a.x&=&a.(\tau.x+y)&{\rm T3}&(x+y)|z&x|z+y|z  &8\\
&&	  &        & x|(y+z)           & x|y + x|z                       &9\\
\end{array}$$
\vspace{-.7em}
\caption{Complete equational axiomatisations of BCCS and the parallel
composition}\label{BCCS}
\end{table}
Let $\GL$ be a GSOS language extending BCCS, and {\rm Ax} a head
normalising equational axiomatisation, respecting $\bis{\!}$, and
containing the axioms {\rm A1--4} of Table~\ref{BCCS}. Then {\rm Ax} is
sound and complete for $\bis{\!}$ on finite processes.
\end{proposition}

\begin{proof}
Using induction on the depth of $p$ and a nested structural induction,
the axioms can convert any finite process $p$ into a basic process.
Here one uses that strongly bisimilar processes have the same depth.
Now apply the well-known fact that the axioms A1--4 are
sound and complete for $\bis{\!}$ on basic processes \cite{Mi90ccs}.
\end{proof}
For the parallel composition operator $\|$ of CCS no finite equational
head normalising axiomatisation respecting strong bisimulation
equivalence exists \cite{Mo90a}. However, {\sc Bergstra \& Klop}
\cite{BK86a} gave such an axiomatisation on the language obtained by
adding two auxiliary operators, the \emph{left merge}
$\leftmerge$\vspace{-1ex} and the \emph{communication merge} $|$, with
rules $\displaystyle \frac{x_1 \goto{a} y_1}{x_1 \leftmerge x_2
\goto{a} y_1\|x_2}$ and $\displaystyle\frac{x_1 \goto{a}
y_1~~~x_2 \goto{\overline a} y_2}{x_1|x_2 \goto{\tau} y_1\|y_2}$,
provided the alphabet $Act$ of actions is finite.  See
\ex{left-merge}. The axioms are CM1--9 of Table~\ref{BCCS}, in which +
binds weakest and $a.\_\,$ strongest, and $a,b$ range over $Act$.

{\sc Aceto, Bloom \& Vaandrager} \cite{ABV94} generalise this idea to
arbitrary GSOS languages with finitely many rules, each with
finitely many premises, and assuming a finite alphabet $Act$.  I
recapitulate their method for positive languages only.
A smooth
operator (\df{straight}) only has rules of the form $\displaystyle
\frac{\{x_i \goto{c_i} y_i \mid
i\!\in\!I\}}{f(x_1,\ldots,x_n)\goto{a}t}$.  The \emph{trigger} of such
a rule is the partial function $\uparrow_r:
\{i,\ldots,n\}\rightharpoonup Act$ given by $\uparrow_r(i)=c_i$ if
$i\!\in\!I$, and $\uparrow_r(i)$ is undefined otherwise.

\begin{definition}{distinctive}\cite{ABV94}
A smooth GSOS operator $f$ is \emph{distinctive}, if no two rules of
$f$ have the same trigger, and the triggers of all rules of $f$ have
the same domain.
\end{definition}
All operators of CCS, as well as \plat{\leftmerge} and $|$, are smooth.
The operators $0$, $a.\_\,$, \plat{\leftmerge} and $|$ are
distinctive, but $\|$ is not. Its triggers have
domains $\{1\}$, $\{2\}$ and $\{1,2\}$.

For every smooth and distinctive operator $f$,
{\sc Aceto, Bloom \& Vaandrager} declare four types of axioms.
First of all, for every rule $r$ as above there is an axiom
$f(\sigma(x_1),\ldots,\sigma(x_n))=a.\sigma(t)$, where
$\sigma:\{x_1,\ldots,x_n\}\rightarrow \IT(\Sigma)$ is the substitution
given by $\sigma(x_i)=c_i.y_i$ for $i\!\in\!I$ and $\sigma(x_i)=x_i$
for $i\!\not\in\!I$. Such an axiom is called an \emph{action law}.
Examples are CM2 and CM5 in Table~\ref{BCCS}.

Secondly, whenever $I$ is the set of active arguments of $f$, but $f$
has no rule of the form above (where the name of the variables $y_i$
is of no importance), there is an axiom
$f(\sigma(x_1),\ldots,\sigma(x_n))=0$, with $\sigma$ as above (for an
arbitrary choice of distinct variables $y_i$). Such an axiom is an
\emph{inaction law}.  An example is CM6. If $f$ has $k$ active
arguments, in total there are $|Act|^k$ action and inaction laws for
$f$, one for every conceivable trigger with as domain the active
arguments of $f$.

Finally, for any active argument $i$ of $f$, there are laws\vspace{-1ex}
\[ f(x_1,\ldots x_{i-1},0,x_{i+1},\ldots,x_n) = 0~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~\mbox{and}\]\vspace{-2em}
\[f(x_1,\ldots,x_i+x_i',\ldots,x_n) =
f(x_1,\ldots,x_i,\ldots,x_n) + f(x_1,\ldots,x_i',\ldots,x_n).\]
Examples for the second type of {inaction law} are CM3 and CM7,
and examples of \emph{distributivity laws} are CM4, CM8 and CM9.

It is not hard to see that all axioms above respect $\bis{}$ and that
together they bring any term $f(p_1,\ldots,p_{ar(f)})$ with the $p_i$
basic processes in head normal form.

The method of \cite{ABV94} makes three types of additions to a given
finite GSOS language $\GL$, and provides an equational head
normalising axiomatisation on the resulting language, that respects
strong bisimulation.

First of all, the operators $0$, $a.\_\,$ and $+$ are added, if not
already there. The corresponding axioms are A1--4 of
Table~\ref{BCCS}. If all other operators are smooth and distinctive, for
each of them the axioms just described are taken, which finishes the
job. (In the presence of negative premises, this step is slightly more
complex.)

In case there are operators $f$ that are smooth but not distinctive, the
set of operational rules of $f$ is partitioned into subsets $D$ such
that no two rules in $D$ have the same trigger, and the triggers of
all rules in $D$ have the same domain. Note that such a partition
can always be found---possibly by taking exactly one rule in each subset
$D$. Now for any subset $D$ in the partition, an operator $f_D$ with
$ar(f_D)=ar(f)$ is added to the language, whose rules are exactly the
rules in that subset, but with $f_D$ in the source. By definition,
$f_D$ is distinctive. Now add an axiom $f(x_1,\ldots,x_{ar(f)}) =
\sum f_D(x_1,\ldots,x_{ar(f)})$, where the sum is taken over all
subsets in the partition, and apply the method above to the operators
$f_D$. Again, it is trivial to check that the axioms respect $\bis{}$
and are head normalising.
Applied to the $\|$ of CCS, this technique yields the left merge and
communication merge as auxiliary operators, as well as a right
merge, and the axiom CM1.

In case of operators $f$ that are not smooth, a smooth operator
$f^\star$ is added to $\GL$, of which $f$ is an abbreviation
in the sense of \df{two-tiered} (cf.\ \ex{straightening}).
The treatment of $f^\star$ proceeds as above, and the project is
finished by the axiom $$f(p_1,...,p_{ar(f)})=f^\star(p_{f(1)},...,p_{f(ar(f^\star)))}).$$

Besides completeness for finite processes, using an infinitary
induction principle the method of \cite{ABV94} even yields
completeness for arbitrary processes. I will not treat this here, as
it does not generalise to weak equivalences.

\section{Turning Cool GSOS Rules into Equations}
\label{sec-cool-equations}

The method of \cite{ABV94} does not apply to $\bis{w}$, $\bis{d}$,
$\bis{\eta}$, and $\bis{b}$, because these equivalences fail to be
congruences for the $+$. However, Bloom \cite{Bl95} shows that the
method applies more or less verbatim to $\bis{rb}$. This section
observes that the same holds for $\bis{r\eta}$, and finds an
adaptation to yield finite equational axiomatisations of
$\bis{rw}$ (resp.\ $\bis{rd}$) that are sound and complete for finite
processes on an augmentation of any RWB cool (resp.\ RDB cool) GSOS
language.

On basic processes, the axioms A1--4 together with T1--T3 are complete
for $\bis{rw}$ \cite{Mi90ccs}, whereas complete axiomatisations for
$\bis{rd}$, $\bis{r\eta}$ and $\bis{rb}$ are obtained by dropping T3,
T2 or both, respectively \cite{GW96}. So in order to get
axiomatisations of these equivalences that are complete for finite processes,
all that is needed is head normalisation. The simplest approach is to
use the same head normalising axioms as in the previous section,
reasoning that axioms that respect $\bis{}$ surely respect a coarser
equivalence like $\bis{rb}$ or $\bis{rw}$.  The only way this approach
could fail is when the auxiliary operators generated by \cite{ABV94}
fail to be congruences for the equivalence relation at hand. The
operators $0$, $a.\_\,$ and $+$ are WB cool, and thus
unproblematic. As observed in \cite{Bl95}, for any RBB cool GSOS
language, the augmented language is also RBB cool. Namely, the new
operators do not show up in targets of new rules, so classifying all
auxiliary operators as wild is sufficient. Since the auxiliary
operators do not increase the collection of receiving arguments of
operators either, it follows likewise that for any RHB cool GSOS
language, the augmented language is also RHB cool. Hence one obtains

\begin{theorem}{RBB completeness}
The method of \cite{ABV94}, together with axiom T1 (and T3), yields
finite equational axiomatisations of $\bis{rb}$ (resp.\ $\bis{r\eta}$)
that are sound and complete for finite processes on an augmentation of
any RBB cool (resp.\ RHB cool) GSOS language.\hfill$\Box$
\end{theorem}
For $\bis{rw}$ and $\bis{rd}$ this approach fails. In particular,
these equivalences fail to be congruences for the communication merge,
as shown in \ex{left-merge}.
\begin{trivlist} \item[\hspace{\labelsep}\bf Conjecture.]\it
There exists no GSOS language including the parallel composition of
CCS and $\geq\!2$ visible actions that admits a finite equational
axiomatisation of weak bisimulation equivalence that is sound and
complete for finite processes.
\end{trivlist}
Nevertheless, such an axiomatisation was found by {\sc Bergstra \&
Klop} \cite{BK85}, using a variant of the communication merge that is
not a GSOS operator; cf.\ \ex{communication merge}. Their
axiomatisation of $\|$ is obtained from the one in Table~\ref{BCCS} by
requiring $a,b\neq\tau$ in CM6, and adding the axioms $\tau.x|y =
x|\tau.y = x|y$.  Here I generalise their approach to arbitrary RWB
cool (or RDB cool) GSOS languages.

In an RWB (or RDB) cool language, the smooth operators $f^\star$ that
are needed to axiomatise a non-smooth operator $f$ are unproblematic.
For tame operators $f$, they are already in the language, and for a
wild $f$ it is not hard to define them in such a way that the
augmented language remains RWB (or RDB) cool. Of the operators $f_D$
needed to axiomatise a non-distinctive operator $f$, those that have
exactly one active argument can be made to satisfy Clause 3 of \df{RWB
cool} by including the relevant $\tau$-rule in $D$. This applies to
the left merge, for example. All operators $f_D$ with another number
of active arguments cannot have $\tau$-premises, by Definitions~\ref{df-RWB cool}
and~\ref{df-cool}. These operators $f_D$ are replaced by counterparts
$f'_D$, obtained by replacing each premise $x\goto{c}y$ in a rule for
$f_D$ by $x\dto\goto{c}y$.  By \thm{cool with lookahead}, $\bis{rw}$ (or
$\bis{rd}$) is a congruence for $f'_D$.

\begin{lemma}{distinctive with lookahead}
For any processes $p_1,...,p_n$ one has
$f(p_1,\ldots,p_{ar(f)}) \bis{rd} \sum f'_D(p_1,\ldots,p_{ar(f)})$.
\end{lemma}

\begin{proof}
Suppose $\sum f'_D(p_1,\ldots,p_{ar(f)}) \goto{a} q$. Then there is a
$\frac{H'}{f'_D(x_1,...,x_n)\goto{a}t}$ and a closed substitution
$\sigma$ with $\sigma(x_i)=p_i$ for $i=1,...,n$ and $\sigma(t)=q$,
such that $p_i\dto\goto{c}_\GL\sigma(y)$ for $(x_i\dto\goto{c}y)$ in $H'$.
This rule has been constructed from a rule
$\frac{H}{f(x_1,...,x_n)\goto{a}t}$, where in $H$ the premises are of
the form $x_i\goto{c}y$. By Lemma RDB, one obtains
$f(p_1,\ldots,p_{ar(f)}) \dto\goto{a} q$.

That $f(p_1,\ldots,p_{ar(f)}) \goto{a} q$ implies $\sum
f'_D(p_1,\ldots,p_{ar(f)}) \goto{a} q$ follows straightforwardly.
\end{proof}
Now the required axiomatisation is obtained by omitting all inaction
laws for the modified operators $f'_D$ with $\sigma(x_i)=\tau.y_i$ for
some active argument $i$, and instead adding \emph{$\tau$-laws}
$$f'_D(x_1,\ldots,\tau.x_i,\ldots,x_n) = f'_D(x_1,\ldots,x_i,\ldots,x_n)$$
for each active argument $i$ of $f'_D$. One obtains

\begin{theorem}{RWB completeness}
The above adaptation of the method of \cite{ABV94}, together with
axioms T1, T2 (and T3), yields finite equational axiomatisations of
$\bis{db}$ (resp.\ $\bis{rw}$) that are sound and complete for finite
processes on an augmentation of any RDB cool (resp.\ RWB cool) GSOS
language.\hfill$\Box$
\end{theorem}

\section{Further work}\label{further}

The main contribution of Bloom's RBB cool format is the classification
of operators in wild and tame ones. In Fokkink \cite{Fok00b} this
classification is refined into a classification on the
\emph{arguments} of operators, thereby allowing operators that have
wild as well as tame arguments. This allows, for instance, capturing
the Kleene star within the format, which is not possible in the
approach presented here. Additionally, \cite{Fok00b} transcends beyond
the GSOS format, by allowing arbitrary terms in the left-hand side of
premises. This allows capturing recursive specification, by the method
of introducing constants rather than variable binding constructs.
In \cite{FGW06a} this work is generalised slightly further, using a
new method to establish congruence formats, while in \cite{FGW06b}
this method is applied to generalise the simply RHB cool format presented
here. Generalising the simply RWB and RDB cool formats along the same
line requires further work.

\section{A Challenge}\label{challenge}

All equivalences of \df{bisimulation} are congruences of the GSOS
language with rules\vspace{-1.5ex}
$$\frac{x_1\goto{a}y}{f(x_1)\goto{a}g(y)} ~~~~~
  \frac{x_1\goto{\tau}y}{g(x_1)\goto{\tau}g(y)} ~~~~~ g(x_1)\goto{\tau} !x_1$$
\vspace{-1ex}
$$\frac{x_1\goto{a}y}{!x_1\goto{a}y\|!x_1}~~~~~
  \frac{x_1 \goto{a} y_1}{x_1 \| x_2 \goto{a} y_1\|x_2}~~~~~
  \frac{x_2 \goto{a} y_2}{x_1 \| x_2 \goto{a} x_1\|y_2}$$
for $a\!\in\!Act$. Here, the operator $!x$ can be understood as a
parallel composition of infinitely many copies of $x$. The rules for
$f$, $g$ and $\|$ are WB cool, but the one for $!$ is not. It is not
even RBB safe in the sense of \cite{Fok00b}.\\[1ex]
{\bf Open problem.\,} Find a congruence format that includes the
language above.

%\bibliography{../../../lib/abbreviations,../../../lib/dbase,../../../lib/biblio/glabbeek,../../../lib/new}
\begin{thebibliography}{10}

\bibitem{ABV94}
{\sc L.~Aceto, B.~Bloom \& F.W. Vaandrager} (1994):
\newblock {\em Turning {SOS} rules into equations.}
\newblock {\sl Information and Computation} 111(1), pp. 1--52.

\bibitem{Bas96}
{\sc T.~Basten} (1996):
\newblock {\em Branching bisimulation is an equivalence indeed!}
\newblock {\sl Information Processing Letters} 58(3), pp. 141--147.

\bibitem{BK86a}
{\sc J.A. Bergstra \& J.W. Klop} (1986):
\newblock {\em Algebra of communicating processes.}
\newblock In J.W.~de Bakker, M.~Hazewinkel \& J.K. Lenstra, editors: {\sl Mathematics and Computer Science}, CWI Monograph 1, North-Holland, Amsterdam, pp. 89--138.

\bibitem{BK85}
{\sc J.A. Bergstra \& J.W. Klop} (1985):
\newblock {\em Algebra of communicating processes with abstraction.}
\newblock {\sl Theoretical Computer Science} 37(1), pp. 77--121.

\bibitem{Bl95}
{\sc B.~Bloom} (1995):
\newblock {\em Structural operational semantics for weak bisimulations.}
\newblock {\sl Theoretical Computer Science} 146, pp. 25--68.

\bibitem{BIM95}
{\sc B.~Bloom, S.~Istrail \& A.R. Meyer} (1995):
\newblock {\em Bisimulation can't be traced.}
\newblock {\sl Journal of the ACM} 42(1), pp. 232--268.

\bibitem{BHR84}
{\sc S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes.}
\newblock {\sl Journal of the ACM} 31(3), pp. 560--599.

\bibitem{Fok00b}
{\sc W.J. Fokkink} (2000):
\newblock {\em Rooted branching bisimulation as a congruence.}
\newblock {\sl Journal of Computer and System Sciences} 60(1), pp. 13--37.

\bibitem{FGW06a}
{\sc W.J. Fokkink, R.J. van Glabbeek \& P. de Wind} (2006):
\newblock {\em Divide and Congruence: From Decomposition of Modalities
  to Preservation of Branching Bisimulation.}
\newblock In F.S. de Boer, M.M. Bonsangue, S. Graf \& W.-P. de Roever,
  editors: Revised Lectures Fourth International Symposium on {\sl Formal
  Methods for Components and Objects}, FMCO 2005, Amsterdam,
  LNCS 4111, Springer, 2006, pp. 195-218.

\bibitem{FGW06b}
{\sc W.J. Fokkink, R.J. van Glabbeek \& P. de Wind} (2005):
\newblock {\em Divide and Congruence Applied to $\eta$-Bisimulation.}
\newblock In P. Mosses \& I. Ulidowski, editors:
  Proceedings of the Second Workshop on {\sl Structural Operational
  Semantics}, SOS 2005, Lisbon,
  {\sl Electronic Notes in Theoretical Computer Science} 156(1), pp. 97-113.

\bibitem{vG05}
{\sc R.J.~van Glabbeek} (2005):
\newblock {\em A characterisation of weak bisimulation congruence.}
\newblock In A.~Middeldorp, V.~van Oostrom, F.~van Raamsdonk \&
R.~de~Vrijer, editors: {\sl Processes, Terms and Cycles: Steps on the
Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion
of His 60th Birthday}, {\sl \rm LNCS} 3838, Springer, pp. 26--39.

\bibitem{GW96}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1996):
\newblock {\em Branching time and abstraction in bisimulation semantics.}
\newblock {\sl Journal of the ACM} 43(3), pp. 555--600.

\bibitem{Mi90ccs}
{\sc R.~Milner} (1990):
\newblock {\em Operational and algebraic semantics of concurrent processes.}
\newblock In J.~van Leeuwen, editor: {\sl Handbook of Theoretical Computer Science}, chapter~19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201--1242.
\newblock Alternatively see{ \em Communication and Concurrency}, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as{ \em A Calculus of Communicating Systems}, LNCS 92, Springer-Verlag, 1980.

\bibitem{Mo90a}
{\sc F.~Moller} (1990):
\newblock {\em The nonexistence of finite axiomatisations for {CCS} congruences.}
\newblock In {\sl Proceedings $5^{th}$ Annual Symposium on Logic in Computer Science, {\rm Philadelphia, USA}}, IEEE Computer Society Press, pp. 142--153.

\bibitem{OH86}
{\sc E.-R. Olderog \& C.A.R. Hoare} (1986):
\newblock {\em Specification-oriented semantics for communicating processes.}
\newblock {\sl Acta Informatica} 23, pp. 9--66.

\bibitem{Pl04}
{\sc G.D. Plotkin} (2004):
\newblock {\em A structural approach to operational semantics.}
\newblock {\sl The Journal of Logic and Algebraic Programming} 60--61, pp. 17--139.
\newblock Originally appeared in 1981.

\bibitem{dS85}
{\sc R.~de Simone} (1985):
\newblock {\em Higher-level synchronising devices in {{\sc Meije}-SCCS}.}
\newblock {\sl Theoretical Computer Science} 37, pp. 245--267.

\bibitem{Ul92}
{\sc I.~Ulidowski} (1992):
\newblock {\em Equivalences on observable processes.}
\newblock In {\sl Proceedings $7^{th}$ Annual Symposium on Logic in Computer Science, {\rm Santa Cruz, California}}, IEEE Computer Society Press, pp. 148--159.

\bibitem{UP02}
{\sc I.~Ulidowski \& I.~Phillips} (2002):
\newblock {\em Ordered {SOS} rules and process languages for branching and eager bisimulations.}
\newblock {\sl Information and Computation} 178(1), pp. 180--213.

\bibitem{UY00}
{\sc I.~Ulidowski \& S.~Yuen} (2000):
\newblock {\em Process languages for rooted eager bisimulation.}
\newblock In C.~Palamidessi, editor: {\sl {\rm Proceedings of the 11th International Conference on} Concurrency Theory{\rm, CONCUR 2000}}, {\sl \rm LNCS} 1877, Springer, pp. 275--289.

\end{thebibliography}
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
