A preliminary version of this paper appeared as [1].

# On the Axiomatisability of Parallel Composition

Luca Aceto  Reykjavik University, Iceland; Gran Sasso Science Institute
(GSSI), Italy<EMAIL_ADDRESS>,  Valentina Castiglioni  Reykjavik University,
Iceland<EMAIL_ADDRESS>,  Anna Ingólfsdóttir  Reykjavik University, Iceland
<EMAIL_ADDRESS>,  Bas Luttik  Eindhoven University of Technology, The Netherlands
<EMAIL_ADDRESS>and  Mathias Ruggaard Pedersen  Reykjavik University,
Iceland<EMAIL_ADDRESS>
###### Abstract.

This paper studies the existence of finite equational axiomatisations of the
_interleaving parallel composition operator_ modulo the behavioural
equivalences in van Glabbeek’s _linear time-branching time spectrum_. In the
setting of the process algebra BCCSP over a finite set of actions, we provide
_finite_ , ground-complete axiomatisations for various simulation and
(decorated) trace semantics. We also show that no congruence over BCCSP that
includes bisimilarity and is included in possible futures equivalence has a
finite, ground-complete axiomatisation; this _negative result_ applies to all
the nested trace and nested simulation semantics.

###### Key words and phrases:

Axiomatisation, Parallel composition, Linear time-branching time spectrum

##  1\. Introduction

_Process algebras_ [7, 5] are prototype specification languages allowing for
the description and analysis of concurrent and distributed systems, or simply
_processes_. These languages offer a variety of operators to specify composite
processes from components one has already built. Notably, in order to model
the concurrent interaction between processes, the majority of process algebras
include some form of _parallel composition_ operator, also known as merge.

Following Milner’s seminal work on CCS [26], the semantics of a process
algebra is often defined according to a two-step approach. In the first step,
the _operational semantics_ [31] of a process is modelled via a _labelled
transition system_ (LTS) [24], in which computational steps are abstracted
into state-to-state transitions having actions as labels.

Behavioural equivalences have then been introduced, in the second step, as
simple and elegant tools for comparing the behaviour of processes. These are
equivalence relations defined on the states of LTSs allowing one to establish
whether two processes have the same _observable behaviour_. Different notions
of observability correspond to different levels of abstraction from the
information carried by the LTS, which can either be considered irrelevant in a
given application context, or be unavailable to an external observer.

In [19], van Glabbeek presented the _linear time-branching time spectrum_ ,
i.e., a taxonomy of behavioural equivalences based on their distinguishing
power. He carried out his study in the setting of the process algebra BCCSP,
which consists of the basic operators from CCS [26] and CSP [23], and he
proposed _ground-complete axiomatisations_ for most of the congruences in the
spectrum over this language. (An axiomatisation is ground-complete if it can
prove all the valid equations relating terms that do not contain variables.)
The presented ground-complete axiomatisations are _finite_ if so is the set of
actions. For the ready simulation, ready trace and failure trace equivalences,
the axiomatisation in [19] made use of conditional equations; Blom, Fokkink
and Nain gave purely equational, finite axiomatisations in [8]. Then, the
works in [2], on nested semantics, and in [11], on impossible futures
semantics, completed the studies of the axiomatisability of behavioural
congruences over BCCSP by providing _negative_ results: neither impossible
futures nor any of the nested semantics have a finite, ground-complete
axiomatisation over BCCSP.

Obtaining a complete axiomatisation of a behavioural congruence is a classic,
key problem in concurrency theory, as an equational axiomatisation
characterises the semantics of a process algebra in a purely syntactic
fashion. Hence, this characterisation becomes independent of the details of
the definition of the process semantics of interest, allowing one to compare
semantics that may have been defined in very different styles via a collection
of revealing axioms.

All the results mentioned so far were obtained over the algebra BCCSP, which
does not include any operator for the parallel composition of processes.
Considering the crucial role of such an operator, it is natural to ask which
of those results would still hold over a process algebra including it.

In the literature, we can find a wealth of studies on the axiomatisability of
parallel composition modulo _bisimulation semantics_ [30]. Briefly, in the
seminal work [22], Hennessy and Milner proposed a ground-complete
axiomatisation of the recursion-free fragment of CCS modulo bisimilarity. That
axiomatisation, however, included infinitely many axioms, which corresponded
to instances of the _expansion law_ used to express equationally the semantics
of the merge operator. Then, Bergstra and Klop showed in [6] that a finite
ground-complete axiomatisation modulo bisimilarity can be obtained by
enriching CCS with two auxiliary operators, i.e., the _left merge_
$\mathbin{\begin{picture}(1.0,1.75)\put(0.0,0.0){\line(1,0){1.0}}
\put(0.0,0.0){\line(0,1){1.75}} \put(0.45,0.0){\line(0,1){1.75}}
\end{picture}}$ and the _communication merge_ $\\!\\!\\!~{}|~{}\\!\\!$. Later,
Moller proved that the use of auxiliary operators is indeed necessary to
obtain a finite equational axiomatisation of bisimilarity in [27, 28, 29].

To the best of our knowledge, no systematic study of the axiomatisability of
the parallel composition operator modulo the other semantics in the spectrum
has been presented so far.

### Our contribution

We consider the process algebra $\mathrm{BCCSP}_{\scriptsize\|}$, i.e., BCCSP
enriched with the interleaving parallel composition operator, and we study the
existence of finite equational axiomatisations of the behavioural congruences
in the linear time-branching time spectrum over it. Our results delineate the
_boundary_ between finite and non-finite axiomatisability of the congruences
in the spectrum over the language $\mathrm{BCCSP}_{\scriptsize\|}$. (See
Figure 1.)

We start by providing a _finite_ , _ground-complete_ axiomatisation for _ready
simulation_ semantics [9]. The axiomatisation is obtained by extending the one
for BCCSP with a few axioms expressing equationally the behaviour of
interleaving modulo the considered congruence. The added axioms allow us to
eliminate all occurrences of the interleaving operator from
$\mathrm{BCCSP}_{\scriptsize\|}$ processes, thus reducing ground-completeness
over $\mathrm{BCCSP}_{\scriptsize\|}$ to ground-completeness over BCCSP [19,
8]. Since the axioms for the elimination of parallel composition modulo ready
simulation equivalence are, of course, sound with respect to equivalences that
are coarser than ready simulation equivalence, the “reduction to ground-
completeness over BCCSP” works for all behavioural equivalences in the
spectrum below ready simulation equivalence. Nevertheless, for those
equivalences, we shall offer more elegant axioms to equationally eliminate
parallel composition from closed terms. We shall then observe a sort of
parallelism between the axiomatisations for the notions of simulation and the
corresponding decorated trace semantics: the axioms used to equationally
express the interplay between the interleaving operator and the other
operators of BCCSP in a decorated trace semantics can be seen as the _linear
counterpart_ of those used in the corresponding notion of simulation
semantics. For instance, while the axioms for ready simulation impose
constraints on the form of both arguments of the interleaving operator to
facilitate equational reductions, those for ready trace equivalence impose
similar constraints but only on one argument.

Finally, we complete our journey in the spectrum by showing that _nested
simulation_ and _nested trace_ semantics do not have a finite axiomatisation
over $\mathrm{BCCSP}_{\scriptsize\|}$. To this end, firstly we adapt Moller’s
arguments to the effect that bisimilarity is not finitely based over CCS to
obtain the _negative result_ for _possible futures equivalence_ , also known
as $2$-_nested trace equivalence_. Informally, the negative result is obtained
by providing an infinite family of equations that are all sound modulo
possible futures equivalence but that cannot all be derived from any finite,
sound axiom system. Then, we exploit the soundness modulo bisimilarity of the
equations in the family to extend the negative result to all the congruences
that are finer than possible futures and coarser than bisimilarity, thus
including all nested trace and nested simulation semantics.

All the results mentioned so far are obtained for a parallel composition
operator that implements interleaving without synchronisation between parallel
components. As natural extension, we then discuss the effect of extending our
results to parallel composition with CCS-style synchronisation.

### Organisation of contents

After reviewing some basic notions on behavioural equivalences and equational
logic in Section 2, we start our journey in the spectrum by providing a
finite, ground-complete axiomatisation for ready simulation equivalence over
$\mathrm{BCCSP}_{\scriptsize\|}$ in Section 3. In Section 4 we discuss how it
is possible to refine the axioms for ready simulation to obtain finite,
ground-complete axiomatisations for completed simulation and simulation
equivalences. Then, in Section 5 similar refinements are provided for the
(decorated) trace equivalences, thus completing the presentation of our
positive results. We end our journey in Section 6 with the presentation of the
negative results, namely that the nested simulation and nested trace
equivalences do not have a finite axiomatisation over
$\mathrm{BCCSP}_{\scriptsize\|}$. In Section 7 we modify the semantics of
parallel composition to allow processes running in parallel to synchronise and
we discuss the effect of this extension on the results obtained in Sections
3–6. Finally, in Section 8 we draw some conclusions and discuss avenues for
future work.

### What’s new

A preliminary version of this paper appeared as [1]. We have enriched our
previous contribution as follows:

  1. (1)

We provide the full proofs of our results.

  2. (2)

We extend the results presented in [1] from purely interleaving parallel
composition to parallel composition with synchronisation à la CCS. (Section
7).

  3. (3)

We present model constructions showing that the specific axioms we provide to
axiomatise parallel compositions in ready simulation equivalence cannot be
derived from the axiomatisations of completed simulation equivalence and ready
trace equivalence. Similarly, we show that the axiomatisations of completed
simulation and failure equivalence cannot be derived from that of completed
trace equivalence.

##  2\. Background

### The language

The language $\mathrm{BCCSP}_{\scriptsize\|}$ extends BCCSP with parallel
composition. Formally, $\mathrm{BCCSP}_{\scriptsize\|}$ consists of basic
operators from CCS [26] and CSP [23], with the purely _interleaving_ parallel
composition operator $\mathbin{\|}$, and is given by the following grammar:

$t::=\mathbf{0}\;\mid\;x\;\mid\;a.t\;\mid\;t+t\;\mid\;t\mathbin{\|}t$

where $a$ ranges over a set of actions $\mathcal{A}$ and $x$ ranges over a
countably infinite set of variables $\mathcal{V}$. In what follows, we assume
that the set of actions $\mathcal{A}$ is _finite_ and non-empty.

We shall use the meta-variables $t,u,\dots$ to range over
$\mathrm{BCCSP}_{\scriptsize\|}$ terms, and write $\mathrm{var}(t)$ for the
collection of variables occurring in the term $t$. We also adopt the standard
convention that prefixing binds strongest and $+$ binds weakest. Moreover,
trailing $\mathbf{0}$’s will often be omitted from terms. We use a _summation_
$\sum_{i\in\\{1,\ldots,k\\}}t_{i}$ to denote the term $t=t_{1}+\cdots+t_{k}$,
where the empty sum represents 0. We can also assume that the terms $t_{i}$,
for $i\in\\{1,\dots,k\\}$, do not have $+$ as head operator, and refer to them
as the _summands_ of $t$. The _size_ of a term $t$, denoted by
$\mathrm{size}(t)$, is the number of operator symbols in it.

A $\mathrm{BCCSP}_{\scriptsize\|}$ term is _closed_ if it does not contain any
variables. We shall, sometimes, refer to closed terms simply as _processes_.
We let $\mathcal{P}$ denote the set of $\mathrm{BCCSP}_{\scriptsize\|}$
processes and let $p,q,\dots$ range over it. We use the _Structural
Operational Semantics_ (SOS) framework [31] to equip processes with an
operational semantics. A _literal_ is an expression of the form
$t\xrightarrow{\,{a}\,}t^{\prime}$ for some process terms $t,t^{\prime}$ and
action $a\in\mathcal{A}$. It is _closed_ if both $t,t^{\prime}$ are closed
terms. The inference rules for _prefixing_ $a.\\_$, _nondeterministic choice_
$+$ and _interleaving parallel composition_ $\mathbin{\|}$ are reported in
Table 1.

$\displaystyle\inference{}{a.x\xrightarrow{\,{a}\,}x}\;\,\inference{x\xrightarrow{\,{a}\,}x^{\prime}}{x+y\xrightarrow{\,{a}\,}x^{\prime}}\;\,\inference{y\xrightarrow{\,{a}\,}y^{\prime}}{x+y\xrightarrow{\,{a}\,}y^{\prime}}\;\,\inference{x\xrightarrow{\,{a}\,}x^{\prime}}{x\mathbin{\|}y\xrightarrow{\,{a}\,}x^{\prime}\mathbin{\|}y}\;\,\inference{y\xrightarrow{\,{a}\,}y^{\prime}}{x\mathbin{\|}y\xrightarrow{\,{a}\,}x\mathbin{\|}y^{\prime}}$
Table 1. Operational semantics of $\mathrm{BCCSP}_{\scriptsize\|}$.

A _substitution_ $\sigma$ is a mapping from variables to terms. It extends to
terms, literals and rules in the usual way. A substitution is _closed_ if it
maps every variable to a process.

