\documentstyle[twoside,12pt]{article}
\pagestyle{myheadings}
% SIDE MARGINS:
\oddsidemargin -4.4mm % Left margin on odd-numbered pages.
\evensidemargin 3.6mm % Left margin on even-numbered pages.
% VERTICAL SPACING:
\topmargin -4mm % Nominal distance from top of page to top
% of box containing running head.
\headheight 13mm % No running headline, and no
\headsep 24pt % space between running headline and text.
% DIMENSION OF TEXT:
\textheight 230mm % Height of text part of page
\textwidth 160mm % Width of text part of page, i.e. of line
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% On American paper the right margin is 6 mm longer, %%%%
%%%% whereas the bottom margin is 17.6 mm smaller. %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside} \newlength{\shifttop}
\setlength{\shiftside}{3mm} \setlength{\shifttop}{-8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 1 for American paper or 0 for A4.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}
\renewcommand{\abstract}[1]{\begin{list}{}
{\rightmargin\leftmargin
\listparindent 1.5em
\parsep 0pt plus 1pt}
\small\item #1\end{list}}
\newtheorem{adefinizione}{Definition}[section]
\newtheorem{alemma}[adefinizione]{Lemma}
\newtheorem{ateorema}[adefinizione]{Theorem}
\newtheorem{acorollario}[adefinizione]{Corollary}
\newtheorem{aproposizione}[adefinizione]{Proposition}
\newenvironment{definizione}{\begin{adefinizione}\rm}{ \end{adefinizione}}
\newenvironment{lemma}{\begin{alemma}\rm}{\end{alemma}}
\newenvironment{teorema}{\begin{ateorema}\rm}{\end{ateorema}}
\newenvironment{corollario}{\begin{acorollario}\rm}{\end{acorollario}}
\newenvironment{proposizione}{\begin{aproposizione}\rm}{\end{aproposizione}}
\newcommand{\dimo}{\par\medskip\noindent{\bf Proof. }}
\newcommand{\deriv}[1]{{\mbox{${\:\stackrel{#1}{\rightarrow}\:}$}}}
\newcommand{\nderiv}[1]{{\mbox{${\not\stackrel{#1}{\longrightarrow}}$} }}
\newcommand{\spazio}{\mbox{ }}
\newcommand{\bigfrac}[2]{\begin{array}{c}#1\\\hline#2\end{array}}
\newcommand{\sem}[1]{\mbox{$[\! [#1]\! ]$}}
\newcommand{\fine}{\hfill{$\rule{2mm}{2mm}$}}
\newcommand{\para}{\mbox{$\,\parallel\!\!_{S}\,$}}
\newcommand{\sync}{\mbox{$\,\mid\!\!_{S}\,$}}
\newcommand{\refin}[1]{\mbox{$[a\leadsto#1]$}}
\newcommand{\rtom}{\mbox{$\gg$}}
\newcommand{\merge}[1]{\mbox{${\stackrel{#1}{\bowtie}}$}}
\newcommand{\lmerge}[1]{\mbox{${\stackrel{#1}{\lhd}}$}}
\newcommand{\rmerge}[1]{\mbox{${\stackrel{#1}{\rhd}}$}}
\newcommand{\nil}{\varepsilon}
\newcommand{\seq}{\cdot}
\newcommand{\name}[1]{\mbox{name($#1$)}}
\newcommand{\idx}[1]{\mbox{index($#1$)}}
\newcommand{\sg}[1]{\mbox{sg($#1$)}}
\newcommand{\incr}[1]{\mbox{inc($#1$)}}
\newcommand{\trans}[2]{f(#1,#2)}
\newcommand{\sk}{\mbox{skip}}
\newcommand{\M}{\mbox{\it Act}}
% ****************** Right Merge *****************************
\newcommand{\rp}
{\,\, \setlength{\unitlength}{1ex} \begin{picture}(1,1.75)
\put(0.45,0){\line(-1,0){1}}
\put(0,0){\line(0,1){1.75}}
\put(0.45,0){\line(0,1){1.75}}
\end{picture} \,}
%*************************************************************
\newcommand{\lpar}{\,\rp\!\!_{S}\,}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% vG's macro for open terms:
\newcommand{\opent}{\mbox{\sf T\hspace{-5.5pt}T}} % Open terms
% Alternative for those who have font msbm10:
% \newfont{\open}{msbm10 scaled\magstep1} % Openface letters
% \newcommand{\opent}{\mbox{\open T}} % Open terms as in Fokkink
%vG's macro for bisimulation:
\newcommand{\bisimm}[1]{ \; % bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}\,}
\newcommand{\bisim}{\bisimm{P'}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%Tex macro package by Vaughan Pratt for drawing character-sized objects%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcount\PLv\newcount\PLw\newcount\PLx\newcount\PLy\newdimen\PLyy\newdimen\PLX
\newbox\PLdot \setbox\PLdot\hbox{\tiny.} \def\scl{.08} % resettable scale
\def\PLot#1{\PLx`#1\advance\PLx-42\PLy\PLx\PLv\PLx\divide\PLy9\PLw\PLy\multiply
\PLw9\advance\PLx-\PLw\advance\PLx-4\PLy-\PLy\advance\PLy4\PLX=\the\PLx pt
\advance\PLyy\the\PLy pt\wd\PLdot=\scl\PLX\raise\scl\PLyy\copy\PLdot}
\def\draw#1{\ifx#1\end\let\next=\relax\else\PLot#1\let\next=\draw\fi\next}
%%%%%%%%%%%%%%%%%%%Polish a by Rob van Glabbeek%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\pa{\mbox{a\hspace{-2pt}\raisebox{-.7pt}% \pa Polish a
{\draw Wabcdefgh_VVM\end}\hspace{1pt}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{Axiomatising ST-Bisimulation Equivalence}
\author{
Nadia Busi$^{a}$ \thanks{The first and third authors have been supported by
CNR, MURST and Esprit project 8130 LOMAPS.}
\and Rob van Glabbeek$^{b}$ \thanks{The second author has been
funded by ONR under grant number N00014-92-J-1974.}
\and Roberto Gorrieri$^{c}$ $^{*}$
\date{\small
$^{a}$Dipartimento di Matematica, Universit\`{a}
di Siena \\
Via del Capitano, 15, I-53100 Siena, Italy \\
e-mail: busi@cs.unibo.it \\
\vspace{.2cm}
$^{b}$Computer Science Department, Stanford University\\
Stanford, CA 94305, USA\\ e-mail: rvg@cs.stanford.edu \\
\vspace{.2cm}
$^{c}$Dipartimento di Matematica, Universit\`{a}
di Bologna \\
Piazza di Porta S. Donato 5, I-40127 Bologna, Italy \\
e-mail: gorrieri@cs.unibo.it \\
}}
\begin{document}
\bibliographystyle{plain}
\maketitle
\abstract{
A simple ST operational semantics for a process algebra is provided, by
defining a set of operational rules in Plotkin's style.
This algebra comprises TCSP parallel composition, ACP sequential composition
and a refinement operator, which is used for replacing an action with an
entire process, thus permitting hierarchical specification of systems.
We prove that ST-bisimulation equivalence is a congruence, resorting
to standard techniques on rule formats. Moreover, we provide a set of
axioms that is sound and complete with respect to ST-bisimulation.
The intriguing case of the forgetful refinement (i.e.\ when an action is
refined into the properly terminated process) is dealt with in a new,
improved manner.
}
\section{Introduction}
Among the non-interleaving equivalences, one of the most relevant is
ST-bisimulation equivalence, originally proposed in \cite{GlaVaan}
over Petri Nets, from which it takes the name (S and T are the initials of
the German words for Place and Transition).
This semantics drops the assumption that actions are {\em atomic}
activities, hence, unobservable in the middle of their evolution.
This is implemented by splitting every action in two distinct phases: the
{\em beginning} and the {\em ending} which, instead, are considered atomic.
Additionally, in order to prevent possible confusion in the presence of
autoconcurrent actions, every ending phase is unambiguously related to
its own beginning phase through some supplementary information.
In the version of ST semantics we exploit, a causal link connects every ending
phase to the corresponding beginning phase \cite{GorLan}. This is achieved by
equipping each ending phase of an action with a ``relative pointer'' to
indicate the number of phases which have occurred from the beginning of
that action.
ST semantics expresses an elementary form of duration,
as many action phases can be executed in between a beginning and its end.
Moreover, ST semantics is {\em the} semantics for the operation of {\em action
refinement}. This operation substitutes the execution of a process for
an action, thereby
introducing the possibility of relating descriptions of the same system
at different levels of detail.
It has been extensively studied in the semantic domain
of event structures \cite{GlGo2,DaDe}, where an event is replaced by
a whole structure.
ST-bisimulation equivalence has been proved to be a congruence for this
operation in \cite{Glabbeek} and the coarsest congruence contained in
interleaving bisimulation in \cite{Vog}.
In this paper, we define an ST operational semantics in SOS style \cite{Plotkin}
for a process algebra equipped with the TCSP parallel composition
operator, the ACP sequential composition operator and the refinement one.
The transition system we define is labelled on action phases; hence, two
agents are ST-bisimulation equivalent if their corresponding states are
strongly bisimilar.
The transition system specification (TSS, for short) we propose fits the
{\em tyft} format of \cite{GroVaan}. Therefore, we can exploit a nice result
of that paper, namely that strong bisimulation is a congruence.
Then, we provide a sound and complete axiomatization for
ST-bisimulation: to obtain this, we conservatively extend the TSS by adding
some auxiliary operators, following the lines of the algorithm defined in
\cite{Aceto}.
We claim that the operational description we provide for the operator of
action refinement is in perfect agreement (apart from the way the empty
refinement is dealt with) with the denotational one in terms of flow event
structures described in \cite{GlGo2}. Our claim is based on
a similar proof, provided in \cite{Busi}, where a slightly different
language and a slightly different version of ST semantics are considered.
We argue that our way of dealing with the empty refinement, which can
be useful in applications \cite{GlGo2}, is more
satisfactory than the one of \cite{GlGo1}, and that event structures
are not expressive enough to model this type of refinement.
\section{Labelled Transition Systems}
We recall the basic, relevant notions about transition system specification
from \cite{GroVaan}, incorporating a recent improvement reported
in \cite{Fok,vGamast}.
Let $V$ be a denumerable set of variables; $x$, $y$, $z$ are typical
elements of $V$.
A single sorted signature $\Sigma$ is a pair $(F, \sharp)$, where $F$ is a
set of function names disjoint with $V$, and $\sharp:F\rightarrow\omega$
is a rank function which gives the arity of a function name.
With $\opent(\Sigma)$ and $T(\Sigma)$ we denote the set of open and
closed terms respectively over signature $\Sigma$. $V(t)\subseteq V$
denotes the set of variables in a term $t$. A substitution $\sigma$ is a
mapping $V\rightarrow \opent(\Sigma)$, extended homomorphically to
terms.
%The composition of substitutions $\sigma\circ\rho$ is defined by:
%$\sigma\circ\rho(x) = \sigma(\rho(x))$ for $x\in V$.
\begin{definizione}
A {\em transition system specification} (TSS) is a triple $(\Sigma, A, R)$
with $\Sigma$ a signature, $A$ a set of labels and $R$ a set of rules of the
form
$\bigfrac{\{t_{i}\deriv{a_{i}}t'_{i}\mid i\in I\}}{t\deriv{a}t'}$
with $I$ an index set, $t_{i}, t'_{i}, t, t'\in
\opent(\Sigma)$, $a_{i}, a\in A$ for $i\in I$.
\fine
\end{definizione}
If $r$ is a rule satisfying the above format, then the elements of
$\{t_{i}\deriv{a_{i}}t'_{i}\mid i\in I\}$ are called the {\em premises}
of $r$ and $t\deriv{a}t'$ is called the {\em conclusion} of $r$.
A rule of the form $\frac{\emptyset} {t\deriv{a}t'}$ is called an
axiom, which, if no confusion can arise, is also written as $t\deriv{a}t'$.
An expression of the form $t\deriv{a}t'$ with $a\in A$ and
$t,t'\in \opent(\Sigma)$ is called a transition (labelled with $a$).
The letters $\phi$, $\psi$, $\chi$ are used to range over transitions.
The notions `substitution', `$V(\cdot)$' and `closed' extend to
transitions and rules as expected.
\begin{definizione}
Let $P = (\Sigma, A, R)$ be a TSS. A {\em proof} of a transition $\psi$
from $P$ is a well-founded, upwardly branching tree of which the nodes are
labelled by transitions $t\deriv{a}t'$ with $t, t'\in \opent(\Sigma)$ and
$a\in A$, such that: the root is labelled with $\psi$, and if $\chi$ is
the label of a node $q$ and $\{\chi_{i}\mid i\in I\}$ is the set of
labels of the nodes directly above $q$, then there is a rule
$\bigfrac{\{\phi_{i}\mid i\in I\}}{\phi}$ in $R$ and a substitution
$\sigma$ such that $\chi = \sigma(\phi)$ and $\chi_{i} = \sigma(\phi_{i})$
for $i\in I$.
If there exists a proof of $\psi$ from $P$, then $\psi$
is {\em provable} from $P$ (notation $P\vdash\psi$).
\fine\end{definizione}
\begin{definizione}
A {\em labelled transition system (LTS)} is a structure $(S, A,
\rightarrow)$ where $S$ is a set of {\em states}, $A$ an {\em alphabet}, and
$\rightarrow\subseteq S\times A \times S$ a {\em transition relation}.
We write $t\deriv{a}t'$ to indicate that $(t,a,t')\in\rightarrow$.
\fine\end{definizione}
\begin{definizione}
Let ${\cal A} = (S, A, \rightarrow)$ be an LTS. A relation $R\subseteq
S\times S$ is a {\em (strong) bisimulation} if it
satisfies:
\begin{itemize}\vspace{-2ex}
\item
if $(s,t)\in R$ and $s\deriv{a}s'$, then there exists $t'\in S$
with $t\deriv{a}t'$ and $(s',t')\in R$;\vspace{-2ex}
\item
if $(s,t)\in R$ and $t\deriv{a}t'$, then there exists $s'\in
S$ with $s\deriv{a}s'$ and $(s',t')\in R$.\vspace{-2ex}
\end{itemize}
Two states $s,t\in S$ are {bisimilar} in ${\cal A}$, notation ${\cal A}:
s \bisimm{} t$,
if there exists a bisimulation containing the pair $(s, t)$. Note that
bisimilarity is an equivalence relation.
\fine
\end{definizione}
\begin{definizione}
Let $P = (\Sigma, A, R)$ be a TSS. The transition system $TS(P)$
specified by $P$ is the triple
$TS(P) = (T(\Sigma), A, \rightarrow_{P})$
where the relation $\rightarrow_{P}$ is defined by: $t\deriv{a}_{P}\,t'$ iff
$P\vdash t\deriv{a}t'$.
We say that two terms $t, t'\in T(\Sigma)$ are ($P$-)bisimilar, notation
$t\bisimm{P} \, t'$, if $TS(P): t\bisimm{} t'$.
We write $t\bisimm{} t'$ if it is clear from the context what $P$ is.
\fine\end{definizione}
TSSs do not always generate LTSs for which bisimulation is a
congruence, but they do if their rules satisfy the format below.
\begin{definizione}
Let $\Sigma = (F,\sharp)$ be a signature and let $P = (\Sigma, A, R)$ be a TSS.
A rule in $R$ is in {\em tyft format} if it has the form
$\bigfrac{\{t_{i}\deriv{a_{i}}y_{i}\mid i\in I\}}{f(x_{1},
\ldots,x_{\sharp(f)})\deriv{a} t}$
with $f$ a function name from $F$, $x_{i}$ $(1\leq
i\leq \sharp(f))$ and $y_{i}$ $(i\in I)$ are all different variables,
$a_{i}, a\in A$ and $t_{i}, t\in \opent(\Sigma)$ for $i\in I$.
$P$ is in {\em tyft} format if all the rules in $R$ are in {\em tyft} format.
\fine
\end{definizione}
\begin{teorema}
Let $\Sigma = (F,\sharp)$ be a signature and $P = (\Sigma,A, R)$ a TSS.
If $P$ is in {\em tyft} format then strong
bisimulation is a congruence for all function names in $F$.
\fine
\end{teorema}
\pagebreak
\begin{definizione}
Let $P = (\Sigma, A, R)$ be a TSS and let $r$ be a rule in $R$.
The {\em bound} variables of $r$ are recursively defined as the ones that
occur in the left hand side of the conclusion or in the right hand
side of a premise $t\deriv{a}t'$, where $t$ contains bound variables only.
A rule $r$ is {\em pure} if all variables that occur in it are bound.
The TSS $P$ is called pure if all rules in $R$ are pure.
\fine
\end{definizione}
Given two TSSs $P_{0}$ and $P_{1}$ we use $P_{0}\oplus P_{1}$ to denote
their componentwise union, which is only defined if function names that
occur in both the signatures of $P_{0}$ and $P_{1}$ are given the same
arity. If $P_{0}$ and $P_{1}$ are in {\em tyft} format and
some other conditions are satisfied, we have that the outgoing transitions
in
the transition system defined by $P_{0}$ of terms in the signature of
$P_{0}$ are the same as the outgoing transitions of these terms in the
transition system defined by $P_{0}\oplus P_{1}$.
\begin{definizione}
Let $P_{i} = (\Sigma_{i}, A_{i}, R_{i})$ $(i=0,1)$ be two TSSs with $P =
P_{0}\oplus P_{1}$ defined. Let $P = (\Sigma, A, R)$. We say that $P$ is a
{\em conservative extension} of $P_{0}$ and that $P_{1}$ can be added
conservatively to $P_{0}$ if for all $t\in
T(\Sigma_{0})$, $a\in A$ and $t'\in
T(\Sigma)$:
\vspace{.3cm}
\noindent \hfill
$P\vdash t\deriv{a}t' \; \Longleftrightarrow \; P_{0}\vdash t\deriv{a}t'$
\fine
\end{definizione}
Note that if $P$ is a conservative extension of $P_{0}$, $P$ is also a
conservative extension up to bisimulation, i.e.\ for $t,t'\in
T(\Sigma_{0})$:
$t\bisimm{P} \, t' \; \Longleftrightarrow \; t\bisimm{P_{0}} \, t'$.
\begin{teorema}
Let $P_{0} = (\Sigma_{0}, A_{0}, R_{0})$ be a TSS in pure {\em tyft} format and
let $P_{1} = (\Sigma_{1}, A_{1}, R_{1})$ be a TSS in {\em tyft} format such
that no rule of $R_{1}$ contains a function name from $\Sigma_{0}$ in the
source of its conclusion. Let $P = P_{0}\oplus P_{1}$ be defined. Then $P_{1}$
can be added conservatively to $P_{0}$.
\fine
\end{teorema}
\section{The Language}
Let $\M$ be a countable set of actions;
$a, b, c, d$ range over $\M$ and $S$ over the subsets of $\M$.
The process terms are generated by the following syntax:
\[t ::= \nil\mid\delta\mid a\mid t\seq t'\mid t+t'\mid t\para t'\mid
t\refin{t'}\]
Intuitively, $\nil$ is the successfully terminated process,
whereas $\delta$ is the deadlocked process. The operators $\seq$ and $+$
are the ACP sequential and alternative composition, respectively.
With $\para$ we mean the TCSP parallel composition, where synchronisation
over actions in $S$ is required\footnote{One could consider also more
general parallel operators, like the ACP one. Our work can be easily
adapted to ACP and similar languages.}. When set $S$ is empty (i.e.\ when
no synchronization is allowed), we usually omit the subscript $S$ in
$\para$. Finally $\refin{}$ is the refinement operator as defined
e.g.\ in \cite{DegGor}.
Recursion can be added and modelled in our operational approach in the
usual way (see \cite{GorLan2} for a possible operational ST semantics
for recursion).
However, as our main concern is the axiomatisation, we prefer to
restrict our attention to the finite calculus above.
\section{Operational Semantics}\label{operational}
To define the operational semantics, we need a more generous
signature to represent the states.
Let $k$ range over integers.
Let $\Sigma = (F,\sharp)$, where
\[\begin{array}{rcl}
F & = & \{\nil, \delta, +, \seq\} \cup \{a\mid a\in \M\} \cup
\{a^{1} \mid a\in \M\} \cup \{[k]\mid k\neq 0\}\\
& & \cup \{\para\mid S\subseteq\M\} \cup
\{\refin{}\mid a\in \M\}\cup \{\merge{k}\mid k>0\}\\
\multicolumn{3}{l}{\sharp(\nil) = \sharp(\delta) = \sharp(a) =
\sharp(a^{1}) = 0} \\
\multicolumn{3}{l}{\sharp([k]) = 1} \\
\multicolumn{3}{l}{\sharp(+) = \sharp(\seq) = \sharp(\para) =
\sharp(\refin{}) = \sharp(\merge{k}) = 2}
\end{array}\]
As any action is split in two phases, we need a unary operator to
represent the state of its intermediate execution.
An action $a$ performs its beginning (denoted, with abuse of notation,
$a$ as well), reaching $a^1$. This performs the ending of the action
$a$, where the superscript $1$ states that this ending refers to the
just performed transition. In general, the
causal pointer from an ending to its beginning is implemented as a
superscript number $k$ stating that its beginning has been executed $k$
transitions before.
The {\em delay} operator $[k]$ suitably updates the pointers. It will be
introduced in a context of parallel composition and refinement.
The {\em merge} operator $\merge{k}$ is used when merging the executions
of a refined agent and the activated refining agent. Intuitively,
it is a restricted form of parallel composition, as illustrated
in Section 6.
Let $\M^{\omega} = \{\mu^{k}\mid\mu\in \M\wedge k>0 \}$ be the
set of {\em endings};
let $\M_{ST} = \M\cup \M^{\omega}$ be the set of {\em phases},
where a label in $\M$ is called a {\em beginning};
$\eta$ ranges over $\M_{ST}$
and $\theta$ ranges over $\M_{ST}\cup\{\surd\}$, where action $\surd$
(sometimes called ``tick'') denotes clean termination.
Let $P = (\Sigma, A, R)$ be the TSS where $A = \M_{ST}\cup\{\surd\}$
and $R$ is the set of rules listed in Table \ref{rules}
commented upon below.
The auxiliary functions used in the rules are defined in
Table~\ref{func}.
\begin{table}[htb]
{\renewcommand{\arraystretch}{1.4}
\[\begin{array}{|l|}
\hline
\begin{array}{@{}l|l|l@{}}
\name{a} = a & \idx{a} = 0 & \trans{a}{k} = a\\
\name{a^{k}} = a & \idx{a^{k}} = k & \trans{a^{h}}{k} = \left\{
\begin{array}{@{}ll@{}}
a^{h+sg(k)} & \mbox{ if }h\geq |k| \\
a^{h} & \mbox{ otherwise }
\end{array}\right.\\
\name{\surd} = \surd~~ & & \trans{\surd}{k} = \surd
\end{array}\\
\hline
\begin{array}{@{}l|l@{}}
\sg{k} = \left\{
\begin{array}{ll}
1 & \mbox{ if }k>0 \\
- 1 & \mbox{ if }k<0
\end{array}\right.\hspace{1.1cm} &
\incr{k} = k + sg(k)
\end{array}\\
\hline
\end{array}\]}\vspace{-1ex}
\caption{Auxiliary functions on action phases} \label{func}
\end{table}
The functions name and index are intuitively clear. They extract from
a label the name of the action and the associated index, respectively.
Function $\sg{k}$ returns the sign of the integer $k$, while
$\incr{k}$ increases the absolute value of $k$. Finally, function $f$
updates the index of the label to which it is applied.\footnote{From
the definition of $f$ we cannot exclude to obtain action endings with
a zero or negative index. However, we have that terms reachable from
elements of the language contain positive indexes only.}
\begin{table}[hp]
{\renewcommand{\arraystretch}{1.4}
\[\begin{array}{|c|}
\hline
\begin{array}{lcllcl}
(ACT1) & a\deriv{a}a^{1} &
(ACT2) & a^{1}\deriv{a^{1}}\nil &\\
(TICK) & \nil\deriv{\surd}\delta &
(DELAY) & \bigfrac{x\deriv{\theta}x'}
{[k]x\deriv{\trans{\theta}{k}}[\incr{k}]x'} & \\
(SEQ1) & \bigfrac{x\deriv{\eta}x'}{x\seq y\deriv{\eta}x'\seq
y}\hspace{1cm} &
(SEQ2) & \bigfrac{x\deriv{\surd}x' \spazio y\deriv{\theta}y'}{x\seq
y\deriv{\theta} y'} &\\
(ALT1) & \bigfrac{x \deriv{\theta} x'} {x + y \deriv{\theta}
x'} &
(ALT2) & \bigfrac{y \deriv{\theta} y'} {x + y \deriv{\theta}
y'} &
\end{array} \\
\begin{array}{lcl}
(PAR1) & \bigfrac{x \deriv{\eta} x'} {x \para y \deriv{\eta} x'\para
[1]y} &
\name{\eta}\not\in S \\
(PAR2) & \bigfrac{y \deriv{\eta} y'} {x \para y \deriv{\eta} [1]x\para
y'} &
\name{\eta}\not\in S \\
(PAR3) & \bigfrac{x \deriv{\theta} x'\spazio y \deriv{\theta} y'} {x
\para y \deriv{\theta} x'\para y'} & \name{\theta}\in
S\cup\{\surd\}
\end{array}\\
\hline
\begin{array}{lcl}
(REF1) & \bigfrac{x \deriv{\theta} x'} {x \refin{y} \deriv{\theta}
x'\refin{y}} & \theta \neq a\\
(REF2) & \bigfrac{x \deriv{a} x'\spazio y \deriv{\eta} y'}
{x\refin{y}\deriv{\eta} x'\refin{y}\merge{1} y'} &\\
(REF3) & \bigfrac{x\deriv{a}x'\spazio x'\deriv{a^{1}}x''\spazio
[-1][-1](x''\refin{y})\deriv{\theta}x''' \spazio
y\deriv{\surd}y'}{x\refin{y}\deriv{\theta}x'''}\hspace{-40.89372pt} &
\\
(MERGE1) & \bigfrac{x \deriv{\eta} x'} {x\merge{k} y
\deriv{\eta} x'\merge{k+1}[1]y} & \idx{\eta}\neq k\\
(MERGE2) & \bigfrac{y \deriv{\eta} y'} {x\merge{k} y \deriv{\eta}
[1]x\merge{k+1} y'} &\\
(MERGE3) & \bigfrac{x \deriv{a^{k}} x'\spazio [-1]x'
\deriv{\theta} x''\spazio y\deriv{\surd}y'} {x\merge{k}y
\deriv{\theta} x''} &
\end{array} \\
\hline
\end{array}\]
}
\caption{Rules for basic operators} \protect\label{rules}
\end{table}
Axiom $({\it ACT}1)$ represents the starting of an action, while $({\it
ACT}2)$
accounts for the execution of the ending. $({\it TICK})$ is the rule for
the term $\nil$, which performs $\surd$ and terminates.
The rules for sequential and alternative composition are
standard (see e.g.\ \cite{GroVaan}).
The rules for the TCSP-like parallel composition are almost standard.
According to $({\it PAR}1)$, the asynchronous execution of a phase
from the left subagent can be performed if this phase is part of an
action not in the synchronisation set $S$; note, however, that the
right subagent is
delayed (i.e.\ the delay $[1]$ operator is applied to it), because
the pointers of all ending phases it will execute that point back to
before the current state must be incremented by one, as they refer to
transitions which are one step further back.
Rule $({\it PAR}3)$ needs no delay as
both subagents take part in the synchronisation; note that the
termination signal $\surd$ can only be performed synchronously by the
two subagents. The rule for the delay operator might appear a bit
clumsy, as it works for integers $k$ which can also be negative. A
negative delay is needed when skipping some transitions, as now
the pointers are to be decreased. The operator $[k]$ increments
pointers by 1 if $k$ is positive; it decrements by 1 if $k$ is
negative. Thus decrementing by $2$ needs to be expressed as
$[-1][-1]$; not as $[-2]$. The value of $|k|$ specifies {\em which}
pointers need to be adapted; namely all pointers that point back at
least $k$ phases before the current state.
More interesting are the rules for refinement. Rule $(REF1)$ accounts
for the case when the performed phase belongs to an action which is not
to be refined. On the contrary, $(REF2)$ states that whenever the agent
under refinement, $x$, starts the execution of the action to be refined,
$a$, then $x[a\leadsto y]$ performs the first, non tick, phase the
refining agent $y$ is able to do; the reached state is the merge of the
two subagents, where the parameter $1$ of the merge operator
remembers the index of the ending phase of the refined action.
Particular care should be devoted to rule $(REF3)$ which deals with the
case when $y$ can properly terminate, as in the so-called {\em empty}
refinement $\refin{\nil}$ (see Section 6 for a longer discussion). If
$x$ is ready to
start the execution of $a$, then it will complete it, becoming $x''$,
and then we will take the first transition the refinement of $x''$ is
able to do, remembering to update the pointers, as we have skipped two
transitions (the one for $a$ and the other for $a^1$).
The three rules for the merge operator state that the refined agent
$x$ can always perform a phase asynchronously, provided that this phase
is not the ending of the action which has been refined (see rule
$({\it MERGE}1)$ with its side condition); that the refining agent can
proceed
without any constraint (see rule $({\it MERGE}2)$); and that the merged
execution of the two ends when $x$ is ready to perform the ending of
the refined action and $y$ can terminate properly.
It is worth-while observing that the transitions are labelled
with parameters that range over actions and natural numbers,
and not directly with actions, as required by the {\em tyft} format;
so, every rule in our TSS is a rule schema corresponding to an
infinite set of rules.
\begin{proposizione}
$P$ is pure and in {\em tyft} format.
Strong bisimulation is a congruence for all function names in $F$.
\fine
\end{proposizione}
\section{Axiomatisation}\label{axiomatisation}
In this section we introduce a set of auxiliary operators; then we define
an axiomatisation and prove its soundness and completeness with respect
to bisimulation.
\subsection{Auxiliary Operators}
First we introduce a set of auxiliary operators, that are necessary to
obtain the axiomatisation.
Let $\Sigma' = (F', \sharp')$, where:
\[\begin{array}{rcl}
F'& =& F \cup \{a^{+}\mid a\in \M\}\cup \{a^{k}\mid a\in \M\wedge
k\geq 2\}\\
&&\cup \{\lpar, \sync\mid S\subseteq\M\} \cup
\{\lmerge{k}, \rmerge{k}\mid k>0\}\cup \{\rtom\} \\
\multicolumn{3}{l}{\mbox{if $f\in F$ then $\sharp'(f) = \sharp(f)$}} \\
\multicolumn{3}{l}{\sharp'(a^{+}) = \sharp'(a^{k}) = 0} \\
\multicolumn{3}{l}{\sharp'(\lpar) = \sharp'(\sync) =
\sharp'(\lmerge{k}) = \sharp'(\rmerge{k}) = \sharp'(\rtom) = 2}
\end{array}\]
In this setting, it is essential to introduce a syntactical
distinction between actions and beginnings. To this aim, we introduce
the auxiliary beginnings of the form $a^+$, which can perform the
beginning $a$ and then terminate successfully. The operators of the
form $a^k$, for any $k \geq 2$, are needed as
we have labels of this kind in the operational rules of the previous
section. The left-parallel $\lpar$ and the synchronisation-parallel
$\sync$ are useful for the axiomatisation of the parallel operator
$\para$. They play the same r\^ole as the left-merge and communication
merge of ACP \cite{BK-ACP}. However, whereas the left-merge of \cite{BK-ACP}
insists that the first {\em action} in a parallel composition comes from the
argument on the left, our $\lpar$ only insists that the first {\em
phase}
comes from the argument on the left. As far as the mnemonics concerns,
$\lpar$ points to the {\em left}, whereas the left merge is shaped
like an L\@; there is no need for a right-merge here.
The auxiliary operators $\lmerge{k}$ and $\rmerge{k}$ play a similar
r\^ole in the axiomatisation of the $\merge{k}$. Due to the
asymmetry between the refined and the refining process both are needed
here. $\rtom$ is used to axiomatise the refinement operator.
Let $P' = (\Sigma', A, R')$ a TSS,
where $R'$ is the set of rules listed in
Tables \ref{rules} and \ref{rulesAux}.
\begin{table}[htb]
{\renewcommand{\arraystretch}{1.4}
$$\begin{array}{|c|}
\hline
\begin{array}{lclc}
(ACT3) & a^{+} \deriv{a} \nil &
(ACT4) & a^{k} \deriv{a^{k}} \nil \hspace{2cm} k>1 \\
(RTOM1) & \bigfrac{y \deriv{\eta} y'} {x\rtom y \deriv{\eta}
x\merge{1} y'} &
(RTOM2) & \bigfrac{x \deriv{a^{1}} x'\spazio [-1][-1]x'
\deriv{\theta} x''\spazio y\deriv{\surd}y'} {x\rtom y
\deriv{\theta} x''} \\
(RME1) & \bigfrac{y \deriv{\eta} y'} {x\rmerge{k} y \deriv{\eta}
[1]x\merge{k+1} y'} &
(RME2) & \bigfrac{x \deriv{a^{k}} x'\spazio [-1]x'
\deriv{\theta} x''\spazio y\deriv{\surd}y'} {x\rmerge{k}y
\deriv{\theta} x''} \\
\end{array}
\\
\begin{array}{lcl}
(LME) & \bigfrac{x \deriv{\eta} x'} {x\lmerge{k} y
\deriv{\eta} x'\merge{k+1}[1]y} & \idx{\eta}\neq k\\
(LPAR) & \bigfrac{x \deriv{\eta} x'} {x \lpar y \deriv{\eta}
x'\para [1]y} & \name{\eta}\not\in S \\
(SYNC) & \bigfrac{x \deriv{\theta} x'\spazio y \deriv{\theta} y'}
{x \sync y \deriv{\theta} x'\para y'} & \name{\theta}\in
S\cup\{\surd\} \\
\end{array}\\
\hline
\end{array}$$\vspace{-3ex}
\caption{Rules for auxiliary operators}\label{rulesAux}
}
\end{table}
The only rules we comment on are those for
$\rtom$. The first rule states that the next transition, if not tick,
must be taken from the right subagent; the reached state is the merge
of the two, with pointer one. The second rule, instead, covers the case
when $y$ can terminate. This rule is similar to $(REF3)$. In this
way $x\rtom y$ behaves exactly like $x\refin{y}$ when the latter is
about to start refining an action $a$.
\begin{proposizione}
$P'$ is in {\em tyft} format.
Strong bisimulation is a congruence for all function names in $F'$.
$P'$ is a conservative extension of $P$.
\fine
\end{proposizione}
The binary operators are left associative and binding priority
is defined in decreasing order as follows:
$\seq > [k] > \refin{} > \para,\lpar,\sync,\merge{k},\lmerge{k},\rmerge{k},
\rtom > +$.
\subsection{Axiomatisation}
Let $\M^{+}=\{\mu^{+}\mid \mu\in \M\}$.
Let $\lambda$ range over $\M^{+}\cup \M^{\omega}\cup\{\delta\}$.
We extend the auxiliary functions introduced in the previous section in the
following way:
\[\begin{array}{|l|l|l|}
\hline
\name{a^{+}} = a &\idx{a^{+}} = 0 & \trans{a^{+}}{k} = a^{+} \\
\name{\delta} = \delta &\idx{\delta} = 0 & \trans{\delta}{k} = \delta \\
\hline
\end{array}\]
\begin{table}[hp]
{\renewcommand{\arraystretch}{1.4}
$$\begin{array}{@{}|l|@{}}
\hline
\begin{array}{lrcl|lrcl}
(alt1) & x + y & = & y + x &
(seq1) & (x y) z & = & x (y z)\\
(alt2) & (x + y) + z & = & x + (y + z)\hspace{1.5cm} &
(seq2) & (x+y) z & = & x z + y z \\
(alt3) & x + x & = & x &
(seq3) & \delta x & = & \delta \\
(alt4) & x + \delta & = & x &
(seq4) & \nil x & = & x \\
&&&&
(seq5) & x \nil & = & x
\end{array} \\
\hline
\begin{array}{lrcll}
(act) & a & = & a^{+} a^{1} &
\end{array}\\
\hline
\begin{array}{lrcll}
(par) & x\para y & = & x\lpar y + y\lpar x + x\sync y \hspace{-19.19388pt} &
\end{array}\\
\hline
\begin{array}{lrcll}
(lpar1) & \lambda x\lpar y & = & \lambda(x\para [1]y) & \mbox{ if
}\name{\lambda}\not\in S \\
(lpar2) & \lambda x\lpar y & = & \delta & \mbox{ if
}\name{\lambda}\in S \\
(lpar3) & \nil\lpar x & = & \delta & \\
(lpar4) & (x+y)\lpar z & = & x\lpar z + y\lpar z &
\end{array}\\
\hline
\begin{array}{lrcll}
(sync1) & \lambda x\sync \lambda y & = & \lambda(x\para y) &
\mbox{ if }\name{\lambda}\in S \\
(sync2) & \lambda x\sync \lambda' y & = & \delta &
\mbox{ if }\name{\lambda}\not\in S \vee \lambda\neq\lambda'\\
(sync3) & \nil \sync \lambda y& = & \delta & \\
(sync4) & \nil\sync \nil & = & \nil & \\
(sync5) & (x+y)\sync z & = & x\sync z + y\sync z & \\
(sync6) & x\sync y & = & y\sync x &
\end{array}\\
\hline
\begin{array}{lrcll}
(delay1) & [k](\lambda x) & = & \trans{\lambda}{k}([\incr{k}]x) & \\
(delay2) & [k]\nil & = & \nil & \\
(delay3) & [k](x+y) & = & [k]x + [k]y & \\
\end{array}\\
\hline
\end{array}$$}
\caption{Axioms for all the operators (except refinement)} \label{axiom1}
\end{table}
Let ${\cal T}$ be the axiom set in Tables \ref{axiom1} and
\ref{axiom2}.
Our axioms for the interaction between $\parallel$ and the empty
process is a mild variation on the treatment of \cite{Vrancken}.
While the axioms for the alternative, sequential and parallel
composition are almost standard, the other axioms are not so usual.
First, observe axiom $({\it act})$. It states that any action $a$ should
be
intended as composed of the sequence of its beginning and its ending
(with pointer $1$). The three axioms for the delay operator reflect
clearly its operational definition. More intriguing is the case of
refinement; in particular, $({\it ref}2)$ shows that the refinement can
start
by dropping the beginning of the refined action and giving priority
to the refining subagent $y$. Note that no action has been extracted
from the term, so, no phase has been ``executed''.
This is done by the first application of axiom $({\it rtom}1)$, if $y$
is not
terminated, or of $({\it rtom}2)$, if $y$ terminates properly.
The axioms for $\lmerge{k}$ and $\rmerge{k}$ are intuitively clear, as
$({\it lmerge}1)$ corresponds to the operational rule $({\it
MERGE}1)$, $({\it rmerge}1)$
to $({\it MERGE}2)$ and $({\it rmerge}2)$ to $({\it MERGE}3)$.
Finally, note that the axioms for $\rtom$ and $\rmerge{k}$ are
very similar: they differ only in the application of the delay operator
in the first two axioms.
\begin{table}[hp]
{\renewcommand{\arraystretch}{1.4}
$$\begin{array}{|lrcll|}
\hline
({\it ref}1) & (\lambda x)\refin{y} & = & \lambda (x\refin{y}) & \mbox{ if
}\lambda\not=a^{+} \\
({\it ref}2) & (a^{+} x)\refin{y} & = & (x\refin{y})\rtom y & \\
({\it ref}3) & \nil\refin{y} & = & \nil & \\
({\it ref}4) & (x+y)\refin{z} & = & x\refin{z} + y\refin{z} & \\
\hline
(rtom1) & x\rtom\lambda y & = & \lambda (x\merge{1}y) & \\
(rtom2) & a^{1} x\rtom\nil & = & [-1][-1]x& \\
(rtom3) & \lambda x\rtom\nil & = & \delta & \mbox{ if
}\idx{\lambda}\neq 1 \\
(rtom4) & \nil\rtom\nil & = & \delta &\\
(rtom5) & (x+y)\rtom\nil & = & x\rtom\nil + y\rtom\nil & \\
(rtom6) & x\rtom(y+z) & = & x\rtom y + x\rtom z & \\
\hline
(merge) & x\merge{k} y & = & x\lmerge{k} y + x\rmerge{k} y & \\
\hline
(lmerge1) & \lambda x\lmerge{k}y & = & \lambda (x\merge{k+1}[1]y) &
\mbox{ if }\idx{\lambda}\neq k\\
(lmerge2) & \lambda x\lmerge{k}y & = & \delta & \mbox { if } \idx{\lambda}=k
\\
(lmerge3) & \nil\lmerge{k}x & = & \delta &\\
(lmerge4) & (x+y)\lmerge{k}z & = & x\lmerge{k}z + y\lmerge{k}z & \\
\hline
(rmerge1) & x\rmerge{k}\lambda y & = & \lambda ([1]x\merge{k+1}y) &\\
(rmerge2) & a^{k} x\rmerge{k}\nil & = & [-1]x& \\
(rmerge3) & \lambda x\rmerge{k}\nil & = & \delta & \mbox{ if
}\idx{\lambda}\neq k \\
(rmerge4) & \nil\rmerge{k}\nil & = & \delta &\\
(rmerge5) & (x+y)\rmerge{k}\nil & = & x\rmerge{k}\nil + y\rmerge{k}\nil & \\
(rmerge6) & x\rmerge{k}(y+z) & = & x\rmerge{k}y + x\rmerge{k}z & \\
\hline
\end{array}$$}
\caption{Axioms for the refinement operator} \label{axiom2}
\end{table}
\subsection{Soundness and Completeness}
We cannot apply the algorithm presented in \cite{Aceto} because the rules
of our TSS do not fit the GSOS format used in that paper, due to the presence in our TSS of
lookahead and of an infinite set of rules and operators. However, we follow the lines
presented there.
Given a set $E$ of equations between terms, and $t=t'$ another
equation, we write $E \vdash t=t'$ to indicate that the equation
$t=t'$ is derivable from $E$ by means of equational logic.
The rules of equational logic assert that equality is a congruence
that it is preserved by instantiation of variables.
For a formal definition see, e.g.\ \cite{Hen}.
In the following we state that the theory ${\cal T}$ is sound and
complete with respect to $\bisimm{}$.
\begin{teorema} \label{consistaxiom}
If $(t = t')\in{\cal T}$ then for any closed substitution $\rho$ we have
$\rho(t)\bisimm{}\rho(t')$.
\dimo
We report the proofs for a selected set of significant axioms.
\\
Let $\rho$ be a closed substitution.
\\
{\bf (ref2)}
We want to prove that $\rho((a^{+}x)\refin{y})\bisimm{}\rho((x\refin{y})\rtom
y)$, that is\\
$(a^{+}\rho(x))\refin{\rho(y)} \bisimm{}(\rho(x)\refin{\rho(y)})
\rtom \rho(y)$.
If $(a^{+}\rho(x))\refin{\rho(y)}\deriv{\theta}t$ three cases may occur.
\begin{itemize}\vspace{-1ex}
\item
The transition is obtained by applying $({\it REF}1)$. Then the transition
$a^{+}\rho(x)\deriv{\theta}$ is derivable, with $\theta\neq a$.
This transition can be obtained in two ways:
\\
by $({\it SEQ}1)$, so we need that $a^{+}\deriv{\theta}$, but the
only transition for $a^{+}$ is $a^{+}\deriv{a}\epsilon$, hence $\theta = a$
(contradiction); or
\\
by $({\it SEQ}2)$, but we need that $a^{+}\deriv{\surd}$
(contradiction).\vspace{-1ex}
\item
The transition is obtained by applying $({\it REF}2)$. Then we have that
$\theta\neq\surd$,
$a^{+}\rho(x)\deriv{a}u$, $\rho(y)\deriv{\theta}v$ and $t =
u\refin{\rho(y)}\merge{1}v$.
The transition $a^{+}\rho(x)\deriv{a}u$
can be obtained only by an application of $({\it ACT}3)$ and $({\it
SEQ}1)$, so we have that $u = \nil\rho(x)$, from which $t\hspace{-1.59pt} =
\nil\rho(x)\refin{\rho(y)}\merge{1}v$.
Applying $({\it RTOM}1)$ to the transition $\rho(y)\deriv{\theta}v$ (remember
that $\theta\neq\surd$) we obtain
$(\rho(x)\refin{\rho(y)}) \rtom \rho(y)\deriv{\theta} (\rho(x)\refin{\rho
(y)})\merge{1}v$.
From the soundness of axiom $({\it seq}4)$ we have that
$\nil\rho(x)\bisimm{}\rho(x)$, thus
from the congruence property of $\bisimm{}$ we have
$t\bisimm{}(\rho(x)\refin{\rho (y)})\merge{1}v$.\vspace{-1ex}
\item
The transition is obtained by applying $({\it REF}3)$. Then we have
$a^{+}\rho(x)\deriv{a}u$, $u\deriv{a^{1}}u'$, $[-1][-1](u'\refin{\rho(y)})
\deriv{\theta}t$ and $\rho(y)\deriv{\surd}v$.
As in the previous case, we have $u = \nil\rho(x)$. The only
explanation for the transition $\nil\rho(x)\deriv{a^{1}}u'$ is through
$({\it SEQ}2)$ and $({\it TICK})$, thus it must be that $\rho(x)\deriv{a^{1}}u'$.
Being $a^{1}\neq a$, with an application of $({\it REF}1)$ to this transition
we obtain $\rho(x)\refin{\rho(y)}\deriv{a^{1}}u'\refin{\rho(y)}$.
Applying $({\it RTOM}2)$ yields $(\nil\rho(x)\refin{\rho(y)})\rtom\rho(y)
\deriv{\theta} t$.\vspace{-1ex}
\end{itemize}
Symmetrically, we obtain that if $(\rho(x)\refin{\rho(y)})\rtom\rho(y)
\deriv{\theta}t$ there exists an $u$ such that
$(a^{+}\rho(x))\refin{\rho(y)}\deriv{\theta}u$ and $t\bisimm{} u$.
\noindent
{\bf (delay1)}
We want to prove that $[k](\lambda \rho(x)) \bisimm{}\trans{\lambda}{k}
([\incr{k}]\rho(x))$.
Suppose that $[k](\lambda \rho(x))\deriv{\theta}t$. This transition can
be obtained only by $({\it DELAY})$; so there exist
$\theta'$ and $u$ such that $\lambda\rho(x)\deriv{\theta'}u$, $\theta =
\trans{\theta'}{k}$ and $t = [\incr{k}]u$.
From $\lambda\rho(x)\deriv{\theta'}u$ we can derive that $\lambda\neq\delta$,
$\theta'=\lambda$ and $u = \nil\rho(x)$. Hence $\trans{\lambda}{k} = \theta$
and with (${\it ACT}$3 or 4) and $({\it SEQ}1)$ we obtain that
$\trans{\lambda}{k}([\incr{k}]\rho(x))\deriv{\theta}\nil([\incr{k}]\rho(x))$.
From the soundness of axiom $(seq4)$ and the congruence property of
$\bisimm{}$ we have that $[\incr{k}]\nil\rho(x)\bisimm{}
\nil([\incr{k}]\rho(x))$.
The other direction of the proof is similar.
\noindent
{\bf (rtom2)}
We want to prove that $(a^{1}\rho(x))\rtom\nil \bisimm{}[-1][-1]\rho(x)$.
Suppose that $(a^{1}\rho(x))\rtom\nil\deriv{\theta}t$.
Because the only possible transition for $\nil$ is
$\nil\deriv{\surd}\delta$, the transition above cannot be obtained by an
application of the rule $({\it RTOM}1)$. Hence $({\it RTOM}2)$ has
been applied.
As the only transition for $a^{1}\rho(x)$ is $a^{1}\rho(x)
\deriv{a^{1}}\nil\rho(x)$ it must be that $[-1][-1]\nil\rho(x)\deriv{\theta}t$.
From the soundness of axiom $({\it seq}4)$ and the congruence property of
$\bisimm{}$ we have that $[-1][-1]\nil\rho(x)\bisimm{}
[-1][-1]\rho(x)$, so we have that $[-1][-1]\rho(x)\deriv{\theta}u$
and $t\bisimm{} u$.
Again the other direction of the proof is similar.
\fine
\end{teorema}
\begin{corollario} \label{consist}
If ${\cal T}\vdash t = t'$ then for any closed substitution $\rho$ we have
$\rho(t)\bisimm{}\rho(t')$.
\fine
\end{corollario}
\begin{definizione}
A term $t\in T(\Sigma')$ is in {\em normal form} if it can be generated by
the following grammar:
\[ n::= \nil\mid \delta \mid a^{+}\seq n \mid a^{k}\seq n \mid n + n' \]
A term $t\in T(\Sigma')$ can be {\em brought in normal form} if
there is a term $n$ in normal form with ${\cal T} \vdash t=n$.
\fine
\end{definizione}
\begin{definizione}
Let $n$ be a term in normal form. The length of $n$ is defined in the
following way:
\[\begin{array}{l}
l(\nil) = 1 \hspace{1cm}
l(a^{+}\seq n) = l(n) + 1 \\
l(\delta) = 1\hspace{1cm}
l(a^{k}\seq n) = l(n) + 1 \\
l(n+n') = l(n) + l(n') + 1
\end{array}\vspace{-4.5ex}\]
\fine
\end{definizione}
\begin{lemma} \label{operatornorm}
Let $n$ and $m$ be terms in normal form. Then
\newcounter{itm}
\begin{list}{\theitm.}{\leftmargin20pt\labelwidth15pt\labelsep5pt
\usecounter{itm}\topsep 0pt\itemsep 0pt\parsep 0pt}
\item the term $n\seq m$
can be brought in normal form;
\item for all $k\neq 0$ there exists a term $n'$ in normal form with
${\cal T} \vdash [k]n = n'$ and $l(n')=l(n)$;
\item the terms $n\lpar m$, $n\sync m$ and $n\para m$
can be brought in normal form;
\item for all $k>0$ the terms $n\rmerge{k}m$, $n\lmerge{k}m$ and $n\merge{k}m$
can be brought in normal form;
\item the term $n\rtom m$ can be brought in normal form;
\item and the term $n\refin{m}$ can be brought in normal form.
\end{list}
\dimo
We establish part 4 with induction on the sum of the length of $n$ and $m$.
The other parts proceed likewise.
\\
Let $n$ and $m$ be two terms in normal form and $l(n) + l(m) = i$.
We first prove that there exists a term $p$ in normal form such that
${\cal T}\vdash n\rmerge{k} m = p$.
\begin{list}{$\bullet$}{\leftmargin20pt\labelwidth15pt\labelsep5pt
\topsep 4pt\itemsep 0pt\parsep 0pt}
\item
if $m$ is $\nil$ we can have the following cases:
\begin{list}{\bf --}{\leftmargin20pt\topsep 0pt\itemsep 0pt\parsep 0pt}
\item
if $n$ is $\nil$, we have that $\nil\rmerge{k}\nil =
\delta$ $({\it rmerge}4)$, and $\delta$ is in normal form.
\item
if $n$ is $\delta$, we use that $\delta =
\delta x$ (seq3). Thus, using $({\it rmerge}3)$ we have
$\delta \rmerge{k} \nil = \delta x \rmerge{k} \nil = \delta$.
\item
if $n$ is $a^{+} n'$ we have
$a^{+}n'\rmerge{k}\nil = \delta$, by $({\it rmerge}3)$.
\item
if $n$ is $a^{h}n'$ and $h\neq k$, we also have
$a^{h}n'\rmerge{k}\nil = \delta$.
\item
if $n$ is $a^{k}n'$, we have $a^{k}n'\rmerge{k}\nil =
[-1]n'$ by $({\it rmerge}2)$, on which we apply part 2 of the lemma.
\item
if $n$ is $n'+n''$, we have
$(n'+n'')\rmerge{k}\nil = n'\rmerge{k}\nil + n''\rmerge{k}\nil$ by
$({\it rmerge}5)$. As $l(n'),l(n'')