The inference rules in Table 1 induce the $\mathcal{A}$-_labelled transition
system_ [24] $(\mathcal{P},\mathcal{A},\xrightarrow{\,{}\,})$ whose transition
relation
${\xrightarrow{\,{}\,}}\subseteq\mathcal{P}\times\mathcal{A}\times\mathcal{P}$
contains exactly the closed literals that can be derived using the rules in
Table 1. As usual, we write $p\xrightarrow{\,{a}\,}p^{\prime}$ in lieu of
$(p,a,p^{\prime})\in{\xrightarrow{\,{}\,}}$. For each $p\in\mathcal{P}$ and
$a\in\mathcal{A}$, we write $p\xrightarrow{\,{a}\,}$ if
$p\xrightarrow{\,{a}\,}p^{\prime}$ holds for some $p^{\prime}$, and
$p\mathrel{{\xrightarrow{\,{a}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$ otherwise. The _initials_ of $p$ are the actions that label
the outgoing transitions of $p$, that is, $\mathtt{I}(p)=\\{a\mid
p\xrightarrow{\,{a}\,}\\}$. For a sequence of actions $\alpha=a_{1}\cdots
a_{k}$ ($k\geq 0$), and processes $p,p^{\prime}$, we write
$p\xrightarrow{\,{\alpha}\,}p^{\prime}$ if and only if there exists a sequence
of transitions
$p=p_{0}\xrightarrow{\,{a_{1}}\,}p_{1}\xrightarrow{\,{a_{2}}\,}\cdots\xrightarrow{\,{a_{k}}\,}p_{k}=p^{\prime}$.
If $p\xrightarrow{\,{\alpha}\,}p^{\prime}$ holds for some process
$p^{\prime}$, then $\alpha$ is a trace of $p$, and $p^{\prime}$ is a
_derivative_ of $p$. Moreover, we say that $\alpha$ is a _completed trace_ of
$p$ if $\mathtt{I}(p^{\prime})=\emptyset$. We let $\mathtt{T}(p)$ denote the
_set of traces_ of $p$, and we use $\mathtt{CT}(p)\subseteq\mathtt{T}(p)$ for
the set of completed traces of $p$. We write $\varepsilon$ for the _empty
trace_ ; $|\alpha|$ stands for the _length_ of trace $\alpha$. It is well
known, and easy to show, that $\mathtt{T}(p)$ is finite and $\mathtt{CT}(p)$
is non-empty for each $\mathrm{BCCSP}_{\scriptsize\|}$ process $p$. It follows
that we can define the _depth_ of a process $p$, denoted by $0pt(p)$, as the
length of a _longest_ completed trace of $p$. Formally,
$0pt(p)=\max\\{|\alpha|\mid\alpha\in\mathtt{CT}(p)\\}$. Similarly, the _norm_
of a process $p$, denoted by $\mathrm{norm}(p)$, is the length of a _shortest_
completed trace of $p$, i.e.
$\mathrm{norm}(p)=\min\\{|\alpha|\mid\alpha\in\mathtt{CT}(p)\\}$.

### Behavioural equivalences.

_Behavioural equivalences_ have been introduced to establish whether the
behaviours of two processes are _indistinguishable for their observers_.
Roughly, they allow us to check whether the _observable_ semantics of two
processes is _the same_. In the literature we can find several notions of
behavioural equivalence based on the observations that an external observer
can make on the process. In his seminal article [19], van Glabbeek gave a
taxonomy of the behavioural equivalences discussed in the literature on
concurrency theory, which is now called the _linear time-branching time
spectrum_ (see Figure 1).

One of the main concerns in the development of a meta-theory of process
languages is to guarantee their _compositionality_ , i.e., that the
_replacement_ of a component of a system with an
$\,{\mathcal{R}}\,$-equivalent one, for a chosen behavioural equivalence
$\,{\mathcal{R}}\,$, does not affect the behaviour of that system. In
algebraic terms, this is known as the _congruence property_ of
$\,{\mathcal{R}}\,$ with respect to all language operators, which consists in
verifying whether

$f(t_{1},\dots,t_{n})\,{\mathcal{R}}\,f(t_{1}^{\prime},\dots,t_{n}^{\prime})\text{
for every $n$-ary operator }f\text{ whenever
}t_{i}\,{\mathcal{R}}\,t_{i}^{\prime}\text{ for all }i=1,\dots,n.$

bisimulation ($\sim_{\mathtt{B}}$)$2$-nested simulation
($\sim_{2\mathtt{S}}$)failure simulation ($\sim_{\mathtt{F}\mathtt{S}}$) $=$
ready simulation ($\sim_{\mathtt{R}\mathtt{S}}$)ready trace
($\sim_{\mathtt{RT}}$)failure trace ($\sim_{\mathtt{FT}}$)readies
($\sim_{\mathtt{R}}$)failures ($\sim_{\mathtt{F}}$)completed trace
($\sim_{\mathtt{CT}}$)trace ($\sim_{\mathtt{T}}$)completed simulation
($\sim_{\mathtt{C}\mathtt{S}}$)simulation ($\sim_{\mathtt{S}}$)possible
futures ($\sim_{\mathtt{PF}}$)

Figure 1.  The linear time-branching time spectrum [19]. For the equivalence
relations in blue we provide a finite, ground-complete axiomatization. For the
ones in red, we provide a negative result. The case of bisimulation is known
from the literature [27, 28, 29].

Since $\mathrm{BCCSP}_{\scriptsize\|}$ operators are defined by inference
rules in the de Simone format [15], by [17, Theorem 4] we have that all the
equivalences in the spectrum in Figure 1 are congruences with respect to them.
Our aim in this paper is to investigate the existence of a finite equational
axiomatisation of $\mathrm{BCCSP}_{\scriptsize\|}$ modulo all those
congruences.

### Equational Logic.

An _axiom system_ $\mathcal{E}$ is a collection of _equations_ $t\approx u$
over $\mathrm{BCCSP}_{\scriptsize\|}$. An equation $t\approx u$ is _derivable_
from an axiom system $\mathcal{E}$, notation $\mathcal{E}\vdash t\approx u$,
if there is an _equational proof_ for it from $\mathcal{E}$, namely if
$t\approx u$ can be inferred from the axioms in $\mathcal{E}$ using the
_rules_ of _equational logic_ , which express reflexivity, symmetry,
transitivity, substitution and closure under $\mathrm{BCCSP}_{\scriptsize\|}$
contexts and are reported in Table 2. In equational proofs, we shall write
$p\stackrel{{\scriptstyle(\mathrm{A})}}{{\approx}}q$ to highlight that the
axiom denoted by A is used in that step of the proof.

$\displaystyle\scalebox{0.9}{($e_{1}$)}\;t\approx
t\qquad\scalebox{0.9}{($e_{2}$)}\;\inference{t\approx u}{u\approx
t}\qquad\scalebox{0.9}{($e_{3}$)}\;\inference{{t\approx u\quad u\approx
v}}{{t\approx v}}\qquad\scalebox{0.9}{($e_{4}$)}\;\inference{{t\approx
u}}{{\sigma(t)\approx\sigma(u)}}$
$\displaystyle\scalebox{0.9}{($e_{5}$)}\;\inference{t\approx u}{a.t\approx
a.u}\qquad\scalebox{0.9}{($e_{6}$)}\;\inference{t\approx u\quad
t^{\prime}\approx u^{\prime}}{t+t^{\prime}\approx
u+u^{\prime}}\qquad\scalebox{0.9}{($e_{8}$)}\;\inference{t\approx u\quad
t^{\prime}\approx u^{\prime}}{t\mathbin{\|}t^{\prime}\approx
u\mathbin{\|}u^{\prime}}\enspace.$ Table 2.  The rules of equational logic

We are interested in equations that are valid modulo some congruence relation
$\,{\mathcal{R}}\,$ over closed terms. The equation $t\approx u$ is said to be
_sound_ modulo $\,{\mathcal{R}}\,$ if
$\sigma(t)\,\,{\mathcal{R}}\,\,\sigma(u)$ for all closed substitutions
$\sigma$. For simplicity, if $t\approx u$ is sound modulo $\,{\mathcal{R}}\,$,
then we write $t\,\,{\mathcal{R}}\,\,u$. An axiom system is _sound_ modulo
$\,{\mathcal{R}}\,$ if, and only if, all of its equations are sound modulo
$\,{\mathcal{R}}\,$. Conversely, we say that $\mathcal{E}$ is _ground-
complete_ modulo $\,{\mathcal{R}}\,$ if $p\,\,{\mathcal{R}}\,\,q$ implies
$\mathcal{E}\vdash p\approx q$ for all closed terms $p,q$. We say that
$\,{\mathcal{R}}\,$ has a _finite_ ground-complete axiomatisation, if there is
a _finite_ axiom system $\mathcal{E}$ that is sound and ground-complete modulo
$\,{\mathcal{R}}\,$.

(A0) $x+\mathbf{0}\approx x$ |  (P0) $x\mathbin{\|}\mathbf{0}\approx x$
---|---
(A1) $x+y\approx y+x$ |  (P1) $x\mathbin{\|}y\approx y\mathbin{\|}x$
(A2) $(x+y)+z\approx x+(y+z)$ |
(A3) $x+x\approx x$ |
Table 3. Basic axioms for $\mathrm{BCCSP}_{\scriptsize\|}$. We define
$\mathcal{E}_{0}=\\{\mathrm{A0,A1,A2,A3}\\}$ and
$\mathcal{E}_{1}=\mathcal{E}_{0}\cup\\{\mathrm{P0,P1}\\}$.

In Table 3 we present some basic axioms for $\mathrm{BCCSP}_{\scriptsize\|}$
that are sound with respect to all the behavioural equivalences in Figure 1.
Henceforth, we will let $\mathcal{E}_{0}=\\{\mathrm{A0,A1,A2,A3}\\}$, and we
will denote by $\mathcal{E}_{1}$ the axiom system consisting of all the axioms
in Table 3, namely $\mathcal{E}_{1}=\mathcal{E}_{0}\cup\\{\mathrm{P0,P1}\\}$.

(EL1) $ax\mathbin{\|}by\approx a(x\mathbin{\|}by)+b(ax\mathbin{\|}y)$
---
(EL2) $\sum_{i\in I}a_{i}x_{i}\mathbin{\|}\sum_{j\in
J}b_{j}y_{j}\approx\sum_{i\in I}a_{i}(x_{i}\mathbin{\|}\sum_{j\in
J}b_{j}y_{j})+\sum_{j\in J}b_{j}(\sum_{i\in I}a_{i}x_{i}\mathbin{\|}y_{j})$
with $a_{i}\neq a_{k}$ whenever $i\neq k$ and $b_{j}\neq b_{h}$ whenever
$j\neq h$, $\forall\,i,k\in I,\forall\,j,h\in J$
(EL3) $\sum_{i\in I}a_{i}x_{i}\mathbin{\|}\sum_{j\in
J}b_{j}y_{j}\approx\sum_{i\in I}a_{i}(x_{i}\mathbin{\|}\sum_{j\in
J}b_{j}y_{j})+\sum_{j\in J}b_{j}(\sum_{i\in I}a_{i}x_{i}\mathbin{\|}y_{j})$
Table 4.  The different instantiations of the expansion law.

To be able to eliminate the interleaving parallel composition operator from
closed terms we will make use of two refinements EL1 and EL2 of EL3, which is
the classic expansion law [22] (see Table 4). We remark that the actions
occurring in the three axioms in Table 4 are not action variables. Hence, when
we write that an axiom system $\mathcal{E}$ includes one of these axioms, we
mean that it includes all possible instances of that axiom with respect to the
actions in $\mathcal{A}$. In particular, EL3 is a schema that generates
infinitely many axioms, regardless of the cardinality of the set of actions.
This is due to the fact that we can have arbitrary summations in the two
arguments of the parallel composition in the left hand side of EL3. On the
other hand, when the set of actions is assumed to be finite, we are guaranteed
that there are only finitely many instances of EL1 and EL2. Indeed, EL1 is a
particular instance of EL2, i.e., the one in which both summations are over
singletons. The reason for considering both is that, as we will see, EL1 is
enough to obtain the elimination result when combined with axioms allowing us
to reduce any process of the form $(\sum_{i\in
I}a_{i}p_{i})\mathbin{\|}(\sum_{j\in J}b_{j}q_{j})$ to $\sum_{i\in I,j\in
J}(a_{i}p_{i}\mathbin{\|}b_{j}q_{j})$. Axiom EL2 is needed when this reduction
is not sound modulo the considered semantics.

##  3\. Ready simulation

In this section, we begin our journey in the spectrum by studying the
equational theory of _ready simulation_ equivalence, whose formal definition
is recalled below together with those of _completed simulation_ and
_simulation_ equivalence.

[Simulation equivalences] no line here

  * •

A _simulation_ is a binary relation
${\,{\mathcal{R}}\,}\subseteq\mathcal{P}\times\mathcal{P}$ such that, whenever
$p\,{\mathcal{R}}\,q$ and $p\xrightarrow{\,{a}\,}p^{\prime}$, then there is
some $q^{\prime}$ such that $q\xrightarrow{\,{a}\,}q^{\prime}$ and
$p^{\prime}\,{\mathcal{R}}\,q^{\prime}$. We write $p\sqsubseteq_{\mathtt{S}}q$
if there is a simulation $\\!\,{\mathcal{R}}\,\\!$ such that
$p\,{\mathcal{R}}\,q$. We say that $p$ is _simulation equivalent_ to $q$,
notation $p\sim_{\mathtt{S}}q$, if $p\sqsubseteq_{\mathtt{S}}q$ and
$q\sqsubseteq_{\mathtt{S}}p$.

  * •

A _completed simulation_ is a simulation $\\!\,{\mathcal{R}}\,\\!$ such that,
whenever $p\,{\mathcal{R}}\,q$ and $\mathtt{I}(p)=\emptyset$, then
$\mathtt{I}(q)=\emptyset$. We write $p\sqsubseteq_{\mathtt{CS}}q$ if there is
a completed simulation $\\!\,{\mathcal{R}}\,\\!$ such that
$p\,{\mathcal{R}}\,q$. We say that $p$ is _completed simulation equivalent_ to
$q$, notation $p\sim_{\mathtt{CS}}q$, if $p\sqsubseteq_{\mathtt{CS}}q$ and
$q\sqsubseteq_{\mathtt{CS}}p$.

  * •

A _ready simulation_ is a simulation $\\!\,{\mathcal{R}}\,\\!$ such that,
whenever $p\,{\mathcal{R}}\,q$ then $\mathtt{I}(p)=\mathtt{I}(q)$. We write
$p\sqsubseteq_{\mathtt{RS}}q$ if there is a ready simulation
$\\!\,{\mathcal{R}}\,\\!$ such that $p\,{\mathcal{R}}\,q$. We say that $p$ is
_ready simulation equivalent_ to $q$, notation $p\sim_{\mathtt{RS}}q$, if
$p\sqsubseteq_{\mathtt{RS}}q$ and $q\sqsubseteq_{\mathtt{RS}}p$.

In [18] the notion of _failure simulation_ was also introduced as a simulation
$\\!\,{\mathcal{R}}\,\\!$ such that, whenever $p\,{\mathcal{R}}\,q$ and
$\mathtt{I}(p)\cap X=\emptyset$, for some $X\subseteq\mathcal{A}$, then
$\mathtt{I}(q)\cap X=\emptyset$. Then, in [17] it was proved that the notion
of failure simulation coincides with that of ready simulation.

(RS) $a(bx+by+z)\approx a(bx+by+z)+a(bx+z)$
---
(RSP1)
$(ax+ay+u)\mathbin{\|}(bz+bw+v)\approx(ax+u)\mathbin{\|}(bz+bw+v)+(ay+u)\mathbin{\|}(bz+bw+v)+$
$(ax+ay+u)\mathbin{\|}(bz+bw+v)\approx$
$+(ax+ay+u)\mathbin{\|}(bz+v)+(ax+ay+u)\mathbin{\|}(bw+v)$
(RSP2) $\left(\sum_{i\in
I}a_{i}x_{i}\right)\mathbin{\|}(by+bz+w)\approx\left(\sum_{i\in
I}a_{i}x_{i}\right)\mathbin{\|}(by+w)+\left(\sum_{i\in
I}a_{i}x_{i}\right)\mathbin{\|}(bz+w)+$
$\left(\sum_{i\in I}a_{i}x_{i}\right)\mathbin{\|}(by+bz+w)\approx$
$+\sum_{i\in I}a_{i}\left(x_{i}\mathbin{\|}(by+bz+w)\right)$
$\left(\sum_{i\in I}a_{i}x_{i}\right)\mathbin{\|}(by+bz+w)\approx$ where
$a_{j}\neq a_{k}$ whenever $j\neq k$ for $j,k\in I$
$\mathcal{E}_{\mathtt{RS}}=\mathcal{E}_{1}\cup\\{\textrm{RS, RSP1, RSP2,
EL2}\\}$
Table 5.  Additional axioms for ready simulation equivalence.

Our aim is to provide a _finite_ , _ground-complete_ axiomatisation of
$\mathrm{BCCSP}_{\scriptsize\|}$ modulo ready simulation equivalence. To this
end, we recall that in [19] it was proved that the axiom system consisting of
$\mathcal{E}_{0}$ together with axiom RS in Table 5 is a ground-complete
axiomatisation of BCCSP, i.e., the language that is obtained from
$\mathrm{BCCSP}_{\scriptsize\|}$ if $\mathbin{\|}$ is omitted, modulo
$\sim_{\mathtt{RS}}$. Hence, to obtain a finite, ground-complete
axiomatisation of $\mathrm{BCCSP}_{\scriptsize\|}$ modulo $\sim_{\mathtt{RS}}$
it suffices to enrich the axiom system $\mathcal{E}_{1}\cup\\{\mathrm{RS}\\}$
with finitely many axioms allowing one to eliminate all occurrences of
$\mathbin{\|}$ from closed $\mathrm{BCCSP}_{\scriptsize\|}$ terms. In fact, by
letting $\mathcal{E}_{\mathtt{RS}}$ denote the axiom system
$\mathcal{E}_{1}\cup\\{\mathrm{RS}\\}$ suitably enriched with such elimination
axioms, the elimination result consists in proving that for every closed
$\mathrm{BCCSP}_{\scriptsize\|}$ term $p$ there is a closed BCCSP term $q$
(i.e., without any occurrence of $\mathbin{\|}$ in it) such that
$\mathcal{E}_{\mathtt{RS}}\vdash p\approx q$. Then, the completeness of the
proposed axiom system over $\mathrm{BCCSP}_{\scriptsize\|}$ is a direct
consequence of that over BCCSP proved in [19].

Clearly, EL3 would allow us to obtain the desired elimination, but, as
previously mentioned, it is a schema that finitely presents an infinite
collection of equations, and thus an axiom system including it is infinite.
Instead, we include EL2, which is a variant of EL3 that generates only
finitely many axioms (see Table 4), and the schemata RSP1 and RSP2 that
characterise the distributivity of $\mathbin{\|}$ over $+$ modulo
$\sim_{\mathtt{RS}}$ (see Table 5).

First of all, we notice that the axiom system
$\mathcal{E}_{\mathtt{RS}}=\mathcal{E}_{1}\cup\\{\mathrm{RS,RSP1,RSP2,EL2}\\}$
is sound modulo ready simulation equivalence.

######  Theorem 1 ($\mathcal{E}_{\mathtt{RS}}$ soundness).

The axiom system $\mathcal{E}_{\mathtt{RS}}$ is sound for
$\mathrm{BCCSP}_{\scriptsize\|}$ modulo ready simulation equivalence, namely
whenever $\mathcal{E}_{\mathtt{RS}}\vdash p\approx q$ then
$p\sim_{\mathtt{RS}}q$.

Let us focus now on ground-completeness. Intuitively, RSP1 and RSP2 have been
constructed in such a way that the set of initial actions of the two arguments
of $\mathbin{\|}$ is preserved, while the initial term is reduced to a sum of
terms of smaller size. Briefly, according to the main features of ready
simulation semantics, axiom RSP1 allows us to distribute $\mathbin{\|}$ over
$+$ when both arguments of $\mathbin{\|}$ have nondeterministic choices among
summands having the same initial action. Conversely, axiom RSP2 deals with the
case in which only one argument of $\mathbin{\|}$ has summands with the same
initial action. In order to preserve the branching structure of the process,
which is fundamental to guarantee the soundness of the axioms modulo
$\sim_{\mathtt{RS}}$, both RSP1 and RSP2 take into account the behaviour of
both arguments of $\mathbin{\|}$: the terms in the right-hand side of both
axioms are such that whenever the initial nondeterministic choice of one
argument of $\mathbin{\|}$ is resolved, the entire behaviour of the other
argument is preserved. In fact, we stress that a simplified version of, e.g.,
RSP1 in which only one argument of $\mathbin{\|}$ distributes over $+$ would
not be sound modulo $\sim_{\mathtt{RS}}$. Consider, for instance, the process
$p=(a+aa+b)\mathbin{\|}c$. It is immediate to verify that
$p\not\sim_{\mathtt{RS}}(a+b)\mathbin{\|}c+(aa+b)\mathbin{\|}c$ (since
$p\not\sqsubseteq_{\mathtt{RS}}(a+b)\mathbin{\|}c+(aa+b)\mathbin{\|}c$).

The idea is that by (repeatedly) applying axioms RSP1 and RSP2, from left to
right, we are able to reduce a process of the form $(\sum_{i\in
I}p_{i})\mathbin{\|}(\sum_{j\in J}p_{j})$ to one of the form $\sum_{k\in
K}p_{k}$ such that whenever $p_{k}$ has $\mathbin{\|}$ as head operator then
$p_{k}=\sum_{h\in H}a_{h}p_{h}\mathbin{\|}\sum_{l\in L}b_{l}p_{l}$, with
$a_{h}\neq a_{h^{\prime}}$ for $h\neq h^{\prime}$, and $b_{l}\neq
b_{l^{\prime}}$ for $l\neq l^{\prime}$, for some closed
$\mathrm{BCCSP}_{\scriptsize\|}$ terms $p_{h},p_{l}$. The elimination of
$\mathbin{\|}$ from these terms can then proceed by means of the finitary
refinement EL2 of the expansion law presented in Table 4. In particular, we
notice that RSP2 is needed because RSP1 alone does not allow us to reduce all
processes of the form $(\sum_{i\in I}p_{i})\mathbin{\|}(\sum_{j\in J}p_{j})$
into a sum of processes to which EL2 can be applied. This is mainly due to the
fact that, in order to be sound modulo $\sim_{\mathtt{RS}}$, RSP1 imposes
constraints on the form of both arguments of a process $(\sum_{i\in
I}p_{i})\mathbin{\|}(\sum_{j\in J}p_{j})$.

We can then proceed to prove the elimination result, starting from a useful
remark on the form of closed BCCSP terms.

######  Remark 2 (General form of BCCSP processes).

Given any closed BCCSP term $p$, we can assume, without loss of generality,
that $p=\sum_{i\in I}a_{i}p_{i}$ for some finite index set $I$, actions
$a_{i}\in\mathcal{A}$, and closed BCCSP terms $p_{i}$, for $i\in I$. In fact,
in case $p$ is not already in this shape, then by applying axioms A0 and A1 in
Table 3 we can remove superfluous occurrences of $\mathbf{0}$ summands. In
particular, we remark that this transformation does not increase the number of
operator symbols occurring in $p$.

######  Lemma 3.

For all closed _BCCSP_ terms $p$ and $q$ there exists a closed _BCCSP_ term
$r$ such that $\mathcal{E}_{\mathtt{RS}}\vdash p\mathbin{\|}q\approx r$.

######  Proof 3.1.

The proof is by induction on $\mathrm{size}(p)+\mathrm{size}(q)$. Since $p,q$
are closed BCCSP terms, we can assume that $p=\sum_{i\in I}a_{i}p_{i}$ and
$q=\sum_{j\in J}b_{j}q_{j}$ (see Remark 2). We proceed by a case analysis
according to the cardinalities of the sets $I$ and $J$.

  1. (1)

Case $|I|=0$ or $|J|=0$. In that case we can apply axioms P0 and P1 in Table 3
to obtain that either $p\mathbin{\|}q\approx p$ or $p\mathbin{\|}q\approx q$.

  2. (2)

Case $|I|=|J|=1$. Let $I=\\{i_{0}\\}$ and $J=\\{j_{0}\\}$. In this case we
have that

$p\mathbin{\|}q\stackrel{{\scriptstyle(\mathrm{EL2})}}{{\approx}}a_{i_{0}}(p_{i_{0}}\mathbin{\|}b_{j_{0}}q_{j_{0}})+b_{j_{0}}(a_{i_{0}}p_{i_{0}}\mathbin{\|}q_{j_{0}})\enspace,$

so by induction hypothesis there exist closed BCCSP terms $r_{i_{0}}$ and
$r_{j_{0}}$ such that

$p_{i_{0}}\mathbin{\|}b_{j_{0}}q_{j_{0}}\approx r_{i_{0}}\quad\text{ and
}\quad a_{i_{0}}p_{i_{0}}\mathbin{\|}q_{j_{0}}\approx r_{j_{0}}\enspace.$

We can conclude that $p\mathbin{\|}q\approx
a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$, where
$a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$ is a closed BCCSP term.

  3. (3)

Case $|I|=1$ and $|J|>1$. We consider two sub-cases:

     * •

There exist $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$ and
$b_{j_{0}}=b_{j_{1}}$.

In this case we have that

$\displaystyle
p\mathbin{\|}q\stackrel{{\scriptstyle\text{({A2})}}}{{\approx}}$
$\displaystyle
p\mathbin{\|}\left(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j}\right)$
$\displaystyle\stackrel{{\scriptstyle\text{({RSP2})}}}{{\approx}}$
$\displaystyle
a_{i_{0}}\left(p_{i_{0}}\mathbin{\|}(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})\right)$
$\displaystyle+p\mathbin{\|}(b_{j_{0}}q_{j_{0}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})+p\mathbin{\|}(b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j}).$

By the induction hypothesis there exist closed BCCSP terms $r_{1}$, $r_{2}$,
and $r_{3}$ such that

$\displaystyle
a_{i_{0}}\left(p_{i_{0}}\mathbin{\|}(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})\right)\approx r_{1}$
$\displaystyle p\mathbin{\|}(b_{j_{0}}q_{j_{0}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})\approx r_{2}$
$\displaystyle p\mathbin{\|}(b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})\approx r_{3}\enspace.$

We have therefore obtained that $p\mathbin{\|}q\approx
a_{i_{0}}r_{1}+r_{2}+r_{3}$ for the closed BCCSP term
$a_{0}r_{1}+r_{2}+r_{3}$.

     * •

For all $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$ we have $b_{j_{0}}\neq
b_{j_{1}}$.

In this case we have that

$p\mathbin{\|}q\stackrel{{\scriptstyle(\mathrm{EL2})}}{{\approx}}a_{i_{0}}(p_{i_{0}}\mathbin{\|}\sum_{j\in
J}b_{j}q_{j})+\sum_{j\in J}b_{j}(p\mathbin{\|}q_{j})\enspace,$

and the induction hypothesis then gives, for each $j\in J$, a closed BCCSP
term $r_{j}$ such that

$p\mathbin{\|}q_{j}\approx r_{j}$

as well as a closed BCCSP term $r^{\prime}$ such that

$p_{i_{0}}\mathbin{\|}\sum_{j\in J}b_{j}q_{j}\approx r^{\prime}\enspace.$

Therefore, $p\mathbin{\|}q$ is equivalent to the closed BCCSP term
$a_{i_{0}}r^{\prime}+\sum_{j\in J}b_{j}r_{j}$.

  4. (4)

Case $|I|>1$ and $|J|=1$. This case can be handled symmetrically to the case
where $|I|=1$ and $|J|>1$ by applying axiom P1 in Table 3.

  5. (5)

Case $|I|>1$ and $|J|>1$. We consider four sub-cases:

     * •

There exist $i_{0}$ and $i_{1}$ such that $i_{0}\neq i_{1}$ and
$a_{i_{0}}=a_{i_{1}}$, and there exist $j_{0}$ and $j_{1}$ such that
$j_{0}\neq j_{1}$ and $b_{j_{0}}=b_{j_{1}}$.

In this case we have that

$\displaystyle p\mathbin{\|}q\approx{}$
$\displaystyle(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})$
$\displaystyle\stackrel{{\scriptstyle\text{({RSP1})}}}{{\approx}}$
$\displaystyle(a_{i_{0}}p_{i_{0}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})$
$\displaystyle+(a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{1})\mathbin{\|}(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})$
$\displaystyle+(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(b_{j_{0}}q_{j_{0}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})$
$\displaystyle+(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j}).$

By the induction hypothesis there are closed BCCSP terms $r_{1}$, $r_{2}$,
$r_{3}$, and $r_{4}$ such that

$\displaystyle r_{1}\approx{}$ $\displaystyle(a_{i_{0}}p_{i_{0}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})$ $\displaystyle
r_{2}\approx{}$ $\displaystyle(a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{1})\mathbin{\|}(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})$ $\displaystyle
r_{3}\approx{}$
$\displaystyle(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(b_{j_{0}}q_{j_{0}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})$ $\displaystyle
r_{4}\approx{}$
$\displaystyle(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}\\{j_{0},j_{1}\\}}b_{j}q_{j})\enspace.$

Hence $p\mathbin{\|}q$ is equivalent to the closed BCCSP term
$r_{1}+r_{2}+r_{3}+r_{4}$.

     * •

There exist $i_{0}$ and $i_{1}$ such that $i_{0}\neq i_{1}$ and
$a_{i_{0}}=a_{i_{1}}$, and for all $j_{0}$ and $j_{1}$ such that $j_{0}\neq
j_{1}$ we have $b_{j_{0}}\neq b_{j_{1}}$.

In this case we have that

$\displaystyle p\mathbin{\|}q\approx{}$
$\displaystyle(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\mathbin{\|}(\sum_{j\in
J}b_{j}q_{j})$
$\displaystyle\stackrel{{\scriptstyle(\mathrm{P1})}}{{\approx}}$
$\displaystyle(\sum_{j\in
J}b_{j}q_{j})\mathbin{\|}(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})$
$\displaystyle\stackrel{{\scriptstyle(\mathrm{RSP2})}}{{\approx}}$
$\displaystyle\sum_{j\in
J}b_{j}(q_{j}\mathbin{\|}(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i}))$
$\displaystyle+(\sum_{j\in
J}b_{j}q_{j})\mathbin{\|}(a_{i_{0}}p_{i_{0}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})+(\sum_{j\in
J}b_{j}q_{j})\mathbin{\|}(a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i}),$

so the induction hypothesis gives, for each $j\in J$, a closed BCCSP term
$r_{j}$ such that

$r_{j}\approx
q_{j}\mathbin{\|}(a_{i_{0}}p_{i_{0}}+a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i}),$

as well as closed BCCSP terms $r^{\prime}$ and $r^{\prime\prime}$ such that

$\displaystyle r^{\prime}\approx{}$ $\displaystyle(\sum_{j\in
J}b_{j}q_{j})\mathbin{\|}(a_{i_{0}}p_{i_{0}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})$ $\displaystyle
r^{\prime\prime}\approx{}$ $\displaystyle(\sum_{j\in
J}b_{j}q_{j})\mathbin{\|}(a_{i_{1}}p_{i_{1}}+\sum_{i\in
I\mathbin{\backslash}\\{i_{0},i_{1}\\}}a_{i}p_{i})\enspace.$

Thus $p\mathbin{\|}q$ is equivalent to the closed BCCSP term $\sum_{j\in
J}b_{j}r_{j}+r^{\prime}+r^{\prime\prime}$.

     * •

For all $i_{0}$ and $i_{1}$ such that $i_{0}\neq i_{1}$ we have $a_{i_{0}}\neq
a_{i_{1}}$, and there exist $j_{0}$ and $j_{1}$ such that $j_{0}\neq j_{1}$
and $b_{j_{0}}=b_{j_{1}}$.

This case follows by applying a symmetrical argument to that used in the
previous item and it is therefore omitted.

     * •

For all $i_{0}$ and $i_{1}$ such that $i_{0}\neq i_{1}$ we have $a_{i_{0}}\neq
a_{i_{1}}$, and for all $j_{0}$ and $j_{1}$ such that $j_{0}\neq j_{1}$ we
have $b_{j_{0}}\neq b_{j_{1}}$.

In this case we have that

$p\mathbin{\|}q\approx\sum_{i\in I}a_{i}p_{i}\mathbin{\|}\sum_{j\in
J}b_{j}q_{j}$

and all the conditions for an application of axiom EL2 in Table4 are
satisfied. Hence

$p\mathbin{\|}q\stackrel{{\scriptstyle(\textrm{EL2})}}{{\approx}}\sum_{i\in
I}a_{i}(p_{i}\mathbin{\|}\sum_{j\in J}b_{j}q_{j})+\sum_{j\in
J}b_{j}(\sum_{i\in I}a_{i}p_{i}\mathbin{\|}q_{j}),$

and by the induction hypothesis there exist, for each $i\in I$, a closed BCCSP
term $r_{i}$ such that

$r_{i}\approx p_{i}\mathbin{\|}\sum_{j\in J}b_{j}q_{j}\enspace,$

and for each $j\in J$, a closed BCCSP term $r_{j}^{\prime}$ such that

$r_{j}^{\prime}\approx\sum_{i\in I}a_{i}p_{i}\mathbin{\|}q_{j}\enspace.$

Therefore $p\mathbin{\|}q$ is equivalent to the closed BCCSP term $\sum_{i\in
I}a_{i}r_{i}+\sum_{j\in J}b_{j}r_{j}^{\prime}$.

######  Proposition 4 ($\mathcal{E}_{\mathtt{RS}}$ elimination).

For every closed $\mathrm{BCCSP}_{\scriptsize\|}$ term $p$ there exists a
_BCCSP_ term $q$ such that $\mathcal{E}_{\mathtt{RS}}\vdash p\approx q$.

######  Proof 3.2.

Straightforward by induction on the structure of $p$, using Lemma 3 in the
case that $p$ is of the form $p_{1}\mathbin{\|}p_{2}$ for some processes
$p_{1}$ and $p_{2}$.

The ground-completeness of $\mathcal{E}_{\mathtt{RS}}$ then follows from the
ground-completeness of $\mathcal{E}_{0}\cup\\{\mathrm{RS}\\}$ over BCCSP [19].

######  Theorem 5 ($\mathcal{E}_{\mathtt{RS}}$ completeness).

The axiom system $\mathcal{E}_{\mathtt{RS}}$ is a ground-complete
axiomatisation of $\mathrm{BCCSP}_{\scriptsize\|}$ modulo ready simulation
equivalence, i.e., whenever $p\sim_{\mathtt{RS}}q$ then
$\mathcal{E}_{\mathtt{RS}}\vdash p\approx q$.

We remark that since axioms RSP1, RSP2, and EL2 are sound modulo ready
simulation equivalence, they are automatically sound modulo all the
equivalences in the spectrum that are coarser than $\sim_{\mathtt{RS}}$,
namely the completed simulation, simulation, and (decorated) trace
equivalences. Hence, we can easily obtain finite, ground-complete
axiomatisations of $\mathrm{BCCSP}_{\scriptsize\|}$ modulo each of those
equivalences by adding RSP1, RSP2 and EL2 to the respective ground-complete
axiomatisations of BCCSP that have been proposed in the literature [19, 8].
However, for each of those equivalences we can provide stronger axioms that
give a more elegant characterisation of the distributivity properties of
$\mathbin{\|}$ over $+$. In particular, the axiom schema RSP2 yields
$|\mathcal{A}|\cdot 2^{|\mathcal{A}|}$ equational axioms and EL2 yields
$2^{2|\mathcal{A}|}$ equational axioms. By exploiting the various forms of
distributivity of parallel composition over choice, we can obtain more concise
ground-complete axiomatisations of $\mathrm{BCCSP}_{\scriptsize\|}$ modulo the
coarser equivalences. We devote the next two sections to the presentation of
these results.

##  4\. Completed simulation and simulation

In this section we refine the axiom system $\mathcal{E}_{\mathtt{RS}}$ to
obtain finite, ground-complete axiomatisations of
$\mathrm{BCCSP}_{\scriptsize\|}$ modulo completed simulation and simulation
equivalences. To this end, we replace RSP1 and RSP2 with new axioms, tailored
for the considered semantics, that allow us to obtain the elimination of
$\mathbin{\|}$ from closed $\mathrm{BCCSP}_{\scriptsize\|}$ terms, while using
less restrictive forms of distributivity of $\mathbin{\|}$ over $+$.

(CS) $a(bx+y+z)\approx a(bx+y+z)+a(bx+z)$
---
(CSP1)
$(ax+by+u)\mathbin{\|}(cz+dw+v)\approx(ax+u)\mathbin{\|}(cz+dw+v)+(by+u)\mathbin{\|}(cz+dw+v)+$
$(ax+by+u)\mathbin{\|}(cz+dw+v)\approx$
$+(ax+by+u)\mathbin{\|}(cz+v)+(ax+by+u)\mathbin{\|}(dw+v)$
(CSP2) $ax\mathbin{\|}(by+cz+w)\approx
a(x\mathbin{\|}(by+cz+w))+ax\mathbin{\|}(by+w)+ax\mathbin{\|}(cz+w)$
$\mathcal{E}_{\mathtt{CS}}=\mathcal{E}_{1}\cup\\{\textrm{CS, CSP1, CSP2,
EL1}\\}$
(S) $a(x+y)\approx a(x+y)+ax$
(SP1) $(x+y)\mathbin{\|}(z+w)\approx
x\mathbin{\|}(z+w)+y\mathbin{\|}(z+w)+(x+y)\mathbin{\|}z+(x+y)\mathbin{\|}w$
(SP2) $ax\mathbin{\|}(y+z)\approx
a(x\mathbin{\|}(y+z))+ax\mathbin{\|}y+ax\mathbin{\|}z$
$\mathcal{E}_{\mathtt{S}}=\mathcal{E}_{1}\cup\\{\textrm{S, SP1, SP2, EL1}\\}$
Table 6.  Additional axioms for (completed) simulation equivalence.

Let us focus first on completed simulation equivalence. We can use axioms CSP1
and CSP2 in Table 6 to characterise restricted forms of distributivity of
$\mathbin{\|}$ over $+$ modulo $\sim_{\mathtt{CS}}$. Intuitively, CSP1 is the
_completed simulation counterpart_ of RSP1, and CSP2 is that of RSP2. Notice
that both CSP1 and CSP2 are such that, when distributing $\mathbin{\|}$ over
$+$, we never obtain $\mathbf{0}$ as an argument of $\mathbin{\|}$, thus
guaranteeing their soundness modulo $\sim_{\mathtt{CS}}$. Moreover, we stress
that CSP1 and CSP2 are not sound modulo ready simulation equivalence. This is
due to the fact that both axioms allow for distributing $\mathbin{\|}$ over
$+$ regardless of the initial actions of the summands. It is then immediate to
check that, for instance,
$a\mathbin{\|}(b+c)\not\sim_{\mathtt{RS}}a\mathbin{\|}b+a\mathbin{\|}c+a\mathbin{\|}(b+c)$,
whereas
$a\mathbin{\|}(b+c)\sim_{\mathtt{CS}}a\mathbin{\|}b+a\mathbin{\|}c+a\mathbin{\|}(b+c)$.
Interestingly, due to the relaxed constraints on distributivity, by
(repeatedly) applying CSP1 and CSP2, from left to right, we are able to reduce
a $\mathrm{BCCSP}_{\scriptsize\|}$ process of the form $(\sum_{i\in
I}p_{i})\mathbin{\|}(\sum_{j\in J}p_{j})$ to a
$\mathrm{BCCSP}_{\scriptsize\|}$ process of the form $\sum_{k\in K}p_{k}$ such
that whenever $p_{k}$ has $\mathbin{\|}$ as head operator then
$p_{k}=a_{k}q_{k}\mathbin{\|}b_{k}q^{\prime}_{k}$ for some
$q_{k},q^{\prime}_{k}$. We can then use the refinement EL1 of the expansion
law to proceed with the elimination of $\mathbin{\|}$ from these terms.

Consider the axiom system
$\mathcal{E}_{\mathtt{CS}}=\mathcal{E}_{1}\cup\\{\textrm{CS,CSP1,CSP2,EL1}\\}$.
We can formalise the elimination result for $\sim_{\mathtt{CS}}$ as a direct
consequence of the following result.

######  Lemma 6.

For all closed _BCCSP_ terms $p$ and $q$ there exists a closed _BCCSP_ term
$r$ such that $\mathcal{E}_{\mathtt{CS}}\vdash p\mathbin{\|}q\approx r$.

######  Proof 4.1.

The proof is by induction on $\mathrm{size}(p)+\mathrm{size}(q)$. First note
that, since $p$ and $q$ are closed BCCSP terms, we may assume that
$p=\sum_{i\in I}a_{i}p_{i}$ and $q=\sum_{j\in J}b_{j}q_{j}$ (see Remark 2).

We proceed by a case analysis according to the cardinalities of the sets $I$
and $J$.

  1. (1)

Case ${|I|}=0$ or ${|J|}=0$. First note that if ${|J|}=0$, i.e.,
$J=\emptyset$, then $q=\mathbf{0}$, so $p\mathbin{\|}q\approx p$ by P0, and
$p$ is the required closed BCCSP term. Similarly, if ${|I|}=0$, i.e.,
$I=\emptyset$, then $p=\mathbf{0}$, so $p\mathbin{\|}q\approx
q\mathbin{\|}p\approx q$ by P1 and P0 in Table 3, and $q$ is the required
closed BCCSP term.

  2. (2)

Case ${|I|}={|J|}=1$. Let $I=\\{i_{0}\\}$ and $J=\\{j_{0}\\}$, then

$p\mathbin{\|}q\stackrel{{\scriptstyle\text{(EL1)}}}{{\approx}}a_{i_{0}}(p_{i_{0}}\mathbin{\|}q)+b_{j_{0}}(p\mathbin{\|}q_{j_{0}})\enskip.$

Since $\mathrm{size}(p_{i_{0}})<\mathrm{size}(p)$ and
$\mathrm{size}(q_{j_{0}})<\mathrm{size}(q)$, by the induction hypothesis there
exist closed BCCSP terms $r_{i_{0}}$ and $r_{j_{0}}$ such that
${p_{i_{0}}\mathbin{\|}q}\approx r_{i_{0}}$ and
${p\mathbin{\|}q_{j_{0}}}\approx r_{j_{0}}$. It follows that
$p\mathbin{\|}q\approx a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$ and clearly
$a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$ is a closed BCCSP term.

  3. (3)

Case ${|I|}=1$ and $|J|>1$. We can then assume that $I=\\{i_{0}\\}$ and there
exist $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$, then

$\textstyle
p\mathbin{\|}q\stackrel{{\scriptstyle\text{(CSP2)}}}{{\approx}}a_{i_{0}}(p_{i}\mathbin{\|}q)+p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{0}\\}}}}b_{j}q_{j}\right)+p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{1}\\}}}}b_{j}q_{j}\right)\enskip.$

Since $\mathrm{size}(p_{i_{0}})<\mathrm{size}(p)$,
$\mathrm{size}(\sum_{j\in{J\mathbin{\backslash}{\\{j_{0}\\}}}}b_{j}q_{j})<\mathrm{size}(q)$
and
$\mathrm{size}(\sum_{j\in{J\mathbin{\backslash}{\\{j_{1}\\}}}}b_{j}q_{j})<\mathrm{size}(q)$,
by the induction hypothesis there exist closed BCCSP terms $r_{i_{0}}$,
$r_{j_{0}}$ and $r_{j_{1}}$ such that

$p_{i_{0}}\mathbin{\|}q\approx r_{i_{0}}\qquad
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{0}\\}}}}b_{j}q_{j}\right)\approx
r_{j_{0}}\quad\text{ and }\quad
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{1}\\}}}}b_{j}q_{j}\right)\approx
r_{j_{1}}\enspace.$

So we have $p\mathbin{\|}q\approx a_{i_{0}}r_{i_{0}}+r_{j_{0}}+r_{j_{1}}$ and
$a_{i_{0}}r_{i_{0}}+r_{j_{0}}+r_{j_{1}}$ is a closed BCCSP term.

  4. (4)

Case $|I|>1$ and ${|J|}=1$. The proof is similar as in the previous case, with
an additional application of axiom P1 in Table 3.

  5. (5)

Case $|I|,|J|>1$. In this case there exist $i_{0},i_{1}\in I$ with $i_{0}\neq
i_{1}$ and $j_{0},j_{1}\in J$ with $j_{0}\neq j_{1}$. Then

$\displaystyle
p\mathbin{\|}q\stackrel{{\scriptstyle\text{(CSP1)}}}{{\approx}}$
$\displaystyle\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{0}\\}}}a_{i}p_{i}\right)\mathbin{\|}q+\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{1}\\}}}a_{i}p_{i}\right)\mathbin{\|}q$
$\displaystyle+p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{0}\\}}}b_{j}q_{j}\right)+p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{1}\\}}}b_{j}q_{i}\right)\enskip.$

Note that
$\mathrm{size}(\sum_{i\in{I\mathbin{\backslash}\\{i_{0}\\}}}a_{i}p_{i})<\mathrm{size}(p)$,
$\mathrm{size}(\sum_{i\in{I\mathbin{\backslash}\\{i_{1}\\}}}a_{i}p_{i})<\mathrm{size}(p)$,
$\mathrm{size}(\sum_{j\in{J\mathbin{\backslash}\\{j_{0}\\}}}b_{j}q_{j})<\mathrm{size}(q)$
and
$\mathrm{size}(\sum_{j\in{J\mathbin{\backslash}\\{j_{1}\\}}}b_{j}q_{i})<\mathrm{size}(q)$,
so by the induction hypothesis there exist $r_{i_{0}}$, $r_{i_{1}}$,
$r_{j_{0}}$ and $r_{j_{1}}$ such that

$\displaystyle\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{0}\\}}}a_{i}p_{i}\right)\mathbin{\|}q\approx
r_{i_{0}},$
$\displaystyle\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{1}\\}}}a_{i}p_{i}\right)\mathbin{\|}q\approx
r_{i_{1}}$ $\displaystyle
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{0}\\}}}b_{j}q_{j}\right)\approx
r_{j_{0}}$ $\displaystyle
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{1}\\}}}b_{j}q_{i}\right)\approx
r_{j_{1}}\enspace.$

It follows that $p\mathbin{\|}q\approx
r_{i_{0}}+r_{i_{1}}+r_{j_{0}}+r_{j_{1}}$ and
$r_{i_{0}}+r_{i_{1}}+r_{j_{0}}+r_{j_{1}}$ is a closed BCCSP term.

######  Proposition 7 ($\mathcal{E}_{\mathtt{CS}}$ elimination).

For every closed $\mathrm{BCCSP}_{\scriptsize\|}$ term $p$ there exists a
_BCCSP_ term $q$ such that $\mathcal{E}_{\mathtt{CS}}\vdash p\approx q$.

######  Proof 4.2.

Straightforward by induction on the structure of $p$, using Lemma 6 in the
case that $p$ is of the form $p_{1}\mathbin{\|}p_{2}$ for some $p_{1}$ and
$p_{2}$.

A similar reasoning could be applied to obtain the elimination result for
simulation equivalence. Although this result could be directly derived by the
soundness of CSP1 and CSP2 modulo simulation equivalence, stronger
distributivity properties for parallel composition over summation hold modulo
$\sim_{\mathtt{S}}$. Instead of CSP1 and CSP2, we include SP1 and SP2 in Table
6, letting
$\mathcal{E}_{\mathtt{S}}=\mathcal{E}_{1}\cup\\{\textrm{S,SP1,SP2,EL1}\\}$. By
showing that the axioms CS, CSP1 and CSP2 are derivable from
$\mathcal{E}_{\mathtt{S}}$, we can obtain the elimination result for
simulation equivalence as an immediate corollary of that for completed
simulation.

######  Lemma 8.

The axioms of the system $\mathcal{E}_{\mathtt{CS}}$ are derivable from the
axiom system $\mathcal{E}_{\mathtt{S}}$, namely:

  1. (1)

$\mathcal{E}_{\mathtt{S}}\vdash\mathrm{CS}$,

  2. (2)

$\mathcal{E}_{\mathtt{S}}\vdash\mathrm{CSP1}$, and

  3. (3)

$\mathcal{E}_{\mathtt{S}}\vdash\mathrm{CSP2}$.

######  Proof 4.3.

We start with the derivation of CS. We have the following equational
derivation:

$\displaystyle a(bx+y+z)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{(A1),(A2)}}}{{\approx}}$
$\displaystyle a(bx+z+y)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{(S)}}}{{\approx}}$ $\displaystyle
a(bx+z+y)+a(bx+z)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{(A1),(A2)}}}{{\approx}}$
$\displaystyle a(bx+y+z)+a(bx+z)\enskip.$

In the case of CSP1, we have the following equational derivation:

$\displaystyle(ax+by+u)\mathbin{\|}(cz+dw+v)$
$\displaystyle\quad\makebox[38.11116pt]{$\stackrel{{\scriptstyle\mathrm{(A1),(A3)}}}{{\approx}}$}(ax+u+by+u)\mathbin{\|}(cz+v+dw+v)$
$\displaystyle\quad\makebox[38.11116pt]{$\stackrel{{\scriptstyle\mathrm{(SP1)}}}{{\approx}}$}(ax+u)\mathbin{\|}(cz+v+dw+v)+(by+u)\mathbin{\|}(cz+v+dw+v)$
$\displaystyle\qquad\qquad\qquad\mbox{}+(ax+u+by+u)\mathbin{\|}(cz+v)+(ax+u+by+u)\mathbin{\|}(dw+v)$
$\displaystyle\quad\makebox[38.11116pt]{$\stackrel{{\scriptstyle\mathrm{(A1),(A3)}}}{{\approx}}$}(ax+u)\mathbin{\|}(cz+dw+v)+(by+u)\mathbin{\|}(cz+dw+v)$
$\displaystyle\qquad\qquad\qquad\mbox{}+(ax+by+u)\mathbin{\|}(cz+v)+(ax+by+u)\mathbin{\|}(dw+v)\enskip.$

Finally, for CSP2 we have the following equational derivation:

$\displaystyle ax\mathbin{\|}(by+cz+w)$
$\displaystyle\quad\makebox[38.11116pt]{$\stackrel{{\scriptstyle\mathrm{(A1),(A3)}}}{{\approx}}$}ax\mathbin{\|}(by+w+cz+w)$
$\displaystyle\quad\makebox[38.11116pt]{$\stackrel{{\scriptstyle\mathrm{(SP2)}}}{{\approx}}$}a(x\mathbin{\|}(by+w+cz+w))+ax\mathbin{\|}(by+w)+ax\mathbin{\|}(cz+w)$
$\displaystyle\quad\makebox[38.11116pt]{$\stackrel{{\scriptstyle\mathrm{(A1),(A3)}}}{{\approx}}$}a(x\mathbin{\|}(by+cz+w))+ax\mathbin{\|}(by+w)+ax\mathbin{\|}(cz+w)\enskip.$

######  Proposition 9 ($\mathcal{E}_{\mathtt{S}}$ elimination).

For every closed $\mathrm{BCCSP}_{\scriptsize\|}{}$ term $p$ there exists a
closed _BCCSP_ term $q$ such that $\mathcal{E}_{\mathtt{S}}\vdash p\approx q$.

######  Remark 10.

As we showed in Lemma 8, the axiom system $\mathcal{E}_{\mathtt{S}}$ proves
all the equations in $\mathcal{E}_{\mathtt{CS}}$. A natural question at this
point is whether all the equations in $\mathcal{E}_{\mathtt{RS}}$ can be
derived from $\mathcal{E}_{\mathtt{CS}}$. Indeed, that result would allow one
to infer Proposition 7 (the elimination result for completed simulation
equivalence) from Proposition 4 (the elimination result for ready simulation
equivalence). The answer is negative, as it is not possible to derive EL2 from
$\mathcal{E}_{\mathtt{CS}}$ . To prove this claim, we have used Mace4 [25] to
generate a model for $\mathcal{E}_{\mathtt{CS}}$ in which EL2 does not hold
(if there are at least two actions). The code can be found in Appendix A.
Below, we only present the model and show that it does not satisfy EL2. The
verification that the model indeed satisfies the axioms of
$\mathcal{E}_{\mathtt{CS}}$ is lengthy and tedious. We used the mCRL2 toolset
[20, 10] to double check the correctness of the model produced by Mace4.

$a$: | 0 | 1 | 2 | 3 | 4
---|---|---|---|---|---
| 2 | 2 | 3 | 4 | 4

$b$: | 0 | 1 | 2 | 3 | 4
---|---|---|---|---|---
| 3 | 2 | 3 | 4 | 4

$\mathbin{\|}$: | 0 | 1 | 2 | 3 | 4
---|---|---|---|---|---
0 | 0 | 1 | 2 | 3 | 4
1 | 1 | 0 | 2 | 1 | 2
2 | 2 | 2 | 3 | 4 | 4
3 | 3 | 1 | 4 | 4 | 4
4 | 4 | 2 | 4 | 4 | 4

$+$: | 0 | 1 | 2 | 3 | 4
---|---|---|---|---|---
0 | 0 | 1 | 2 | 3 | 4
1 | 1 | 1 | 2 | 3 | 4
2 | 2 | 2 | 2 | 4 | 4
3 | 3 | 3 | 4 | 3 | 4
4 | 4 | 4 | 4 | 4 | 4

Table 7.  A model for $\mathcal{E}_{\mathtt{CS}}$ and
$\mathcal{E}_{\mathtt{CT}}$.

Let $\mathcal{A}=\\{a,b\\}$, and consider the model with carrier set
$\\{0,1,2,3,4\\}$ and the operations defined in Table 7. This model does not
satisfy

$(ax+by)\mathbin{\|}(az+bw)\approx
a(x\mathbin{\|}(az+bw))+b(y\mathbin{\|}(az+bw))+a((ax+by)\mathbin{\|}z)+b((ax+by)\mathbin{\|}w)$

for, e.g., the valuation $x=0$, $y=0$, $z=1$, and $w=1$.

In light of the results above, and those in [19] showing that
$\mathcal{E}_{0}\cup\\{\mathrm{CS}\\}$ and
$\mathcal{E}_{0}\cup\\{\mathrm{S}\\}$ are sound and ground-complete
axiomatisations of BCCSP modulo $\sim_{\mathtt{CS}}$ and $\sim_{\mathtt{S}}$,
respectively, we can infer that $\mathcal{E}_{\mathtt{CS}}$ and
$\mathcal{E}_{\mathtt{S}}$ are ground-complete axiomatisations of
$\mathrm{BCCSP}_{\scriptsize\|}$ modulo completed simulation equivalence and
simulation equivalence, respectively.

######  Theorem 11 (Soundness and completeness of $\mathcal{E}_{\mathtt{CS}}$
and $\mathcal{E}_{\mathtt{S}}$).

Let $\mathtt{X}\in\\{\mathtt{CS},\mathtt{S}\\}$. The axiom system
$\mathcal{E}_{\mathtt{X}}$ is a sound, ground-complete axiomatisation of
$\mathrm{BCCSP}_{\scriptsize\|}$ modulo $\sim_{\mathtt{X}}$, i.e.,
$p\sim_{\mathtt{X}}q$ if and only if $\mathcal{E}_{\mathtt{X}}\vdash p\approx
q$.

At the end of Section 3 we noticed that the size of
$\mathcal{E}_{\mathtt{RS}}$ is exponential in $\mathcal{A}$. Now, as a final
remark, we observe that the size of $\mathcal{E}_{\mathtt{CS}}$ is polynomial
in $|\mathcal{A}|$, and the size of $\mathcal{E}_{\mathtt{S}}$ is linear in
$|\mathcal{A}|$. In detail, $\mathcal{E}_{\mathtt{CS}}$ contains
$|\mathcal{A}|^{2}$ equations that are instances of CS, $|\mathcal{A}|^{4}$
equations that are instances of CSP1, and $|\mathcal{A}|^{3}$ equations
arising from (CSP2). On the other hand, in $\mathcal{E}_{\mathtt{S}}$, the
axiom schemata S and SP2 yield $|\mathcal{A}|$ equations each, whereas SP1 is
just one equation.

##  5\. Linear semantics: from ready traces to traces

We continue our journey in the spectrum by moving to the linear-time
semantics. In this section we consider trace semantics and all of its
decorated versions, and we provide a finite, ground-complete axiomatisation
for each of them (see Table 8).

(RT) $a\left(\sum_{i=1}^{|\mathcal{A}|}(b_{i}x_{i}+b_{i}y_{i})+z\right)\approx
a\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}y_{i}+z\right)$
---
(FP) $(ax+ay+w)\mathbin{\|}z\approx(ax+w)\mathbin{\|}z+(ay+w)\mathbin{\|}z$
$\mathcal{E}_{\mathtt{RT}}=\mathcal{E}_{1}\cup\\{\textrm{RT},\textrm{FP},\textrm{EL2}\\}$
(FT) $ax+ay\approx ax+ay+a(x+y)$
$\mathcal{E}_{\mathtt{FT}}=\mathcal{E}_{1}\cup\\{\textrm{FT},\textrm{RS},\textrm{FP},\textrm{EL2}\\}$
(R) $a(bx+z)+a(by+w)\approx a(bx+by+z)+a(by+w)$
$\mathcal{E}_{\mathtt{R}}=\mathcal{E}_{1}\cup\\{\textrm{R, FP, EL2}\\}$
(F) $ax+a(y+z)\approx ax+a(x+y)+a(y+z)$
$\mathcal{E}_{\mathtt{F}}=\mathcal{E}_{1}\cup\\{\textrm{F, R, FP, EL2}\\}$
Table 8. Additional axioms for ready (trace) and failure (trace) equivalences.

From a technical point of view, we can split the results of this section into
two parts:

  1. (1)

those for ready trace, failure trace, ready, and failures equivalence, and

  2. (2)

those for completed trace, and trace equivalence.

In both parts we prove the elimination result only for the finest semantics,
namely ready trace (Proposition 13) and completed trace (Proposition 20)
respectively. We then obtain the remaining elimination results by showing that
all the axioms in $\mathcal{E}_{\mathtt{X}}$ are provable from
$\mathcal{E}_{\mathtt{Y}}$, where $\mathtt{X}$ is finer than $\mathtt{Y}$ in
the considered part.

###  5.1. From ready traces to failures

First we deal with the decorated trace semantics based on the comparison of
the failure and ready sets of processes.

[Readiness and failures equivalences]

  * •

A _failure pair_ of a process $p$ is a pair $(\alpha,X)$, with
$\alpha\in\mathcal{A}^{*}$ and $X\subseteq\mathcal{A}$, such that
$p\xrightarrow{\,{\alpha}\,}q$ for some process $q$ with $\mathtt{I}(q)\cap
X=\emptyset$. We denote by $\mathtt{F}(p)$ the set of failure pairs of $p$.
Two processes $p$ and $q$ are _failures equivalent_ , denoted
$p\sim_{\mathtt{F}}q$, if $\mathtt{F}(p)=\mathtt{F}(q)$.

  * •

A _ready pair_ of a process $p$ is a pair $(\alpha,X)$, with
$\alpha\in\mathcal{A}^{*}$ and $X\subseteq\mathcal{A}$, such that
$p\xrightarrow{\,{\alpha}\,}q$ for some process $q$ with $\mathtt{I}(q)=X$. We
let $\mathtt{R}(p)$ denote the set of ready pairs of $p$. Two processes $p$
and $q$ are _ready equivalent_ , written $p\sim_{\mathtt{R}}q$, if
$\mathtt{R}(p)=\mathtt{R}(q)$.

  * •

A _failure trace_ of a process $p$ is a sequence $X_{0}a_{1}X_{1}\dots
a_{n}X_{n}$, with $X_{i}\subseteq\mathcal{A}$ and $a_{i}\in\mathcal{A}$, such
that there are $p_{1},\dots,p_{n}\in\mathcal{P}$ with
$p=p_{0}\xrightarrow{\,{a_{1}}\,}p_{1}\xrightarrow{\,{a_{2}}\,}\dots\xrightarrow{\,{a_{n}}\,}p_{n}$
and $\mathtt{I}(p_{i})\cap X_{i}=\emptyset$ for all $0\leq i\leq n$. We write
$\mathtt{FT}(p)$ for the set of failure traces of $p$. Two processes $p$ and
$q$ are _failure trace equivalent_ , denoted $p\sim_{\mathtt{FT}}q$, if
$\mathtt{FT}(p)=\mathtt{FT}(q)$.

  * •

A _ready trace_ of a process $p$ is a sequence $X_{0}a_{1}X_{1}\dots
a_{n}X_{n}$, for $X_{i}\subseteq\mathcal{A}$ and $a_{i}\in\mathcal{A}$, such
that there are $p_{1},\dots p_{n}\in\mathcal{P}$ with
$p=p_{0}\xrightarrow{\,{a_{1}}\,}p_{1}\xrightarrow{\,{a_{2}}\,}\dots\xrightarrow{\,{a_{n}}\,}p_{n}$
and $\mathtt{I}(p_{i})=X_{i}$ for all $0\leq i\leq n$. We write
$\mathtt{RT}(p)$ for the set of ready traces of $p$. Two processes $p$ and $q$
are _ready trace equivalent_ , denoted $p\sim_{\mathtt{RT}}q$, if
$\mathtt{RT}(p)=\mathtt{RT}(q)$.

We consider first the finest equivalence among those in Definition 5.1, namely
ready trace equivalence. This can be considered as the linear counterpart of
ready simulation: we focus on the current execution of the process and we
require that each step is mimicked by reaching processes having the same sets
of initial actions. Interestingly, we can find a similar correlation between
the axioms characterising the distributivity of $\mathbin{\|}$ over $+$ modulo
the two semantics. Consider axiom FP in Table 8. We can see this axiom as the
_linear_ counterpart of RSP1: since in the linear semantics we are interested
only in the current execution of a process, we can characterise the
distributivity of $\mathbin{\|}$ over $+$ by treating the two arguments of
$\mathbin{\|}$ independently from one another. To obtain the elimination
result for $\sim_{\mathtt{RT}}$ we do not need to introduce the linear
counterpart of axiom RSP2. In fact, FP imposes constraints on the form of only
one argument of $\mathbin{\|}$. Hence, it is possible to use it to reduce any
process of the form $(\sum_{i\in I}p_{i})\mathbin{\|}(\sum_{j\in J}p_{j})$
into a sum of processes to which EL2 can be applied. We can in fact prove that
the axioms in the system
$\mathcal{E}_{\mathtt{RT}}=\mathcal{E}_{1}\cup\\{\mathrm{RT,FP,EL2}\\}$ are
sufficient to eliminate all occurrences of $\mathbin{\|}$ from closed
$\mathrm{BCCSP}_{\scriptsize\|}$ terms.

######  Lemma 12.

For all closed _BCCSP_ terms $p,q$ there exists a closed _BCCSP_ term $r$ such
that $\mathcal{E}_{\mathtt{RT}}\vdash p\mathbin{\|}q\approx r$.

######  Proof 5.1.

The proof proceeds by induction on the total number of operator symbols
occurring in $p$ and $q$ together, not counting parentheses. First of all we
notice that, since $p$ and $q$ are closed BCCSP terms, we can assume that
$p=\sum_{i\in I}a_{i}p_{i}$ and $q=\sum_{j\in J}b_{j}q_{j}$ (see Remark 2).

We proceed by a case analysis according to the cardinalities of the sets $I$
and $J$.

  1. (1)

Case ${|I|}=0$ or ${|J|}=0$. In case that ${|J|}=0$, i.e., $J=\emptyset$, then
$q=\mathbf{0}$, so $\mathcal{E}_{\mathtt{RT}}\vdash p\mathbin{\|}q\approx p$
by P0, and $p$ is the required closed BCCSP term. Similarly, if ${|I|}=0$,
i.e., $I=\emptyset$, then $p=\mathbf{0}$, so $\mathcal{E}_{\mathtt{RT}}\vdash
p\mathbin{\|}q\approx q\mathbin{\|}p\approx q$ by P0 and P1 in Table 3, and
$q$ is the required closed BCCSP term.

  2. (2)

Case ${|I|}={|J|}=1$. Let $I=\\{i_{0}\\}$ and $J=\\{j_{0}\\}$, then

$p\mathbin{\|}q\stackrel{{\scriptstyle\text{(EL2)}}}{{\approx}}a_{i_{0}}(p_{i_{0}}\mathbin{\|}q)+b_{j_{0}}(p\mathbin{\|}q_{j_{0}})\enspace.$

Since both $p_{i_{0}}$ and $q_{j_{0}}$ have fewer symbols than $p$ and $q$,
respectively, by the inductive hypothesis there exist closed BCCSP terms
$r_{i_{0}}$ and $r_{j_{0}}$ such that $\mathcal{E}_{\mathtt{RT}}\vdash
p_{i_{0}}\mathbin{\|}q\approx r_{i_{0}}$ and $\mathcal{E}_{\mathtt{RT}}\vdash
p\mathbin{\|}q_{j_{0}}\approx r_{j_{0}}$. It follows that
$\mathcal{E}_{\mathtt{RT}}\vdash p\mathbin{\|}q\approx
a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$, where
$a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$ is a closed BCCSP term.

  3. (3)

Case ${|I|}=1$ and $|J|>1$. We can then assume that $I=\\{i_{0}\\}$ and there
exist $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$. We can now distinguish
two cases, according to whether $b_{j_{0}}=b_{j_{1}}$ for some $j_{0},j_{1}\in
J$ with $j_{0}\neq j_{1}$, or not.

     * •

There are some $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$ and
$b_{j_{0}}=b_{j_{1}}$.

In this case we have that

$p\mathbin{\|}q\;\stackrel{{\scriptstyle\text{(P1)}}}{{\approx}}\;\left(\sum_{j\in
J}b_{j}q_{j}\right)\mathbin{\|}p\;\stackrel{{\scriptstyle\text{(FP)}}}{{\approx}}\;\left(\sum_{j\in
J\mathbin{\backslash}{\\{j_{0}\\}}}b_{j}q_{j}\right)\mathbin{\|}p+\left(\sum_{j\in
J\mathbin{\backslash}{\\{j_{1}\\}}}b_{j}q_{j}\right)\mathbin{\|}p\enspace.$

Since both $\sum_{j\in J\mathbin{\backslash}{\\{j_{0}\\}}}b_{j}q_{j}$ and
$\sum_{j\in J\mathbin{\backslash}{\\{j_{1}\\}}}b_{j}q_{j}$ have fewer operator
symbols than $q$, by the inductive hypothesis there exist closed BCCSP terms
$r_{j_{0}}$ and $r_{j_{1}}$ such that

$\mathcal{E}_{\mathtt{RT}}\vdash\left(\sum_{j\in
J\mathbin{\backslash}{\\{j_{0}\\}}}b_{j}q_{j}\right)\mathbin{\|}p\approx
r_{j_{0}}\quad\text{ and }\quad\mathcal{E}_{\mathtt{RT}}\vdash\left(\sum_{j\in
J\mathbin{\backslash}{\\{j_{1}\\}}}b_{j}q_{j}\right)\mathbin{\|}p\approx
r_{j_{1}}\enspace.$

Therefore, we get that $\mathcal{E}_{\mathtt{RT}}\vdash p\mathbin{\|}q\approx
r_{j_{0}}+r_{j_{1}}$, where $r_{j_{0}}+r_{j_{1}}$ is a closed BCCSP term.

     * •

For all $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$ it holds that
$b_{j_{0}}\neq b_{j_{1}}$. In this case we have that

$p\mathbin{\|}q\stackrel{{\scriptstyle\text{(EL2)}}}{{\approx}}a_{i_{0}}(p_{i_{0}}\mathbin{\|}q)+\sum_{j\in
J}b_{j}(p\mathbin{\|}q_{j})\enspace,$

where $p_{i_{0}}$ has fewer operator symbols than $p$ and each $q_{j}$ has
fewer operator symbols than $q$. Hence, by the inductive hypothesis, we obtain
that there is a closed BCCSP term $r_{i_{0}}$ such that

$\mathcal{E}_{\mathtt{RT}}\vdash p_{i_{0}}\mathbin{\|}q\approx
r_{i_{0}}\enspace,$

and for each $j\in J$ there is a closed BCCSP term $r_{j}$ such that

$\mathcal{E}_{\mathtt{RT}}\vdash p\mathbin{\|}q_{j}\approx r_{j}\enspace.$

We can thus conclude that $\mathcal{E}_{\mathtt{RT}}\vdash
p\mathbin{\|}q\approx a_{i_{0}}r_{i_{0}}+\sum_{j\in J}b_{j}r_{j}$, where the
right hand side of the equation is a closed BCCSP term.

  4. (4)

Case $|I|>1$ and ${|J|}=1$. The proof is similar as in the previous case, with
an additional initial application of axiom P1 in Table 3.

  5. (5)

Case $|I|,|J|>1$. In this case there exist $i_{0},i_{1}\in I$ with $i_{0}\neq
i_{1}$ and $j_{0},j_{1}\in J$ with $j_{0}\neq j_{1}$. The proof follows the
same reasoning used in the case ${|I|}=1$ and ${|J|}>1$; we distinguish three
cases:

     * •

There are $i_{0},i_{1}\in I$ such that $i_{0}\neq i_{1}$ and
$a_{i_{0}}=a_{i_{1}}$.

In this case we have that

$p\mathbin{\|}q\stackrel{{\scriptstyle\text{(FP)}}}{{\approx}}\left(\sum_{i\in
I\mathbin{\backslash}{\\{i_{0}\\}}}a_{i}p_{i}\right)\mathbin{\|}q+\left(\sum_{i\in
I\mathbin{\backslash}{\\{i_{1}\\}}}a_{i}p_{i}\right)\mathbin{\|}q\enspace.$

As both $\sum_{i\in I\mathbin{\backslash}{\\{i_{0}\\}}}a_{i}p_{i}$ and
$\sum_{i\in I\mathbin{\backslash}{\\{i_{1}\\}}}a_{i}p_{i}$ have fewer operator
symbols than $p$, by the inductive hypothesis we get that there are closed
BCSSP terms $r_{i_{0}}$ and $r_{i_{1}}$ such that

$\mathcal{E}_{\mathtt{RT}}\vdash\left(\sum_{i\in
I\mathbin{\backslash}{\\{i_{0}\\}}}a_{i}p_{i}\right)\mathbin{\|}q\approx
r_{i_{0}}\quad\text{ and }\quad\mathcal{E}_{\mathtt{RT}}\vdash\left(\sum_{i\in
I\mathbin{\backslash}{\\{i_{1}\\}}}a_{i}p_{i}\right)\mathbin{\|}q\approx
r_{i_{1}}\enspace.$

Consequently, we get that $\mathcal{E}_{\mathtt{RT}}\vdash
p\mathbin{\|}q\approx r_{i_{0}}+r_{i_{1}}$, where $r_{i_{0}}+r_{i_{1}}$ is a
closed BCCSP term.

     * •

There are some $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$ and
$b_{j_{0}}=b_{j_{1}}$.

This case can be obtained from the previous one, by an additional initial
application of axiom P1 in Table 3.

     * •

For all $i_{0},i_{1}\in I$ such that $i_{0}\neq i_{1}$ we have that
$a_{i_{0}}\neq a_{i_{1}}$ and for all $j_{0},j_{1}\in J$ such that $j_{0}\neq
j_{1}$ we have that $b_{j_{0}}\neq b_{j_{1}}$.

In this case we have that

$p\mathbin{\|}q\stackrel{{\scriptstyle\text{(EL2)}}}{{\approx}}\sum_{i\in
I}a_{i}(p_{i}\mathbin{\|}q)+\sum_{j\in J}b_{j}(p\mathbin{\|}q_{j})\enspace.$

Since for each $i\in I$, the term $p_{i}$ has fewer operator symbols than $p$,
by the inductive hypothesis we get that there is a closed BCCSP term $r_{i}$
such that

$\mathcal{E}_{\mathtt{RT}}\vdash p_{i}\mathbin{\|}q\approx r_{i}\enspace.$

Similarly, for each $j\in J$, the term $q_{j}$ has fewer operator symbols than
$q$, so that by the inductive hypothesis we get that there is a closed BCCSP
term $r_{j}$ such that

$\mathcal{E}_{\mathtt{RT}}\vdash p\mathbin{\|}q_{j}\approx r_{j}\enspace.$

Therefore, we can conclude that $\mathcal{E}_{\mathtt{RT}}\vdash
p\mathbin{\|}q\approx\sum_{i\in I}a_{i}r_{i}+\sum_{j\in J}b_{j}r_{j}$, where
the right hand side of the equation is a closed BCCSP term.

######  Proposition 13 ($\mathcal{E}_{\mathtt{RT}}$ elimination).

For every closed $\mathrm{BCCSP}_{\scriptsize\|}$ term $p$ there is a closed
_BCCSP_ term $q$ such that $\mathcal{E}_{\mathtt{RT}}\vdash p\approx q$.

######  Proof 5.2.

The proof follows by an easy induction on the structure of $p$, using Lemma 12
in the case that $p$ is of the form $p_{1}\mathbin{\|}p_{2}$ for some $p_{1}$
and $p_{2}$.

######  Remark 14.

Similarly to the case of completed simulation (cf. Remark 10), the reason why
we propose to prove directly the elimination result for ready trace
equivalence is that axiom RSP2 cannot be derived from those in
$\mathcal{E}_{\mathtt{RT}}$, even though all its closed instantiations can be
derived. Table 9 presents a model, found using Mace4, of
$\mathcal{E}_{\mathtt{RT}}$ from which RSP2 is not derivable: e.g., it does
not satisfy

$ax\mathbin{\|}(ay+az+w)=a(x\mathbin{\|}(ay+az+w))+ax\mathbin{\|}(ay+w)+ax\mathbin{\|}(az+w))$

for $x=0$, $y=0$, $z=0$ and $w=1$.

a: | 0 | 1 | 2
---|---|---|---
| 0 | 2 | 2

b: | 0 | 1 | 2
---|---|---|---
| 0 | 0 | 0

$\mathbin{\|}$: | 0 | 1 | 2
---|---|---|---
0 | 0 | 1 | 2
1 | 1 | 0 | 1
2 | 2 | 1 | 2

$+$: | 0 | 1 | 2
---|---|---|---
0 | 0 | 1 | 2
1 | 1 | 1 | 2
2 | 2 | 2 | 2

Table 9.  A model for $\mathcal{E}_{\mathtt{RT}}$ and
$\mathcal{E}_{\mathtt{CT}}$.

We refer the interested reader to Appendix B for the Mace4 code.

Interestingly, axiom FP also characterises the distributivity of
$\mathbin{\|}$ over $+$ modulo $\sim_{\mathtt{FT}},\sim_{\mathtt{R}}$ and
$\sim_{\mathtt{F}}$. Consider the axiom systems
$\mathcal{E}_{\mathtt{FT}}=\mathcal{E}_{1}\cup\\{\textrm{FT,RS,FP,EL2}\\}$,
$\mathcal{E}_{\mathtt{R}}=\mathcal{E}_{1}\cup\\{\textrm{R,FP,EL2}\\}$ and
$\mathcal{E}_{\mathtt{F}}=\mathcal{E}_{1}\cup\\{\textrm{F,R,FP,EL2}\\}$. The
following derivability relations among them and $\mathcal{E}_{\mathtt{RT}}$
are then easy to check.

######  Lemma 15.

  1. (1)

The axioms in the system $\mathcal{E}_{\mathtt{RT}}$ are derivable from
$\mathcal{E}_{\mathtt{FT}}$, namely $\mathcal{E}_{\mathtt{FT}}\vdash$ _RT_.

  2. (2)

The axioms in the system $\mathcal{E}_{\mathtt{RT}}$ are derivable from
$\mathcal{E}_{\mathtt{R}}$, namely $\mathcal{E}_{\mathtt{R}}\vdash$ _RT_.

  3. (3)

The axioms in the system $\mathcal{E}_{\mathtt{FT}}$ are derivable from
$\mathcal{E}_{\mathtt{F}}$, namely,

    1. (a)

$\mathcal{E}_{\mathtt{F}}\vdash$ _FT_ , and

    2. (b)

$\mathcal{E}_{\mathtt{F}}\vdash$ _RS_.

Moreover, also the axioms in the system $\mathcal{E}_{\mathtt{R}}$ are
derivable from $\mathcal{E}_{\mathtt{F}}$.

######  Proof 5.3.

  1. (1)

To simplify notation, we introduce some abbreviations: let $|\mathcal{A}|=n$,
and for each $i\in\\{1,\dots,n\\}$ let
$I_{i}=\\{1,\dots,n\\}\mathbin{\backslash}{\\{i\\}}$.

First of all, we notice that if we can prove that

$\displaystyle\mathcal{E}_{\mathtt{FT}}\vdash{}$ $\displaystyle
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+z\right)\approx
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+z\right)+$
$\displaystyle\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad+a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)$
(1) $\displaystyle\mathcal{E}_{\mathtt{FT}}\vdash{}$ $\displaystyle
a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)\approx
a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)+a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)\enspace,$
(2)

then $\mathcal{E}_{\mathtt{FT}}\vdash$ RT, easily follows as

$\displaystyle
a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)$
$\displaystyle\stackrel{{\scriptstyle\eqref{axiom:eft2}}}{{\approx{}}}\qquad$
$\displaystyle
a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)+a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1),(A3)},\eqref{axiom:eft2}}}{{\approx{}}}$
$\displaystyle
a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)+a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+z\right)$
$\displaystyle\stackrel{{\scriptstyle(A1),\eqref{axiom:eft1}}}{{\approx{}}}\quad$
$\displaystyle
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+z\right)\enspace.$

We now proceed to prove the Equations (1) and (2) separately.

    1. (a)

Equation (1) directly follows by

$\displaystyle
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+z\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(FT)}}}{{\approx{}}}\quad$
$\displaystyle
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+z\right)+a\left(\Big{(}\sum_{i=1}^{n}b_{i}x_{i}+z\Big{)}+\Big{(}\sum_{i=1}^{n}b_{i}y_{i}+z\Big{)}\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1),(A2)}}}{{\approx{}}}$
$\displaystyle
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+z\right)+a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)\enspace.$

    2. (b)

Before proceeding to the proof of Equation (2), we notice that

$\displaystyle
a(bx+by+z)\stackrel{{\scriptstyle\textrm{(RS)}}}{{\approx{}}}\quad$
$\displaystyle a(bx+by+z)+a(bx+z)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1),(RS)}}}{{\approx{}}}$
$\displaystyle a(bx+by+z)+a(bx+z)+a(by+z)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(FT),(A3)}}}{{\approx{}}}$
$\displaystyle a(bx+z)+a(by+z)\enspace,$

so that

$\mathcal{E}_{\mathtt{FT}}\vdash a(bx+by+z)\approx a(bx+z)+a(by+z)\enspace.$
(3)

Using Equation (3), we can establish Equation (2) holds for all $n\geq 1$ with
induction on $n$.

If $n=1$, then

$\displaystyle a\left(\sum_{i=1}^{n}(b_{i}x_{i}+b_{i}y_{i})+z\right)$
$\displaystyle\stackrel{{\scriptstyle\eqref{axiom:eft3}}}{{\approx}}$
$\displaystyle a(b_{1}x_{1}+z)+a(b_{1}y_{1}+z)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1),(A2),(A3)}}}{{\approx{}}}$
$\displaystyle a(b_{1}x_{1}+z)+a(b_{1}y_{1}+z)+a(b_{1}x_{1}+z)$
$\displaystyle\stackrel{{\scriptstyle\eqref{axiom:eft3}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{n}(b_{i}x_{i}+b_{i}y_{i})+z\right)+a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)$

Let $n\geq 1$, and suppose that Equation (2) holds (IH). Then

$\displaystyle
a\left(\sum_{i=1}^{n+1}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)},\eqref{axiom:eft3}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+b_{n+1}x_{n+1}+z\right)+a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+b_{n+1}y_{n+1}+z\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(IH)}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+b_{n+1}x_{n+1}+z\right)+a\left(\sum_{i=1}^{n}b_{i}x_{i}+b_{n+1}x_{n+1}+z\right)$
$\displaystyle\qquad\qquad\mbox{}+a\left(\sum_{i=1}^{n}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+b_{n+1}y_{n+1}+z\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)},\eqref{axiom:eft3}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{n+1}\big{(}b_{i}x_{i}+b_{i}y_{i}\big{)}+z\right)+a\left(\sum_{i=1}^{n+1}b_{i}x_{i}+z\right)$

We conclude that Equation (1) holds for all $n\geq 1$, and hence, in
particular, for $n=|\mathcal{A}|$.

  2. (2)

To prove that $\mathcal{E}_{\mathtt{R}}\vdash\textrm{RT}$, we first establish
that for every $n\geq 1$ we have:

$\mathcal{E}_{\mathtt{R}}\vdash
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+w\right)\\\
\approx
a\left(\sum_{i=1}^{n}(b_{i}x_{i}+b_{i}y_{i})+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+w\right)\enskip.$
(4)

We proceed by induction on $n\geq 1$.

If $n=1$, then

$\displaystyle
a\left(\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+w\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(R)}}}{{\approx}}$ $\displaystyle
a\left(\sum_{i=1}^{n}(b_{i}x_{i}+b_{i}y_{i})+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+w\right)$

Let $n\geq 1$, and suppose that Equation (4) holds (IH). Then

$\displaystyle
a\left(\sum_{i=1}^{n+1}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{n+1}b_{i}y_{i}+w\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)}}}{{\approx}}$
$\displaystyle
a\left(b_{n+1}x_{n+1}+\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(b_{n+1}y_{n+1}+\sum_{i=1}^{n}b_{i}y_{i}+w\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(R)}}}{{\approx}}$ $\displaystyle
a\left(b_{n+1}x_{n+1}+b_{n+1}y_{n+1}+\sum_{i=1}^{n}b_{i}x_{i}+z\right)+a\left(b_{n+1}y_{n+1}+\sum_{i=1}^{n}b_{i}y_{i}+w\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{n}b_{i}x_{i}+b_{n+1}x_{n+1}+b_{n+1}y_{n+1}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+b_{n+1}y_{n+1}+w\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(IH)}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{n}(b_{i}x_{i}+b_{i}y_{i})+b_{n+1}x_{n+1}+b_{n+1}y_{n+1}+z\right)+a\left(\sum_{i=1}^{n}b_{i}y_{i}+b_{n+1}y_{n+1}+w\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{n+1}(b_{i}x_{i}+b_{i}y_{i})+z\right)+a\left(\sum_{i=1}^{n+1}b_{i}y_{i}+w\right)$

We conclude that Equation (4) holds for all $n\geq 1$.

We can now derive axiom (RT) as follows:

$\displaystyle
a\left(\sum_{i=1}^{|\mathcal{A}|}(b_{i}x_{i}+b_{i}y_{i})+z\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A3)}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{|\mathcal{A}|}(b_{i}x_{i}+b_{i}y_{i})+z\right)+\left(\sum_{i=1}^{|\mathcal{A}|}(b_{i}x_{i}+b_{i}y_{i})+z\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{|\mathcal{A}|}(b_{i}x_{i}+b_{i}y_{i})+z\right)+\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}x_{i}+\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}y_{i}+z\right)\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)},\eqref{axiom:eft4}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}y_{i}+z\right)+\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}x_{i}+\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}y_{i}+z\right)\right)$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A1)},\textrm{(A2)}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{|\mathcal{A}|}(b_{i}x_{i}+b_{i}y_{i})+z\right)+a\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}y_{i}+z\right)$
$\displaystyle\stackrel{{\scriptstyle\eqref{axiom:eft4}}}{{\approx}}$
$\displaystyle
a\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}x_{i}+z\right)+a\left(\sum_{i=1}^{|\mathcal{A}|}b_{i}y_{i}+z\right)\enskip.$

  3. (3)

The second claim, namely that the axioms in $\mathcal{E}_{\mathtt{R}}$ are
derivable from $\mathcal{E}_{\mathtt{F}}$, follows directly from
$\mathcal{E}_{\mathtt{R}}\subseteq\mathcal{E}_{\mathtt{F}}$.

To prove the first claim, we start by showing that the axiom FT in Table 8 is
derivable from the axiom system $\mathcal{E}_{\mathtt{F}}$.

$\displaystyle ax+ay\stackrel{{\scriptstyle\textrm{(A0)}}}{{\approx{}}}\quad$
$\displaystyle ax+a(y+\mathbf{0})$
$\displaystyle\stackrel{{\scriptstyle\textrm{(F)}}}{{\approx{}}}\quad$
$\displaystyle ax+a(x+y)+a(y+\mathbf{0})$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A0),(A1)}}}{{\approx{}}}$
$\displaystyle ax+ay+a(x+y)\enspace.$

We now proceed to prove that the axiom RS in Table 8 is derivable from the
axiom system $\mathcal{E}_{\mathtt{F}}$.

$\displaystyle
a(bx+by+z)+a(bx+z)\stackrel{{\scriptstyle\textrm{(A1),(A2)}}}{{\approx{}}}$
$\displaystyle a(bx+z)+a(by+(bx+z))$
$\displaystyle\stackrel{{\scriptstyle\textrm{(R)}}}{{\approx{}}}\quad$
$\displaystyle a(bx+by+z)+a(by+(bx+z))$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A2),(A3)}}}{{\approx{}}}$
$\displaystyle a(bx+by+z)\enspace.$

The next proposition is then a corollary of Proposition 13 and Lemma 15.

######  Proposition 16 ($\mathcal{E}_{\mathtt{FT}}$,
$\mathcal{E}_{\mathtt{R}}$, $\mathcal{E}_{\mathtt{F}}$ elimination).

Let $\mathtt{X}\in\\{\mathtt{FT},\mathtt{R},\mathtt{F}\\}$. For every
$\mathrm{BCCSP}_{\scriptsize\|}$ term $p$ there is a closed _BCCSP_ term $q$
such that $\mathcal{E}_{\mathtt{X}}\vdash p\approx q$.

In [8] it was proved that, under the assumption that $\mathcal{A}$ is finite,
the axiom system $\mathcal{E}_{0}\cup\\{\textrm{RT}\\}$ is a ground-complete
axiomatisation of BCCSP modulo $\sim_{\mathtt{RT}}$. Moreover, it was also
proved that $\mathcal{E}_{0}\cup\\{\textrm{FT,RS}\\}$ is a ground-complete
axiomatisation of BCCSP modulo $\sim_{\mathtt{FT}}$. The ground-completeness
of $\mathcal{E}_{0}\cup\\{\mathrm{R}\\}$, modulo $\sim_{\mathtt{R}}$, and that
of $\mathcal{E}_{0}\cup\\{\mathrm{F,R}\\}$, modulo $\sim_{\mathtt{F}}$, over
BCCSP were proved in [19]. Consequently, the soundness and ground-completeness
of the proposed axioms systems can then be derived from the elimination
results above and the completeness results given in [19, 8].

######  Theorem 17 (Soundness and completeness of $\mathcal{E}_{\mathtt{RT}}$,
$\mathcal{E}_{\mathtt{FT}}$, $\mathcal{E}_{\mathtt{R}}$ and
$\mathcal{E}_{\mathtt{F}}$).

Let $\mathtt{X}\in\\{\mathtt{RT},\mathtt{FT},\mathtt{R},\mathtt{F}\\}$. The
axiom system $\mathcal{E}_{\mathtt{X}}$ is a sound, ground-complete
axiomatisation of $\mathrm{BCCSP}_{\scriptsize\|}$ modulo $\sim_{\mathtt{X}}$,
i.e., $p\sim_{\mathtt{X}}q$ if and only if $\mathcal{E}_{\mathtt{X}}\vdash
p\approx q$.

###  5.2. Completed traces and traces

It remains to consider completed trace equivalence and trace equivalence.

[Trace and completed trace equivalences] Two processes $p$ and $q$ are _trace
equivalent_ , denoted $p\sim_{\mathtt{T}}q$, if $\mathtt{T}(p)=\mathtt{T}(q)$.
If, in addition, it holds that $\mathtt{CT}(p)=\mathtt{CT}(q)$, then $p$ and
$q$ are _completed trace equivalent_ , denoted $p\sim_{\mathtt{CT}}q$.

######  Remark 18.

Since we are considering only $\mathrm{BCCSP}_{\scriptsize\|}$ processes with
finite traces, then to prove completed trace equivalence it is enough to check
whether two processes have the same sets of completed traces. In fact, in our
setting, $\mathtt{CT}(p)=\mathtt{CT}(q)$ implies $\mathtt{T}(p)=\mathtt{T}(q)$
for all processes $p,q$.

(CT) $a(bx+z)+a(cy+w)\approx a(bx+cy+z+w)$
---
(CTP) $(ax+by+w)\mathbin{\|}z\approx(ax+w)\mathbin{\|}z+(by+w)\mathbin{\|}z$
$\mathcal{E}_{\mathtt{CT}}=\mathcal{E}_{1}\cup\\{\textrm{CT, CTP, EL1}\\}$
(T) $ax+ay\approx a(x+y)$
(TP) $(x+y)\mathbin{\|}z\approx x\mathbin{\|}z+y\mathbin{\|}z$
$\mathcal{E}_{\mathtt{T}}=\mathcal{E}_{1}\cup\\{\textrm{T, TP, EL1}\\}$
Table 10. Additional axioms for completed trace and trace equivalences.

Consider the axiom systems
$\mathcal{E}_{\mathtt{CT}}=\mathcal{E}_{1}\cup\\{\textrm{CT,CTP,EL1}\\}$ and
$\mathcal{E}_{\mathtt{T}}=\mathcal{E}_{1}\cup\\{\textrm{T,TP,EL1}\\}$,
presented in Table 10. In the same way that axiom FP is the linear counterpart
of RSP1 and RSP2, we have that CTP is the linear counterpart of CSP1 and CSP2,
and TP is that of SP1 and SP2. It is then easy to check that we can use the
axioms in $\mathcal{E}_{\mathtt{CT}}$ to obtain the elimination result for
$\sim_{\mathtt{CT}}$.

######  Lemma 19.

For every closed _BCCSP_ terms $p,q$ there is a closed _BCCSP_ term $r$ such
that $\mathcal{E}_{\mathtt{CT}}\vdash p\mathbin{\|}q\approx r$.

######  Proof 5.4.

The proof proceeds by induction on the total number of operator symbols
occurring in $p$ and $q$ together, not counting parentheses. Since $p$ and $q$
are closed BCCSP terms, we can assume that $p=\sum_{i\in I}a_{i}p_{i}$ and
$q=\sum_{j\in J}b_{j}q_{j}$ (see Remark 2).

We proceed by a case analysis according to the cardinalities of the sets $I$
and $J$.

  1. (1)

Case ${|I|}=0$ or ${|J|}=0$. In case that ${|J|}=0$, i.e., $J=\emptyset$, then
$q=\mathbf{0}$, so $\mathcal{E}_{\mathtt{CT}}\vdash p\mathbin{\|}q\approx p$
by P0, and $p$ is the required closed BCCSP term. Similarly, if ${|I|}=0$,
i.e., $I=\emptyset$, then $p=\mathbf{0}$, so $\mathcal{E}_{\mathtt{CT}}\vdash
p\mathbin{\|}q\approx q\mathbin{\|}p\approx q$ by P0 and P1, and $q$ is the
required closed BCCSP term.

  2. (2)

Case ${|I|}={|J|}=1$. Let $I=\\{i_{0}\\}$ and $J=\\{j_{0}\\}$, then

$p\mathbin{\|}q\stackrel{{\scriptstyle\text{(EL1)}}}{{\approx}}a_{i_{0}}(p_{i_{0}}\mathbin{\|}q)+b_{j_{0}}(p\mathbin{\|}q_{j_{0}})\enspace.$

Since both $p_{i_{0}}$ and $q_{j_{0}}$ have fewer symbols than $p$ and $q$,
respectively, by the inductive hypothesis there exist closed BCCSP terms
$r_{i_{0}}$ and $r_{j_{0}}$ such that $\mathcal{E}_{\mathtt{CT}}\vdash
p_{i_{0}}\mathbin{\|}q\approx r_{i_{0}}$ and $\mathcal{E}_{\mathtt{CT}}\vdash
p\mathbin{\|}q_{j_{0}}\approx r_{j_{0}}$. It follows that
$\mathcal{E}_{\mathtt{CT}}\vdash p\mathbin{\|}q\approx
a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$, where
$a_{i_{0}}r_{i_{0}}+b_{j_{0}}r_{j_{0}}$ is a closed BCCSP term.

  3. (3)

Case ${|I|}=1$ and $|J|>1$. We can then assume that $I=\\{i_{0}\\}$ and there
exist $j_{0},j_{1}\in J$ such that $j_{0}\neq j_{1}$, then

$\displaystyle
p\mathbin{\|}q\stackrel{{\scriptstyle\textrm{(A2),(P1)}}}{{\approx{}}}$
$\displaystyle\left(b_{j_{0}}q_{j_{0}}+b_{j_{1}}q_{j_{1}}+\sum_{j\in
J\mathbin{\backslash}{\\{j_{0},j_{1}\\}}}b_{j}q_{j}\right)\mathbin{\|}p$
$\displaystyle\stackrel{{\scriptstyle\textrm{(CTP)}}}{{\approx{}}}$
$\displaystyle\left(b_{j_{0}}q_{j_{0}}+\sum_{j\in{J\mathbin{\backslash}{\\{j_{0},j_{1}\\}}}}b_{j}q_{j}\right)\mathbin{\|}p+\left(b_{j_{1}}q_{j_{1}}+\sum_{j\in{J\mathbin{\backslash}{\\{j_{0},j_{1}\\}}}}b_{j}q_{j}\right)\mathbin{\|}p$
$\displaystyle\stackrel{{\scriptstyle\textrm{(A2),(P1)}}}{{\approx{}}}$
$\displaystyle\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{1}\\}}}}b_{j}q_{j}\right)\mathbin{\|}p+\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{0}\\}}}}b_{j}q_{j}\right)\mathbin{\|}p\enskip.$

Since $\sum_{j\in{J\mathbin{\backslash}{\\{j_{0}\\}}}}b_{j}q_{j}$ and
$\sum_{j\in{J\mathbin{\backslash}{\\{j_{1}\\}}}}b_{j}q_{j}$ have fewer symbols
than $q$, by the inductive hypothesis there exist closed BCCSP terms
$r_{j_{0}}$ and $r_{j_{1}}$ such that

$\displaystyle\mathcal{E}_{\mathtt{CT}}\vdash
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{0}\\}}}}b_{j}q_{j}\right)\approx
r_{j_{0}}$ $\displaystyle\mathcal{E}_{\mathtt{CT}}\vdash
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}{\\{j_{1}\\}}}}b_{j}q_{j}\right)\approx
r_{j_{0}}\enspace.$

So we have $\mathcal{E}_{\mathtt{CT}}\vdash p\mathbin{\|}q\approx
r_{j_{0}}+r_{j_{1}}$ and $r_{j_{0}}+r_{j_{1}}$ is a closed BCCSP term.

  4. (4)

Case $|I|>1$ and ${|J|}=1$. This case can be obtained as the previous one,
without the initial application of axiom P1.

  5. (5)

Case $|I|,|J|>1$. In this case there exist $i_{0},i_{1}\in I$ with $i_{0}\neq
i_{1}$ and $j_{0},j_{1}\in J$ with $j_{0}\neq j_{1}$. Then

$\displaystyle
p\mathbin{\|}q\stackrel{{\scriptstyle\text{(A2),(P1),(CTP)}}}{{\approx}}$
$\displaystyle\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{0}\\}}}a_{i}p_{i}\right)\mathbin{\|}q+\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{1}\\}}}a_{i}p_{i}\right)\mathbin{\|}q+$
$\displaystyle+p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{0}\\}}}b_{j}q_{j}\right)+p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{1}\\}}}b_{j}q_{i}\right)\enskip.$

Note that $\sum_{i\in{I\mathbin{\backslash}\\{i_{0}\\}}}a_{i}p_{i}$ and
$\sum_{i\in{I\mathbin{\backslash}\\{i_{1}\\}}}a_{i}p_{i}$ have fewer symbols
than $p$, and $\sum_{j\in{J\mathbin{\backslash}\\{j_{0}\\}}}b_{j}q_{j}$ and
$\sum_{j\in{J\mathbin{\backslash}\\{j_{1}\\}}}b_{j}q_{i}$ have fewer symbols
than $q$, so by the inductive hypothesis there exist $r_{i_{0}}$, $r_{i_{1}}$,
$r_{j_{0}}$ and $r_{j_{1}}$ such that

$\displaystyle\mathcal{E}_{\mathtt{CT}}\vdash\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{0}\\}}}a_{i}p_{i}\right)\mathbin{\|}q\approx
r_{i_{0}}$
$\displaystyle\mathcal{E}_{\mathtt{CT}}\vdash\left(\sum_{i\in{I\mathbin{\backslash}\\{i_{1}\\}}}a_{i}p_{i}\right)\mathbin{\|}q\approx
r_{i_{1}}$ $\displaystyle\mathcal{E}_{\mathtt{CT}}\vdash
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{0}\\}}}b_{j}q_{j}\right)\approx
r_{j_{0}}$ $\displaystyle\mathcal{E}_{\mathtt{CT}}\vdash
p\mathbin{\|}\left(\sum_{j\in{J\mathbin{\backslash}\\{j_{1}\\}}}b_{j}q_{i}\right)\approx
r_{j_{1}}\enspace.$

Then $\mathcal{E}_{\mathtt{CT}}\vdash p\mathbin{\|}q\approx
r_{i_{0}}+r_{i_{1}}+r_{j_{0}}+r_{j_{1}}$ and
$r_{i_{0}}+r_{i_{1}}+r_{j_{0}}+r_{j_{1}}$ is a closed BCCSP term.

######  Proposition 20 ($\mathcal{E}_{\mathtt{CT}}$ elimination).

For every closed $\mathrm{BCCSP}_{\scriptsize\|}$ term $p$ there is a closed
BCCSP term $q$ such that $\mathcal{E}_{\mathtt{CT}}\vdash p\approx q$.

######  Proof 5.5.

The proof follows by an easy induction on $p$, using Lemma 19 in the case that
$p$ is of the form $p_{1}\mathbin{\|}p_{2}$ for some $p_{1}$ and $p_{2}$.

Moreover, the elimination for $\sim_{\mathtt{T}}$ follows from the fact that
the axioms in $\mathcal{E}_{\mathtt{CT}}$ are derivable from those in
$\mathcal{E}_{\mathtt{T}}$.

######  Lemma 21.

The axioms in the system $\mathcal{E}_{\mathtt{CT}}$ are derivable from
$\mathcal{E}_{\mathtt{T}}$, namely,

  1. (1)

$\mathcal{E}_{\mathtt{T}}\vdash\mathrm{CT}$, and

  2. (2)

$\mathcal{E}_{\mathtt{T}}\vdash\mathrm{CTP}$.

######  Proof 5.6.

In the case of CT, we have the following equational derivation:

$a(bx+z)+a(cy+w)\stackrel{{\scriptstyle\mathrm{(T)}}}{{\approx}}a(bx+z+cy+w)\enskip.$

For CTP, we have the following equational derivation:

$(ax+by+w)\mathbin{\|}z\stackrel{{\scriptstyle\mathrm{(A1),(A3)}}}{{\approx}}(ax+w+by+w)\mathbin{\|}z\stackrel{{\scriptstyle\mathrm{(TP)}}}{{\approx}}(ax+w)\mathbin{\|}z+(by+w)\mathbin{\|}z\enskip.$

######  Proposition 22 ($\mathcal{E}_{\mathtt{T}}$ elimination).

For every closed $\mathrm{BCCSP}_{\scriptsize\|}{}$ term $p$ there exists a
closed _BCCSP_ term $q$ such that $\mathcal{E}_{\mathtt{T}}\vdash p\approx q$.

######  Remark 23.

We can use the models in Tables 7 and 9 to prove that, respectively, neither
axiom EL2 nor axiom CSP2 are derivable from $\mathcal{E}_{\mathtt{CT}}$. In
detail, in the case of EL2 the counterexample presented in Remark 10 holds
also in the case of $\mathcal{E}_{\mathtt{CT}}$. In the case of CSP2, we
notice that the instance of RSP2 used in Remark 14 is in fact also an instance
of CSP2, and thus the counterexample for RSP2 holds also in this case. We
refer the interested reader to Appendix C for the Mace4 codes generating the
desired models.

In light of Proposition 20, the ground-completeness of
$\mathcal{E}_{\mathtt{CT}}$ over $\mathrm{BCCSP}_{\scriptsize\|}$ modulo
$\sim_{\mathtt{CT}}$ follows from that of
$\mathcal{E}_{0}\cup\\{\mathrm{CT}\\}$ over BCCSP provided in [19]. Similarly,
the ground-completeness of $\mathcal{E}_{0}\cup\\{\mathrm{T}\\}$ over BCCSP
proved in [19] and Proposition 22 give us the ground-completeness of
$\mathcal{E}_{\mathtt{T}}$ over $\mathrm{BCCSP}_{\scriptsize\|}$.

######  Theorem 24 (Soundness and completeness of $\mathcal{E}_{\mathtt{CT}}$
and $\mathcal{E}_{\mathtt{T}}$).

Let $\mathtt{X}\in\\{\mathtt{CT},\mathtt{T}\\}$. The axiom system
$\mathcal{E}_{\mathtt{X}}$ is a ground-complete axiomatisation of
$\mathrm{BCCSP}_{\scriptsize\|}$ modulo $\sim_{\mathtt{X}}$, i.e.,
$p\sim_{\mathtt{X}}q$ if and only if $\mathcal{E}_{\mathtt{X}}\vdash p\approx
q$.

##  6\. The negative results

We dedicate this section to the negative results: we prove that all the
congruences between possible futures equivalence ($\sim_{\mathtt{PF}}$) and
bisimilarity ($\sim_{\mathtt{B}}$) do not admit a finite, ground-complete
axiomatisation over $\mathrm{BCCSP}_{\scriptsize\|}$. This includes all the
nested trace and nested simulation equivalences. In [2] it was shown that,
even if the set of actions is a singleton, the nested semantics admit no
finite axiomatisation over BCCSP. Indeed, the presence of the additional
operator $\mathbin{\|}$ might, at least in principle, allow us to finitely
axiomatise the equations over closed BCCSP terms that are valid modulo the
considered equivalences. Hence, we prove these results directly.

In detail, firstly we focus on the negative result for possible futures
semantics, corresponding to the $2$-nested trace semantics [22]. To obtain it,
we apply the general technique used by Moller to prove that interleaving is
not finitely axiomatisable modulo bisimilarity [27, 28, 29]. Briefly, the main
idea is to identify a _witness property_. This is a specific property of
$\mathrm{BCCSP}_{\scriptsize\|}$ terms, say $W_{N}$ for $N\geq 0$, that, when
$N$ is _large enough_ , is an invariant that is preserved by provability from
finite, sound axiom systems. Roughly, this means that if $\mathcal{E}$ is a
finite set of axioms that are sound modulo possible futures equivalence, the
equation $p\approx q$ can be derived from $\mathcal{E}$, and $N$ is larger
than the size of all the terms in the equations in $\mathcal{E}$, then either
both $p$ and $q$ satisfy $W_{N}$, or none of them does. Then, we exhibit an
infinite family of valid equations, called the _witness family of equations_ ,
in which $W_{N}$ is not preserved, namely it is satisfied only by one side of
each equation.

Afterwards, we exploit the soundness modulo bisimilarity of the equations in
the witness family to lift the negative result for $\sim_{\mathtt{PF}}$ to all
congruences between $\sim_{\mathtt{B}}$ and $\sim_{\mathtt{PF}}$.

Differently from the aforementioned negative results over BCCSP, ours are
obtained assuming that the set of actions contains at least two distinct
elements. In fact, when the action set is a singleton, and _only_ in that
case, the axiom

$ax\mathbin{\|}(ay+az)\approx
ax\mathbin{\|}(ay+a(y+z))+ax\mathbin{\|}(az+a(y+z))$

is sound modulo $\sim_{\mathtt{PF}}$. Due to this axiom we were not able to
prove the negative result for $\sim_{\mathtt{PF}}$ in the case that
$|\mathcal{A}|=1$, which we leave as an open problem for future work.

###  6.1. Possible futures equivalence

According to possible futures equivalence [32] two processes are deemed
equivalent if, by performing the same traces, they reach processes that are
trace equivalent. For this reason, possible futures equivalence is also known
as the $2$-_nested trace equivalence_ [22].

[Possible futures equivalence] A _possible future_ of a process $p$ is a pair
$(\alpha,X)$ where $\alpha\in\mathcal{A}^{*}$ and $X\subseteq\mathcal{A}^{*}$
such that $p\xrightarrow{\,{\alpha}\,}p^{\prime}$ for some $p^{\prime}$ with
$X=\mathtt{T}(p^{\prime})$. We write $\mathtt{PF}(p)$ for the set of possible
futures of $p$. Two processes $p$ and $q$ are said to be _possible futures
equivalent_ , denoted $p\sim_{\mathtt{PF}}q$, if
$\mathtt{PF}(p)=\mathtt{PF}(q)$.

Our order of business is to prove the following result.

######  Theorem 25.

Assume that ${|\mathcal{A}|}\geq 2$. Possible futures equivalence has no
finite, ground-complete, equational axiomatisation over the language
$\mathrm{BCCSP}_{\scriptsize\|}$.

In what follows, for actions $a,b\in\mathcal{A}$ and $i\geq 0$, we let
$b^{0}a$ denote $a.0$ and $b^{i+1}a$ stand for $b(b^{i}a)$. Consider now the
infinite family of equations $\\{e_{N}\mid N\geq 1\\}$ given, for $a\neq b$,
by:

$\displaystyle p_{N}=\sum_{i=1}^{N}b^{i}a$ $\displaystyle(N\geq
1)\enspace\phantom{.}$ $\displaystyle e_{N}\;\colon\;a\mathbin{\|}p_{N}\approx
ap_{N}+\sum_{i=1}^{N}b(a\mathbin{\|}b^{i-1}a)$ $\displaystyle(N\geq
1)\enspace.$

Notice that the equations $e_{N}$ are sound modulo $\sim_{\mathtt{PF}}$ for
all $N\geq 1$.

We also notice that none of the summands in the right-hand side of equation
$e_{N}$ is, alone, possible futures equivalent to $a\mathbin{\|}p_{N}$.
However, we now proceed to show that, when $N$ is large enough, having a
summand possible futures equivalent to $a\mathbin{\|}p_{N}$ is an invariant
under provability from finite sound axiom systems, and it will thus play the
role of witness property for our negative result.

To this end, we introduce first some basic notions and results on
$\sim_{\mathtt{PF}}$.

Firstly, as a simplification, we can focus on the $\mathbf{0}$ _absorption
properties_ of $\mathrm{BCCSP}_{\scriptsize\|}$. Informally, we can restrict
the axiom system to a collection of equations that do not introduce
unnecessary terms that are possible futures equivalent to $\mathbf{0}$ in the
equational proofs, namely $\mathbf{0}$ summands and $\mathbf{0}$ _factors_.
(We refer the interested reader to Appendix D for further details.)

We say that a $\mathrm{BCCSP}_{\scriptsize\|}$ term $t$ has a $\mathbf{0}$
factor if it contains a subterm of the form $t_{1}\mathbin{\|}t_{2}$, where
either $t_{1}$ or $t_{2}$ is possible futures equivalent to $\mathbf{0}$.

Next, we characterise closed $\mathrm{BCCSP}_{\scriptsize\|}$ terms that are
possible futures equivalent to $p_{N}$.

######  Lemma 26.

Let $q$ be a $\mathrm{BCCSP}_{\scriptsize\|}$ term that does not have
$\mathbf{0}$ summands or factors and such that
$\mathtt{CT}(q)=\mathtt{CT}(p_{N})$ for some $N\geq 1$. Then $q$ does not
contain any occurrence of $\mathbin{\|}$.

######  Proof 6.1.

That $q\sim_{\mathtt{CT}}p_{N}$ implies that $q$ does not contain any
occurrence of $\mathbin{\|}$ directly follows by observing that the completed
traces of $p_{N}$, and thus those of $q$, contain exactly one occurrence of
$a$, and this occurrence must be as the last action in the completed trace.

######  Lemma 27.

Let $q$ be a $\mathrm{BCCSP}_{\scriptsize\|}$ term that does not have
$\mathbf{0}$ summands or factors. Then $q\sim_{\mathtt{PF}}p_{N}$, for some
$N\geq 1$, if and only if $q=\sum_{j\in J}q_{j}$ for some terms $q_{j}$ such
that none of them has $+$ as head operator and:

  * •

for each $i\in\\{1,\dots,N\\}$ there is some $j\in J$ such that
$b^{i}a\sim_{\mathtt{PF}}q_{j}$;

  * •

for each $j\in J$ there is some $i\in\\{1,\dots,N\\}$ such that
$q_{j}\sim_{\mathtt{PF}}b^{i}a$.

######  Proof 6.2.

Due to a slight difference in the technical development of the proof, we treat
the case of $N=1$ separately.

  * •

Case $N>1$.

($\Rightarrow$) Let $q\sim_{\mathtt{PF}}p_{N}$.

First of all, we show that $q$ cannot be of the form $q=b.q^{\prime}$ for some
term $q^{\prime}$. In fact, in that case, since $N>1$, we have that
$p_{N}\xrightarrow{\,{b}\,}a$ and $p_{N}\xrightarrow{\,{b}\,}ba$. Therefore,
as $\mathtt{PF}(q)=\mathtt{PF}(p_{N})$, it follows that
$(b,\\{\varepsilon,a\\})=(b,\mathtt{T}(q^{\prime}))=(b,\\{\varepsilon,b,ba\\})$,
which is a contradiction.

We have therefore obtained that $q=\sum_{i\in J}q_{j}$ for some $J$ with
$|J|\geq 2$, and some $q_{j}$, $j\in J$ of the form $b.q_{j}^{\prime}$. Let
$i\in\\{1,\ldots,N\\}$. Since $p_{N}\xrightarrow{\,{b}\,}b^{i-1}a$, we have
that $(b,\mathtt{T}(b^{i-1}a))$ is a possible future of $p_{N}$. Since $q$ is
possible futures equivalent to $p_{N}$, there is some $j$ with
$\mathtt{T}(q^{\prime}_{j})=\mathtt{T}(b^{i-1}a)$. We claim that
$q^{\prime}_{j}$ is possible futures equivalent to $b^{i-1}a$, which yields
that $q_{j}=b.q^{\prime}_{j}$ is possible futures equivalent to $b^{i}a$. To
see this, assume, towards a contradiction, that
$\mathtt{T}(q^{\prime}_{j})=\mathtt{T}(b^{i-1}a)$ but $q_{j}^{\prime}$ is not
possible futures equivalent to $b^{i-1}a$. This means that there are some
$k\leq i-1$ and $q^{\prime}$ such that
$q^{\prime}_{j}\xrightarrow{\,{b^{k}}\,}q^{\prime}$ and
$\mathtt{T}(q^{\prime})$ is strictly included in $\mathtt{T}(b^{i-1-k}a)$.
Since $\mathtt{T}(q^{\prime})$ is prefix closed, this means that
$\mathtt{T}(q^{\prime})=\\{b^{h}\mid 0\leq h\leq\ell\\}$ for some $\ell\leq
i-1-k$. This means that $q$ has $(b^{k+1},\mathtt{T}(q^{\prime}))$ as one of
its possible futures. On the other hand, $p_{N}$ has no such possible future,
due to the missing trailing $a$, which contradicts our assumption that
$q\sim_{\mathtt{PF}}p_{N}$.

Assume now, towards a contradiction, that there is a $j\in J$ such that
$q_{j}\not\sim_{\mathtt{PF}}b^{i}a$ for all $i\in\\{1,\dots,N\\}$. As $q_{j}$
is of the form $b.q^{\prime}_{j}$, for some $q_{j}^{\prime}$, we get that
$q\xrightarrow{\,{b}\,}q_{j}^{\prime}$ and
$(b,\mathtt{T}(q_{j}^{\prime}))\in\mathtt{PF}(q)$. We can distinguish two
cases according to the form of $\mathtt{CT}(q_{j}^{\prime})$:

    * –

$\mathtt{CT}(q_{j}^{\prime})$ includes one completed trace of the form
$b^{k}a$ for some $k\in\\{0,\dots,N-1\\}$. Since $p_{N}$ is possible futures
equivalent to $q$, there is some $i\in\\{1,\dots,N\\}$ with
$\mathtt{T}(b^{i-1}a)=\mathtt{T}(q_{j}^{\prime})$. In this case, the same
reasoning applied above yields a contradiction with
$q\sim_{\mathtt{PF}}p_{N}$.

    * –

There are $b^{k}a,b^{h}a\in\mathtt{CT}(q_{j}^{\prime})$ for some $k\neq
h,k,h\in\\{0,\dots,N-1\\}$. Since there is no $p^{\prime}$ such that
$p_{N}\xrightarrow{\,{b}\,}p^{\prime}$ and
$\mathtt{CT}(p^{\prime})=\mathtt{CT}(q_{j}^{\prime})$, we get an immediate
contradiction with $q\sim_{\mathtt{PF}}p_{N}$.

($\Leftarrow$) Assume now that $q=\sum_{j\in J}q_{j}$, for some terms $q_{j}$
that do not have $+$ as head operator and such that

    1. (1)

for each $i\in\\{1,\dots,N\\}$ there is a $j\in J$ such that
$b^{i}a\sim_{\mathtt{PF}}q_{j}$, and

    2. (2)

for each $j\in J$ there is a $i\in\\{1,\dots,N\\}$ such that
$q_{j}\sim_{\mathtt{PF}}b^{i}a$.

Since possible futures equivalence is a congruence with respect to summation
and, moreover, summation is an idempotent operator (axiom A3 in Table 3), from
these assumptions we can directly conclude that $q\sim_{\mathtt{PF}}p_{N}$.

  * •

Case $N=1$.

($\Rightarrow$) Let $q\sim_{\mathtt{PF}}p_{1}$. Hence

$\mathtt{PF}(q)=\left\\{\Big{(}\varepsilon,\\{\varepsilon,b,ba\\}\Big{)},\Big{(}b,\\{\varepsilon,a\\}\Big{)},\Big{(}ba,\\{\varepsilon\\}\Big{)}\right\\}$

Assume that $q=b.q^{\prime}$ for some term $q^{\prime}$. Then
$(b,\mathtt{T}(q^{\prime}))\in\mathtt{PF}(q)$ implies
$\mathtt{T}(q^{\prime})=\\{\varepsilon,a\\}$, and hence
$q^{\prime}\sim_{\mathtt{PF}}a$. This gives $q=\sum_{j\in J}q_{j}$ for some
$J$ with $|J|=1$ and $q_{j}\sim_{\mathtt{PF}}ba$. The two properties relating
the summands of $q$ and $p_{1}$ are then immediate.

Assume now that $q=\sum_{j\in J}q_{j}$ for some $J$ with $|J|\geq 2$ and some
$q_{j}$ of the form $b.q_{j}^{\prime}$. Assume, towards a contradiction, that
there is some $q_{j}$ such that $q_{j}\not\sim_{\mathtt{PF}}ba$. Since
$q\sim_{\mathtt{PF}}p_{1}$ implies $\mathtt{T}(q)=\mathtt{T}(ba)$, we get that
$q_{j}$, and thus $q$, has $(b,\\{\varepsilon\\})$ as a possible future. This
gives an immediate contradiction with $q\sim_{\mathtt{PF}}p_{1}$.

($\Leftarrow$) The proof of this implication follows as in the case of $N>1$.

This concludes the proof.

In light of Lemma 27, we can also provide a decomposition-like
characterisation of closed $\mathrm{BCCSP}_{\scriptsize\|}$ terms that are
possible futures equivalent to $a\mathbin{\|}p_{N}$. To this end, we need
first to lift the notions of transition, norm and depth from closed terms to
terms. The action-labelled transition relation over
$\mathrm{BCCSP}_{\scriptsize\|}$ terms contains exactly the literals that can
derived using the rules in Table 1. clearly,
$t\xrightarrow{\,{a}\,}t^{\prime}$ implies
$\sigma(t)\xrightarrow{\,{a}\,}\sigma(t^{\prime})$ for all substitutions
$\sigma$. The norm and depth of a term are defined exactly as the norm and
depth of processes, by replacing the transition relation over processes with
that over terms. Equivalently, the norm and depth of terms can be defined
inductively over the structure of terms as follows:

  * •

$\mathrm{norm}(\mathbf{0})=0$;

  * •

$\mathrm{norm}(x)=0$;

  * •

$\mathrm{norm}(a.t)=1+\mathrm{norm}(t)$;

  * •

$\mathrm{norm}(t+u)=\min\\{\mathrm{norm}(t),\mathrm{norm}(u)\\}$;

  * •

$\mathrm{norm}(t\mathbin{\|}u)=\mathrm{norm}(t)+\mathrm{norm}(u)$.

  * •

$0pt(\mathbf{0})=0$;

  * •

$0pt(x)=0$;

  * •

$0pt(a.t)=1+0pt(t)$;

  * •

$0pt(t+u)=\max\\{0pt(t),0pt(u)\\}$;

  * •

$0pt(t\mathbin{\|}u)=0pt(t)+0pt(u)$.

For $k\geq 0$, we denote by $\mathrm{var}_{k}(t)$ the set of variables
occurring in the $k$-derivatives of $t$, namely
$\mathrm{var}_{k}(t)=\\{x\in\mathrm{var}(t^{\prime})\mid
t\xrightarrow{\,{\alpha}\,}t^{\prime},|\alpha|=k\\}$. Finally, we write
$t\sim_{\mathtt{PF}}u$ if $\sigma(t)\sim_{\mathtt{PF}}\sigma(u)$ for all
closed substitutions $\sigma$.

######  Lemma 28.

Let $t,u$ be two $\mathrm{BCCSP}_{\scriptsize\|}$ terms. If
$t\sim_{\mathtt{CT}}u$ then:

  1. (1)

For each $k\geq 0$ it holds that $\mathrm{var}_{k}(t)=\mathrm{var}_{k}(u)$.

  2. (2)

$t$ has a summand $x$, for some variable $x$, if and only if $u$ does.

  3. (3)

$\mathrm{norm}(t)=\mathrm{norm}(u)$ and $0pt(t)=0pt(u)$.

######  Proof 6.3.

  1. (1)

Assume, towards a contradiction, that for some $k\geq 0$ there is a variable
$x$ such that $x\in\mathrm{var}_{k}(t)\setminus\mathrm{var}_{k}(u)$. In
particular, this means that there is a term $t^{\prime}$ such that
$t\xrightarrow{\,{\alpha}\,}t^{\prime}$ for some trace $\alpha$ with
$|\alpha|=k$ and $x\in\mathrm{var}(t^{\prime})$. However, there is no
$u^{\prime}$ such that $u\xrightarrow{\,{\beta}\,}u^{\prime}$ for some trace
$\beta$ with $|\beta|=k$ and $x\in\mathrm{var}(u^{\prime})$. We can assume,
without loss of generality, that $k$ is the largest natural number such that
$x\in\mathrm{var}_{k}(t)$.

Let $n>0pt(t),0pt(u)$. Consider the closed substitution $\sigma$ defined by

$\sigma(y)=\begin{cases}a^{n}&\text{ if }y=x\\\ \mathbf{0}&\text{
otherwise.}\end{cases}$

Then $t\sim_{\mathtt{CT}}u$ implies $t\sim_{\mathtt{T}}u$ and thus
$t\xrightarrow{\,{\alpha}\,}t^{\prime}$ implies that
$u\xrightarrow{\,{\alpha}\,}u^{\prime}$ for some $u^{\prime}$. Let us proceed
by a case analysis on the structure of $t^{\prime}$ to obtain the desired
contradiction.

     * •

$t^{\prime}=x+w$ for some term $w$. Then we get that $\sigma(t)$ has $\alpha
a^{n}$ as a completed trace. However, due to the choices of $n$ and $\sigma$,
we have that $\sigma(u)$ cannot perform the completed trace $a^{n}$ after
$\alpha$, thus contradicting $t\sim_{\mathtt{CT}}u$. By the assumption that
$k$ is the largest natural number such that $x\in\mathrm{var}_{k}(t)$ is
suffices to consider two cases:

     * •

$t^{\prime}=(x+w)\mathbin{\|}w^{\prime}$ for some terms $w,w^{\prime}$ with
$w^{\prime}\neq\mathbf{0}$. From $t\sim_{\mathtt{T}}u$, we infer that for all
$\beta\in\mathtt{CT}(\sigma(w^{\prime}))$ we have that $\alpha\beta$ is a
trace of $\sigma(t)$ and thus of $\sigma(u)$. However, we can proceed as in
the previous case and argue that $\alpha
a^{n}\beta\in\mathtt{CT}(t)\setminus\mathtt{CT}(u)$, which is a contradiction
with $t\sim_{\mathtt{CT}}u$.

  2. (2)

Assume now that $t$ has a summand $x$ for some variable $x$. Then, from item
(1) of this lemma, $x\in\mathrm{var}_{0}(t)$ implies
$x\in\mathrm{var}_{0}(u)$. By applying similar reasoning as in the proof of
the first statement of the lemma we obtain that it cannot be the case that all
the occurrences of $x$ in $u$ are in the scope of prefixing. Hence, $u$ has,
at least, one summand $u^{\prime}$ such that either $u^{\prime}=x$ or
$u^{\prime}=(x+w)\mathbin{\|}w^{\prime}$, for some terms $w,w^{\prime}$ with
$w^{\prime}\neq\mathbf{0}$. Our order of business is to show that it cannot be
the case that all summands $u^{\prime}$ of $u$ with
$x\in\mathrm{var}_{0}(u^{\prime})$ are of the latter form. To this end,
assume, towards a contradiction, that whenever
$x\in\mathrm{var}_{0}(u^{\prime})$ then
$u^{\prime}=(x+w)\mathbin{\|}w^{\prime}$. Let $n>depth(u)$ and consider the
closed substitution $\sigma^{\prime}$ defined by

$\sigma^{\prime}(y)=\begin{cases}a^{n}&\text{ if }y=x\\\ b&\text{
otherwise.}\end{cases}$

Since $t$ has a summand $x$, we obtain that
$a^{n}\in\mathtt{CT}(\sigma^{\prime}(t))$. However,
$a^{n}\not\in\mathtt{CT}(\sigma^{\prime}(u))$. In fact,
$w^{\prime}\neq\mathbf{0}$ and $\sigma^{\prime}(y)\neq\mathbf{0}$ for all
variables $y\in\mathcal{V}$ give that
$\mathtt{I}(\sigma^{\prime}(w^{\prime}))\neq\emptyset$ for all terms
$w^{\prime}$ occurring in the summands $u^{\prime}$ of $u$ such that
$x\in\mathrm{var}_{0}(u^{\prime})$. Therefore
$a^{n}\not\in\mathtt{CT}(\sigma^{\prime}(u^{\prime}))$ for all such summands.
Due to choices of $\sigma^{\prime}$ and $n$, we can conclude that there is no
summand of $\sigma^{\prime}(u)$ having $a^{n}$ has a completed trace, so that
$a^{n}\not\in\mathtt{CT}(\sigma^{\prime}(u))$. This gives a contradiction with
$\sigma^{\prime}(t)\sim_{\mathtt{CT}}\sigma^{\prime}(u)$ and thus with
$t\sim_{\mathtt{CT}}u$.

  3. (3)

$\mathrm{norm}(t)=\mathrm{norm}(u)$ and $0pt(t)=0pt(u)$ follow immediately
from $t\sim_{\mathtt{CT}}u$ and items (1), (2) of this lemma.

######  Remark 29.

Since for all $\mathrm{BCCSP}_{\scriptsize\|}$ terms $t,u$ we have that
$t\sim_{\mathtt{PF}}u$ implies $t\sim_{\mathtt{CT}}u$, Lemma 28 holds also for
all pairs of possible futures equivalent terms.

######  Proposition 30.

Assume that $p,q$ are two $\mathrm{BCCSP}_{\scriptsize\|}$ processes such that
$p,q\not\sim_{\mathtt{PF}}\mathbf{0}$, $p,q$ do not have $\mathbf{0}$ summands
or factors, and $p\mathbin{\|}q\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$, for some
$N>1$. Then either $p\sim_{\mathtt{PF}}a$ and $q\sim_{\mathtt{PF}}p_{N}$, or
$p\sim_{\mathtt{PF}}p_{N}$ and $q\sim_{\mathtt{PF}}a$.

######  Proof 6.4.

By Lemma 28.3, from

$p\mathbin{\|}q\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$ (5)

we can infer that $\mathrm{norm}(p\mathbin{\|}q)=3$. Hence, since
$p,q\not\sim_{\mathtt{PF}}\mathbf{0}$, we have that either
$\mathrm{norm}(p)=1$ and $\mathrm{norm}(q)=2$, or vice versa. We consider only
the former case and prove that then $p\sim_{\mathtt{PF}}a$ and
$q\sim_{\mathtt{PF}}p_{N}$. In the other case it can be proved that
$p\sim_{\mathtt{PF}}p_{N}$ and $q\sim_{\mathtt{PF}}a$ by analogous reasoning.

So assume that $\mathrm{norm}(p)=1$ and $\mathrm{norm}(q)=2$. From Equation
(5) we get that $\mathtt{I}(p),\mathtt{I}(q)\subseteq\\{a,b\\}$. First of all
we argue that it cannot be the case that $a\in\mathtt{I}(p)\cap\mathtt{I}(q)$.
In fact, in that case $p\mathbin{\|}q$ would be able to perform the trace
$a^{2}$, whereas $a\mathbin{\|}p_{N}$ cannot do so, thus giving a
contradiction with Equation (5). We now proceed to show that
$a\in\mathtt{I}(p)$. Assume now, towards a contradiction, that this is not the
case and $\mathtt{I}(p)=\\{b\\}$. This, together with $\mathrm{norm}(p)=1$,
gives that $p$ has a summand $b$. Hence, given any $\alpha\in\mathtt{CT}(q)$
we have that $\alpha b\in\mathtt{CT}(p\mathbin{\|}q)$. However, $\alpha
b\not\in\mathtt{CT}(a\mathbin{\|}p_{N})$, as any completed trace of
$a\mathbin{\|}p_{N}$ must end with an $a$, thus giving that
$p\mathbin{\|}q\not\sim_{\mathtt{CT}}a\mathbin{\|}p_{N}$, which contradicts
Equation (5). We have therefore obtained that
$a\in\mathtt{I}(p),a\not\in\mathtt{I}(q)$ and, moreover, $p$ does not have a
summand $b$. Since $p$ has norm $1$, we conclude that it has a summand $a$.

We now proceed to show that also $0pt(p)=1$, and thus $p\sim_{\mathtt{PF}}a$.
Since $p$ has a summand $a$, we have that
$p\mathbin{\|}q\xrightarrow{\,{a}\,}\mathbf{0}\mathbin{\|}q\sim_{\mathtt{PF}}q$.
By Equation (5), we get $a\mathbin{\|}p_{N}\xrightarrow{\,{a}\,}r$ for some
$r$ such that $q\sim_{\mathtt{T}}r$. Since $a\mathbin{\|}p_{N}$ has a unique
initial $a$-transition
$a\mathbin{\|}p_{N}\xrightarrow{\,{a}\,}\mathbf{0}\mathbin{\|}p_{N}$, we get
that $r\sim_{\mathtt{PF}}p_{N}$ and $q\sim_{\mathtt{T}}p_{N}$. As a
consequence, we obtain that $0pt(q)=N+1$. Then we have

$\displaystyle 0pt(p)={}$ $\displaystyle 0pt(p\mathbin{\|}q)-0pt(q)$
$\displaystyle={}$ $\displaystyle 0pt(a\mathbin{\|}p_{N})-0pt(q)$ (by Eq. (5)
and Lem. 28.3) $\displaystyle={}$ $\displaystyle N+2-(N+1)$ $\displaystyle={}$
$\displaystyle 1\enspace.$

Therefore, we have obtained that $p\sim_{\mathtt{PF}}a$ and thus, since
possible futures equivalence is a congruence with respect to parallel
composition, from Equation (5) it follows that

$a\mathbin{\|}q\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}\enspace.$ (6)

Our order of business will now be to show that $q\sim_{\mathtt{PF}}p_{N}$. We
already know that $\mathtt{T}(q)=\mathtt{T}(p_{N})$. Moreover, as an initial
$a$-transition of $a\mathbin{\|}q$ cannot stem from $q$, from
$(ab^{i}a,\emptyset)\in\mathtt{PF}(a\mathbin{\|}p_{N})$ for all
$i\in\\{1,\dots,N\\}$, we get that
$\mathtt{CT}(p_{N})\subseteq\mathtt{CT}(q)$. Assume, towards a contradiction,
that $\mathtt{CT}(q)\not\subseteq\mathtt{CT}(p_{N})$. As
$q\sim_{\mathtt{T}}p_{N}$, this implies that $q$ has a completed trace of the
form $b^{j}$ for some $1\leq j\leq N$. Hence,
$(ab^{j},\emptyset)\in\mathtt{PF}(a\mathbin{\|}q)$. However, no completed
trace of $a\mathbin{\|}p_{N}$ has a $b$ as last symbol and thus
$a\mathbin{\|}p_{N}$ has no possible future of the form $(\alpha b,\emptyset)$
for some trace $\alpha$. This gives a contradiction with Equation (6).
Therefore, we have that $\mathtt{T}(q)=\mathtt{T}(p_{N})$ and
$\mathtt{CT}(q)=\mathtt{CT}(p_{N})$, thus giving $q\sim_{\mathtt{CT}}p_{N}$.
Notice that, by Lemma 26, this implies that $q$ does not contain any
occurrence of $\mathbin{\|}$ and $q$ can be written in the general form
$q=\sum_{j\in J}q_{j}$ where none of the $q_{j}$ has $+$ as head operator.

Assume, towards a contradiction, that $q\not\sim_{\mathtt{PF}}p_{N}$. By Lemma
27 this implies that either there is an $i\in\\{1,\dots,N\\}$ such that
$b^{i}a\not\sim_{\mathtt{PF}}q_{j}$ for all $j\in J$, or there is a $j\in J$
such that $q_{j}\not\sim_{\mathtt{PF}}b^{i}a$ for all $i\in\\{1,\dots,N\\}$.
In both cases, we can proceed as in the proof of Lemma 27 and obtain a
contradiction with $a\mathbin{\|}p_{N}\sim_{\mathtt{PF}}a\mathbin{\|}q$.

We have therefore obtained that $q\sim_{\mathtt{PF}}p_{N}$, and the proof is
thus concluded.

The following lemma characterises the open $\mathrm{BCCSP}_{\scriptsize\|}$
terms whose substitution instances can be equivalent in possible futures
semantics to terms having at least two summands of $p_{N}$ ($N>1$) as their
summands.

######  Lemma 31.

Let $t$ be a $\mathrm{BCCSP}_{\scriptsize\|}$ term that does not have $+$ as
head operator. Let $m>1$ and $\sigma$ be a closed substitution such that
$\sigma(t)$ has no $\mathbf{0}$ summands or factors. If
$\sigma(t)\sim_{\mathtt{PF}}\sum_{k=1}^{m}b^{i_{k}}a$, for some $1\leq
i_{1}<\dots<i_{m}$, then $t=x$ for some variable $x$.

######  Proof 6.5.

For simplicity of notation, we let $q_{m}$ denote $\sum_{k=1}^{m}b^{i_{k}}a$.
We proceed by showing that the remaining possible forms for $t$ give a
contradiction with $\sigma(t)\sim_{\mathtt{PF}}q_{m}$. We remark that
$\mathtt{I}(q_{m})=\\{b\\}$, and $\sigma(t)\sim_{\mathtt{PF}}q_{m}$ implies
$\mathtt{CT}(\sigma(t))=\mathtt{CT}(q_{m})$.

  * •

$t=b.t^{\prime}$ for some term $t^{\prime}$. Then
$\mathtt{CT}(\sigma(t^{\prime}))=\\{b^{i_{k}-1}a\mid k\in\\{1,\dots,m\\}\\}$,
and since $m>1$ we have that $|\mathtt{CT}(t^{\prime})|\geq 2$. It is then
immediate to verify that
$(b,\mathtt{T}(\sigma(t^{\prime})))\in\mathtt{PF}(\sigma(t))$, whereas
$(b,\mathtt{T}(\sigma(t^{\prime})))\not\in\mathtt{PF}(q_{m})$, since whenever
$q_{m}\xrightarrow{\,{b}\,}r$ then $\mathtt{T}(r)$ includes only one trace of
the form $b^{j}a$ for some $j\in\\{i_{1}-1,\dots,i_{m}-1\\}$. This gives a
contradiction with $\sigma(t)\sim_{\mathtt{PF}}q_{m}$.

  * •

$t=t^{\prime}\mathbin{\|}t^{\prime\prime}$ for some terms
$t^{\prime},t^{\prime\prime}$. Since $\sigma(t)$ has no $\mathbf{0}$ summands
or factors, neither does $t$ thus giving
$t^{\prime},t^{\prime\prime},\sigma(t^{\prime}),\sigma(t^{\prime\prime})\not\sim_{\mathtt{PF}}\mathbf{0}$.
Hence, we directly get a contradiction with
$\mathtt{CT}(\sigma(t))=\mathtt{CT}(q_{m})$, since all completed traces of
$q_{m}$ have exactly one occurrence of $a$ and this occurrence is as the last
action in the completed trace. No process of the form $p\mathbin{\|}q$ with
$\mathtt{I}(p),\mathtt{I}(q)\neq\emptyset$ can satisfy the same property.

We now have all the ingredients necessary to prove Theorem 25. To streamline
our presentation, we split the proof of into two parts: Proposition 33 deals
with the preservation of the witness property under provability from the
substitution rule of equational logic. Theorem 34 builds on Proposition 33 and
proves the witness property to be an invariant under provability from finite
sound axiom systems.

The following lemma is immediate.

######  Lemma 32.

Let $t$ be a $\mathrm{BCCSP}_{\scriptsize\|}$ term, and let $\sigma$ be a
closed substitution. If $x\in\mathrm{var}(t)$ then $0pt(\sigma(t))\geq
0pt(\sigma(x))$.

######  Proposition 33.

Let $t\approx u$ be an equation over $\mathrm{BCCSP}_{\scriptsize\|}$ that is
sound modulo $\sim_{\mathtt{PF}}$. Let $\sigma$ be a closed substitution with
$p=\sigma(t)$ and $q=\sigma(u)$. Suppose that $p$ and $q$ have neither
$\mathbf{0}$ summands nor $\mathbf{0}$ factors, and that
$p,q\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$ for some $N$ larger than the sizes
of $t$ and $u$. If $p$ has a summand possible futures equivalent to
$a\mathbin{\|}p_{N}$, then so does $q$.

######  Proof 6.6.

Since $\sigma(t)$ and $\sigma(u)$ have no $\mathbf{0}$ summands or factors,
neither do $t$ and $u$. We can therefore assume that, for some finite non-
empty index sets $I,J$,

$t=\sum_{i\in I}t_{i}\quad\text{ and }\quad u=\sum_{j\in J}u_{j}\enspace,$ (7)

where none of the $t_{i}$ ($i\in I$) and $u_{j}$ ($j\in J$) is $\mathbf{0}$ or
has $+$ as its head operator. Note that, as $t$ and $u$ have no $\mathbf{0}$
summands or factors, neither do $t_{i}$ ($i\in I$) and $u_{j}$ ($j\in J$).

Since $p=\sigma(t)$ has a summand which is possible futures equivalent to
$a\mathbin{\|}p_{N}$, there is an index $i\in I$ such that

$\sigma(t_{i})\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}\enspace.$

Our aim is now to show that there is an index $j\in J$ such that

$\sigma(u_{j})\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}\enspace,$

proving that $q=\sigma(u)$ has the required summand. This we proceed to do by
a case analysis on the form $t_{i}$ may have.

  1. (1)

Case $t_{i}=x$ for some variable $x$. In this case, we have that
$\sigma(x)\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$ and $t$ has $x$ as a summand.
As $t\approx u$ is sound with respect to possible futures equivalence, from
$t\sim_{\mathtt{PF}}u$ we get $t\sim_{\mathtt{CT}}u$. Hence, by Lemma 28.2, we
obtain that $u$ has a summand $x$ as well, namely there is an index $j\in J$
such that $u_{j}=x$. It is then immediate to conclude that $q=\sigma(u)$ has a
summand which is possible futures equivalent to $a\mathbin{\|}p_{N}$.

  2. (2)

Case $t_{i}=ct^{\prime}$ for some action $c\in\\{a,b\\}$ and term
$t^{\prime}$. This case is vacuous because, since
$\sigma(t_{i})=c\sigma(t^{\prime})\xrightarrow{\,{c}\,}\sigma(t^{\prime})$ is
the only transition afforded by $\sigma(t_{i})$, this term cannot be possible
futures equivalent to $a\mathbin{\|}p_{N}$.

  3. (3)

Case $t_{i}=t^{\prime}\mathbin{\|}t^{\prime\prime}$ for some terms
$t^{\prime},t^{\prime\prime}$. We have that
$\sigma(t_{i})=\sigma(t^{\prime})\mathbin{\|}\sigma(t^{\prime\prime})\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$.
As $\sigma(t_{i})$ has no $\mathbf{0}$ factors, it follows that
$\sigma(t^{\prime})\not\sim_{\mathtt{PF}}\mathbf{0}$ and
$\sigma(t^{\prime\prime})\not\sim_{\mathtt{PF}}\mathbf{0}$. Thus, by
Proposition 30, we can infer that, without loss of generality,

$\sigma(t^{\prime})\sim_{\mathtt{PF}}a\text{ and
}\sigma(t^{\prime\prime})\sim_{\mathtt{PF}}p_{N}\enspace.$

Notice that $\sigma(t^{\prime\prime})\sim_{\mathtt{PF}}p_{N}$ implies
$\mathtt{CT}(\sigma(t^{\prime\prime}))=\mathtt{CT}(p_{N})$. Now,
$t^{\prime\prime}$ can be written in the general form
$t^{\prime\prime}=v_{1}+\cdots+v_{l}$ for some $l>0$, where none of the
summands $v_{h}$ is $\mathbf{0}$ or a sum. By Lemma 27,
$\sigma(t^{\prime\prime})\sim_{\mathtt{PF}}p_{N}$ implies that for each
$i\in\\{1,\dots,N\\}$ there is a summand $r_{i}$ of $\sigma(t^{\prime\prime})$
such that $b^{i}a\sim_{\mathtt{PF}}r_{i}$, and for each summand $r$ of
$\sigma(t^{\prime\prime})$ there is an $i_{r}\in\\{1,\dots,N\\}$ such that
$r\sim_{\mathtt{PF}}b^{i}a$. Observe that, since $N$ is larger than the size
of $t$, we have that $l<N$. Hence, there must be some $h\in\\{1,\ldots,l\\}$
such that

$\sigma(v_{h})\sim_{\mathtt{PF}}\sum_{k=1}^{m}b^{i_{k}}a$

for some $m>1$ and $1\leq i_{1}<\ldots<i_{m}\leq N$. The term $\sigma(v_{h})$
has no $\mathbf{0}$ summands or factors, or else, so would
$\sigma(t^{\prime\prime})$ and $\sigma(t)$. By Lemma 31, it follows that
$v_{h}$ can only be a variable $x$ and

$\sigma(x)\sim_{\mathtt{PF}}\sum_{k=1}^{m}b^{i_{k}}a\enspace.$ (8)

Observe, for later use, that, since $t^{\prime}$ has no $\mathbf{0}$ factors,
the above equation yields that $x\not\in\mathrm{var}(t^{\prime})$, or else
$\sigma(t^{\prime})\not\sim_{\mathtt{PF}}a$ due to Lemma 32. So, modulo
possible futures equivalence, $t_{i}$ has the form
$t^{\prime}\mathbin{\|}(x+t^{\prime\prime\prime})$, for some term
$t^{\prime\prime\prime}$, with $x\not\in\mathrm{var}(t^{\prime})$,
$\sigma(t^{\prime})\sim_{\mathtt{PF}}a$ and
$\sigma(x+t^{\prime\prime})\sim_{\mathtt{PF}}p_{N}$.

Our order of business will now be to show that $\sigma(u)$ has a summand
$u_{j}$ that is possible futures equivalent to $a\mathbin{\|}p_{N}$. We recall
that $t\sim_{\mathtt{PF}}u$ implies $t\sim_{\mathtt{CT}}u$. Thus, by Lemma
28.1 we obtain that $\mathrm{var}_{k}(t)=\mathrm{var}_{k}(u)$ for all $k\geq
0$. Hence, from $x\in\mathrm{var}_{0}(t_{i})$ we get that there is at least
one $j\in J$ such that $x\in\mathrm{var}_{0}(u_{j})$.

So, firstly, we show that $x$ cannot occur in the scope of prefixing in
$u_{j}$, namely $u_{j}$ cannot be of the form $c.u^{\prime}$ or
$(c.u^{\prime}+u^{\prime\prime})\mathbin{\|}u^{\prime\prime\prime}$ for some
$c\in\\{a,b\\}$ and $u^{\prime}$ with $x\in\mathrm{var}(u^{\prime})$. We
proceed by a case analysis:

    1. (a)

$c=b$ and
$u_{j}=(b.u^{\prime}+u^{\prime\prime})\mathbin{\|}u^{\prime\prime\prime}$ for
some
$u^{\prime},u^{\prime\prime},u^{\prime\prime\prime}\in\mathrm{BCCSP}_{\scriptsize\|}$
with $x\in\mathrm{var}(u^{\prime})$. As $\sigma(u)$ does not have $\mathbf{0}$
summands or factors we have that
$\sigma(u^{\prime\prime\prime})\not\sim_{\mathtt{PF}}\mathbf{0}$. Let
$D=\max\\{d\mid x\in\mathrm{var}_{d}(u^{\prime})\\}$. From
$\sigma(x)\sim_{\mathtt{PF}}\sum_{k=1}^{m}b^{i_{k}}a$ (Equation (8)) and
$\mathtt{CT}(\sigma(u))=\mathtt{CT}(a\mathbin{\|}p_{N})$ we can infer that the
completed traces of $\sigma(u^{\prime\prime\prime})$ are of the form $b^{i}a$,
for some $i\in\\{0,\dots,N-i_{m}-D-1\\}$. In fact, since $\sigma(x)$ can
perform at least one completed trace of the form $b^{i_{k}}a$, for some $1\leq
i_{k}\leq N$, and the completed traces of $a\mathbin{\|}p_{N}$ contain exactly
two occurrences of $a$, of which one as the final action of the trace, we can
infer that the completed traces of $\sigma(u^{\prime\prime\prime})$ have to
contain exactly one occurrence of $a$, and this occurrence has to be as the
last symbol of the completed trace. Let
$\alpha\in\mathtt{T}(\sigma(u^{\prime}))$ be such that $|\alpha|=D$ and
$u^{\prime}\xrightarrow{\,{\alpha}\,}w$ with $x\in\mathrm{var}(w)$. By the
choice of $D$, we can infer that $x$ does not occur in the scope of prefixing
in $w$, and thus $\mathtt{T}(\sigma(x))\subseteq\mathtt{T}(\sigma(w))$. Then
we get that $(b^{i}ab\alpha,\mathtt{T}(\sigma(w)))\in\mathtt{PF}(\sigma(u))$,
where $b^{i}a\in\mathtt{CT}(\sigma(u^{\prime\prime\prime}))$. However, as
$m\geq 2$, there is no $p^{\prime}$ such that
$a\mathbin{\|}p_{N}\xrightarrow{\,{b^{i}ab\alpha}\,}p^{\prime}$ and
$\mathtt{T}(\sigma(x))\subseteq\mathtt{T}(p^{\prime})$, thus giving
$(b^{i}ab\alpha,\mathtt{T}(\sigma(w)))\not\in\mathtt{PF}(a\mathbin{\|}p_{N})$.
This gives a contradiction with
$\sigma(u)\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$.

    2. (b)

$c=b$ and $u_{j}=b.u^{\prime}$ for some $\mathrm{BCCSP}_{\scriptsize\|}$ term
$u^{\prime}$ with $x\in\mathrm{var}(u^{\prime})$. The proof of this case is
similar to, actually simpler than, that of the previous case and it is
therefore omitted.

    3. (c)

$c=a$ and
$u_{j}=(a.u^{\prime}+u^{\prime\prime})\mathbin{\|}u^{\prime\prime\prime}$ for
some
$u^{\prime},u^{\prime\prime},u^{\prime\prime\prime}\in\mathrm{BCCSP}_{\scriptsize\|}$
with $x\in\mathrm{var}(u^{\prime})$. As $\sigma(u)$ does not have $\mathbf{0}$
summands or factors we have that
$\sigma(u^{\prime\prime\prime})\not\sim_{\mathtt{PF}}\mathbf{0}$. From
$\sigma(x)\sim_{\mathtt{PF}}\sum_{k=1}^{m}b^{i_{k}}a$ we infer that
$\mathtt{T}(a.\sigma(u^{\prime}))$ includes traces having two occurrences of
action $a$. Since $\sigma(u)\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$, this
implies that there is no $\alpha\in\mathtt{T}(\sigma(u^{\prime\prime\prime}))$
such that $\alpha$ contains an occurrence of action $a$, for otherwise
$\sigma(u)$ could perform a trace having 3 occurrences of that action. In
particular, this implies that the last symbol in each trace of
$\sigma(u^{\prime\prime\prime})$ must be action $b$. This gives that there is
at least one completed trace of $\sigma(u_{j})$, and thus of $\sigma(u)$,
whose last symbol is action $b$. Hence we get
$\mathtt{CT}(\sigma(u))\neq\mathtt{CT}(a\mathbin{\|}p_{N})$, thus giving a
contradiction with $\sigma(u)\sim_{\mathtt{PF}}a\mathbin{\|}p_{N}$.