From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases

Our main objective is to prove the following theorem.

Following the strategy above, we introduce an infinite family of sound inequations for which there exist no finite, sound, axiomatisation from which we can derive all of them:

Intuitively, if we have a closed substitution $\rho$ then $\rho (x)$ is simulated by $\rho (x+x^n)$ and $I(\rho (x))=I(\rho (x+x^n))$. Moreover, Lemma 10 implies that all the inequations in (1) are also sound modulo $\precsim$ for all ${\precsim }_{\mathrm{𝖱𝖲}}\subseteq \precsim \subseteq {\precsim }_{\mathrm{𝖢𝖳}}$.

Next, we identify a property of terms that is invariant under provability from a finite axiom system $ℰ$ that is sound modulo ${\precsim }_{\mathrm{𝖢𝖳}}$. To this end, notice that, since $ℰ$ is finite, it can only contain terms with a breadth less than some $n\ge 2$. Consider then a derivation $ℰ⊢t⪯u$ where $u{\precsim }_{\mathrm{𝖢𝖳}}x+x^n$ and $t{\simeq }_{\mathrm{𝖢𝖳}}x$. We will argue that no derivation step can increase the breadth of the term, showing that $u{\simeq }_{\mathrm{𝖢𝖳}}x$ must hold as well. The following proposition shows that this property is an invariant under provability from finite, sound, axiom systems.

The following properties are straightforward:

1. 1.

   $t{\precsim }_{\mathrm{𝖢𝖳}}u$, by the soundness of $ℰ$;

2. 2.

   $|t|=|u|=0$, by Lemma 4;

3. 3.

   $[[t]]=1$, by Lemma 8;

4. 4.

   $var(t)=var(u)=\{x\}$, by Lemma 3.

The proof of Proposition 11 is by induction on the length of the derivation of $t⪯u$ from $ℰ$, with a case distinction on the last rule used in the derivation. We will sketch here the proof of the most interesting case, i.e. the case of the substitution rule. The core of the proof lies in determining the syntactic structure of $t$ and $u$. We do this by means of the novel notion of breadth: by showing that $[[u]]=1$ must hold, we can determine that $u{\simeq }_{\mathrm{𝖢𝖳}}x$. To this end, we present some properties on the depth and breadth of terms as in Proposition 11:

Assume that $ℰ⊢t⪯u$ because $t=\sigma (v)$ and $u=\sigma (w)$ from some $v⪯w\in ℰ$ and substitution $\sigma$. We have $\sigma (v){\precsim }_{\mathrm{𝖢𝖳}}\sigma (w)$, and since $\sigma (w){\precsim }_{\mathrm{𝖢𝖳}}x+x^n$, we can use Lemma 12.1 to obtain $[[\sigma (w)]]=1$ or $[[\sigma (w)]]=n$. We argue that $[[\sigma (w)]]=1$ must hold, so assume, towards a contradiction, $[[\sigma (w)]]=n$. We have , so there must be some variable $y\in var(w)$ such that $2\le [[\sigma (y)]]\le n$. By the soundness of $ℰ$ we have $v{\precsim }_{\mathrm{𝖢𝖳}}w$. Since $\sigma (w){\precsim }_{\mathrm{𝖢𝖳}}x+x^n$, by Lemma 4 we get $|\sigma (w)|=0$, from which, by Lemma 5, we infer $|w|=0$. Hence, by Lemma 12.2 we obtain $y\in var(v)$. Then we reach a contradiction, since $[[\sigma (v)]]\ge [[\sigma (y)]]>1$ contradicts $[[\sigma (v)]]=1$. Consequently, $[[\sigma (w)]]=1$, so $\sigma (w){\simeq }_{\mathrm{𝖢𝖳}}x$ by Lemma 12.4.

Theorem 9 then follows by noticing that no inequation in (1) satisfies the considered property. In fact, while it is clearly the case that $x{\simeq }_{\mathrm{𝖢𝖳}}x$ and $x+x^n{\precsim }_{\mathrm{𝖢𝖳}}x+x^n$, it is not true that $x+x^n{\simeq }_{\mathrm{𝖢𝖳}}x$. In light of Proposition 11, this means that no finite axiomatisation that is sound modulo ${\precsim }_{\mathrm{𝖢𝖳}}$ can derive all the inequations in (1). Hence, there is not finite basis for ${\precsim }_{\mathrm{𝖢𝖳}}$ over ${\text{BCCSP}}_{\parallel }$. Then, recall that the considered inequations are also sound modulo ${\precsim }_{\mathrm{𝖱𝖲}}$ (Lemma 10). Let ${\precsim }_{\mathrm{𝖱𝖲}}\subseteq \precsim \subseteq {\precsim }_{\mathrm{𝖢𝖳}}$ be a precongruence over ${\text{BCCSP}}_{\parallel }$, and let $ℰ$ be any finite inequational axiomatisation for ${\text{BCCSP}}_{\parallel }$ that is sound modulo $\precsim$. Since $\precsim \subseteq {\precsim }_{\mathrm{𝖢𝖳}}$, we have that $ℰ$ is sound modulo ${\precsim }_{\mathrm{𝖢𝖳}}$. Let $n\ge 2$ and larger than the breadth of each term in the inequations in $ℰ$. Then $x⪯x+x^n$ cannot be derived from $ℰ$. Since this inequation is sound modulo $\precsim$, it follows that $ℰ$ is not complete modulo $\precsim$.

We now show how we can extend Theorem 9 from preorders to equivalences. Specifically, the goal is to prove the following theorem.

From Lemma 10, we infer that the inequation $a.x⪯a.(x+x^n)$ is sound modulo ${\precsim }_{\mathrm{𝖱𝖲}}$ for any $a\in A$. Then, we consider the infinite family of equations:

Intuitively, for any closed substitution $\rho$, $\rho (a.x+a.(x+x^n))$ is simulated by $\rho (a.(x+x^n))$ and vice versa. Additionally, the set of initial actions is $\{a\}$. As a direct consequence of Lemma 14, every equation in (2) is sound modulo $\simeq$ for all ${\simeq }_{\mathrm{𝖱𝖲}}\subseteq \simeq \subseteq {\simeq }_{\mathrm{𝖢𝖳}}$.

We can prove that the equations in (2) are not derivable from any finite axiom system $ℰ$ which is sound modulo ${\simeq }_{\mathrm{𝖢𝖳}}$ and contains terms up to breadth $n\ge 2$. Informally, consider the derivation $ℰ⊢a.x+a.(x+x^n)\approx a.(x+x^n)$. The question is whether we can apply an axiom $v\approx w\in ℰ$, with $\sigma (v)=a.x+a.(x+x^n)$ and $\sigma (w)=a.(x+x^n)$. Since $w$ has a breadth less than $n$, there must be some variable $y\in var(v)$ encapsulating some part of $x^n$. However, equation $a.x+a.(x+x^k\parallel y)\approx a.(x+x^k\parallel y)$ with $k\ge 1$ is not sound modulo ${\simeq }_{\mathrm{𝖢𝖳}}$. Unfortunately, the proof is not this immediate, since the direct application of the axiom does not cover the general case in the considered derivation. Still, notice that $a.x\stackrel{𝑎}{\to }x$, while $a.(x+x^n)\stackrel{𝑎}{\to }x+x^n$ is the only transition from $a.(x+x^n)$. Then, we show that having an $a$-derivative that is completed trace equivalent to a variable is an invariant under provability from finite, sound, axiom systems. Afterwards, we can argue that no equation in (2) satisfies this invariant, from which the non-existence of a finite basis modulo ${\simeq }_{\mathrm{𝖢𝖳}}$ follows.

Also in this case we have some straightforward properties:

1. 1.

   $t{\simeq }_{\mathrm{𝖢𝖳}}u$ by the soundness of $ℰ$;

2. 2.

   $|t|=|u|=1$ by Lemma 4 and the fact that $t\stackrel{𝑎}{\to }$;

3. 3.

   $1\le [[t]]=[[u]]\le n$ by Lemma 8 and the fact that $t^{\prime }{\simeq }_{\mathrm{𝖢𝖳}}x$; and

4. 4.

   $var(t)=var(u)=\{x\}$ by Lemma 3 and the fact that $t^{\prime }{\simeq }_{\mathrm{𝖢𝖳}}x$.

Moreover, as we consider terms $t{\precsim }_{\mathrm{𝖢𝖳}}a.(x+x^n)$, the following lemma will be helpful.

Proposition 15 is proved by induction on the derivation of $ℰ⊢t\approx u$. We sketch only the substitution case. Assume that $ℰ⊢t\approx u$ because $t=\sigma (v)$ and $u=\sigma (w)$ for some $v\approx w\in ℰ$ and substitution $\sigma$. We distinguish two cases, according to the derivation of $t\stackrel{𝑎}{\to }{t}^{\prime }$.

Assume first that there exists some $v^{\prime }$ such that $v\stackrel{𝑎}{\to }{v}^{\prime }$ and $\sigma (v^{\prime }){\simeq }_{\mathrm{𝖢𝖳}}x$. Then consider the closed substitution $\rho$ defined as $\rho (y)=\mathrm{𝟎}$ if $[[\sigma (y)]]\le 1$ and $\rho (y)=a^2\mathbf{.0}$ otherwise. Then, $\rho (v^{\prime })\to ̸$, so $a\in \mathrm{𝖢𝖳}(\rho (v))$. From the soundness of $ℰ$, we have $v{\simeq }_{\mathrm{𝖢𝖳}}w$, so $a\in \mathrm{𝖢𝖳}(\rho (w))$. By construction of $\rho$, this gives that $w\stackrel{𝑎}{\to }{w}^{\prime }$ for some $w^{\prime }$ s.t. $\rho (w^{\prime })\to ̸$. Then, $\sigma (w)\stackrel{𝑎}{\to }\sigma (w^{\prime })$. By Lemma 16 we obtain $\sigma (w^{\prime }){\precsim }_{\mathrm{𝖢𝖳}}x+x^n$, so by Lemma 1 it holds that either $[[\sigma (w^{\prime })]]=1$ or $[[\sigma (w^{\prime })]]=n$. If $[[\sigma (w^{\prime })]]=1$, then $\sigma (w^{\prime }){\simeq }_{\mathrm{𝖢𝖳}}x$ by Lemma 4, so the invariant holds. If $[[\sigma (w^{\prime })]]=n$, then since , there exists some variable $z\in var(w^{\prime })$ such that $2\le [[\sigma (z)]]\le n$. However, we reach a contradiction, since $\rho (w^{\prime })\stackrel{𝑎}{\to }$ contradicts $\rho (w^{\prime })\to ̸$.

Assume now that there is no $v^{\prime }$ such that $v\stackrel{𝑎}{\to }{v}^{\prime }$ and $\sigma (v^{\prime }){\simeq }_{\mathrm{𝖢𝖳}}x$. We first prove that there is some $y\in var(v)$ s.t. $\sigma (y)\stackrel{𝑎}{\to }{t}^{\prime \prime }$ and either $t^{\prime }=t^{\prime \prime }$ or $t^{\prime }=t^{\prime \prime }\parallel \sigma (v_{\parallel })$ for some $v_{\parallel }$. We have $\sigma (v)\stackrel{𝑎}{\to }{t}^{\prime }$, so there must exist some summand $v^{\prime }$ of $v$ such that $\sigma (v^{\prime })\stackrel{𝑎}{\to }{t}^{\prime }$. We proceed by a case distinction on the structure of $v^{\prime }$. We consider only the case $v^{\prime }=v_1\parallel v_2$. In this case, assume, without loss of generality, that $\sigma (v_1)\stackrel{𝑎}{\to }{t}_1$ such that $t^{\prime }=t_1\parallel \sigma (v_2)$. Note that $\sigma (v_2)\to ̸$, since $|\sigma (v)|=1$. We can then perform a case distinction on the summands of $v_1$ to prove that there is some $y\in var(v_1)$ such that $\sigma (y)\stackrel{𝑎}{\to }{t}^{\prime \prime }$ and either $t^{\prime }=t^{\prime \prime }\parallel \sigma (v_2)$ or $t^{\prime }=t^{\prime \prime }\parallel \sigma (v_{\parallel }^{\prime })\parallel \sigma (v_2)=t^{\prime \prime }\parallel \sigma (v_{\parallel }^{\prime }\parallel v_2)$ for some $v_{\parallel }^{\prime }$. If $t^{\prime \prime }=t^{\prime }$, it is clear that $t^{\prime \prime }{\simeq }_{\mathrm{𝖢𝖳}}x$. If $t^{\prime }=t^{\prime \prime }\parallel \sigma (v_{\parallel })$, from $t^{\prime \prime }\parallel \sigma (v_{\parallel }){\simeq }_{\mathrm{𝖢𝖳}}x$ and Lemma 8 it follows that $[[t^{\prime \prime }\parallel \sigma (v_{\parallel })]]=1$. So either $[[t^{\prime \prime }]]=1$ and $[[\sigma (v_{\parallel })]]=0$ or vice versa. Then $t^{\prime \prime }{\simeq }_{\mathrm{𝖢𝖳}}x$ and $\sigma (v_{\parallel }){\simeq }_{\mathrm{𝖢𝖳}}\mathrm{𝟎}$ or vice versa, by Lemmas 3, 4. Consider the closed substitution ${\rho }^{\prime }$ defined as ${\rho }^{\prime }(y)=a^2\mathbf{.0}$, ${\rho }^{\prime }(z)=\mathrm{𝟎}$ if $[[\sigma (z)]]\le 1$ and ${\rho }^{\prime }(z)=a^3\mathbf{.0}$ otherwise. Then $a^2\in \mathrm{𝖢𝖳}({\rho }^{\prime }(v))$ in both forms of $t^{\prime }$, so, by soundness of $ℰ$, $a^2\in \mathrm{𝖢𝖳}({\rho }^{\prime }(w))$. Hence, there is some summand $w^{\prime }$ of $w$ such that $a^2\in \mathrm{𝖢𝖳}({\rho }^{\prime }(w^{\prime }))$. We expand only the case $w^{\prime }=w_1\parallel w_2$. Assume, without loss of generality, that $a^2\in \mathrm{𝖢𝖳}({\rho }^{\prime }(w_1))$ and $\mathrm{𝖢𝖳}({\rho }^{\prime }(w_2))=\{\epsilon \}$ (it is impossible that $a\in \mathrm{𝖢𝖳}({\rho }^{\prime }(w_1))$ and $a\in \mathrm{𝖢𝖳}({\rho }^{\prime }(w_2))$, since $|\sigma (w)|\le 1$ and by construction of ${\rho }^{\prime }$). From $a^2\in \mathrm{𝖢𝖳}({\rho }^{\prime }(w_1))$, we can again do a case distinction on the summands of $w_1$. This process can be repeated a finite number of times, until the nested summand $y$ is reached. Let $w_{\parallel }$ be the accumulation of parallel compositions, such that $\mathrm{𝖢𝖳}({\rho }^{\prime }(w_{\parallel }))=\{\epsilon \}$. We obtain that $\sigma (w)\stackrel{𝑎}{\to }{t}^{\prime \prime }\parallel \sigma (w_{\parallel })$. By Lemma 16 we must have that $t^{\prime \prime }\parallel \sigma (w_{\parallel }){\precsim }_{\mathrm{𝖢𝖳}}x+x^n$. Hence, $[[t^{\prime \prime }\parallel \sigma (w_{\parallel })]]=1$ or $[[t^{\prime \prime }\parallel \sigma (w_{\parallel })]]=n$ by Lemma 1. In the first case we obtain that $t^{\prime \prime }\parallel \sigma (w_{\parallel }){\simeq }_{\mathrm{𝖢𝖳}}x$ by Lemma 4, so the invariant holds. In the second case we reason towards a contradiction as above. Hence, $a^2\in \mathrm{𝖢𝖳}({\rho }^{\prime }(w))$ only holds if $\sigma (w)\stackrel{𝑎}{\to }{u}^{\prime }$ for some $u^{\prime }{\simeq }_{\mathrm{𝖢𝖳}}x$.

As discussed above, the equations in (2) do not satisfy the invariant in Proposition 15. Hence Theorem 13 follows for ${\simeq }_{\mathrm{𝖢𝖳}}$. The same reasoning applied in Section 3.1 then allows us to conclude that Theorem 13 holds for any congruence included between ${\simeq }_{\mathrm{𝖱𝖲}}$ and ${\simeq }_{\mathrm{𝖢𝖳}}$.

The main result of this subsection is the following theorem.

For this section, assume $A=\{a\}$ and that $\simeq$ represents a congruence between ${\simeq }_{𝖲}$ and ${\simeq }_{𝖳}$. To prove that the algebra of ${\text{BCCSP}}_{\parallel }$ processes modulo $\simeq$ has no finite basis we apply the transformation technique: we show how a presupposed finite basis for the algebra of ${\text{BCCSP}}_{\parallel }$ processes modulo $\simeq$ can be transformed into a finite basis for the so-called max-plus algebra of natural numbers with $\max$ and $+$ as operations. Since it has been shown that the latter algebra is not finitely based [5], it then follows that the former cannot be finitely based either. A similar approach was applied by Aceto et al. to prove that there exists no finite basis modulo ${\simeq }_{𝖳}$ if $|A|=1$ over the process algebra BPA [4].

The following lemma is straightforward to prove.

Note that Lemma 18 establishes an isomorphism from the algebra of closed ${\text{BCCSP}}_{\parallel }$ expressions modulo $\simeq$ with constant $\mathrm{𝟎}$ and binary operations $+$ and $\parallel$ and the max-plus algebra with constant $0$ and binary operations $\max$ and $+$. Hence, there is a correspondence between the equational theories of these two algebras that we shall now formalise. We need the following inductively defined mapping (with $𝚆$ the set of variables in the max-plus algebra):

The following lemma is then the counterpart of Lemma 18 on the max-plus algebra, since the mapping defined above combines the depth of terms with occurrences of variables.

Now suppose that $ℰ$ is a finite basis for the algebra ${\text{BCCSP}}_{\parallel }$ processes modulo $\simeq$. Then, in particular, if $t\simeq u$, then $ℰ⊢t\approx u$. Now $ℰ$ may include axioms with action prefixes, so we cannot readily transform all of $ℰ$ into a complete set of axioms for the max-plus algebra. The following lemma, however, establishes that whenever two (open) ${\text{BCCSP}}_{\parallel }$ terms are equivalent modulo $\simeq$, then either both or neither have occurrences of the action prefix.

Now, let ${ℰ}^{\prime }\subseteq ℰ$ be obtained by removing all axioms with occurrences of the action prefix. By Lemma 20 we have, for all ${\text{BCCSP}}_{\parallel }$-terms $t$ and $u$ without occurrences of action prefixes that $ℰ⊢t\approx u$ if and only if ${ℰ}^{\prime }⊢t\approx u$. Denote by $⟨{ℰ}^{\prime }⟩$ the set of equations $⟨t⟩\approx ⟨u⟩$ such that $(t\approx u)\in {ℰ}^{\prime }$. Then, for $t,u$ without occurrences of action prefixes, $ℰ⊢t\approx u$ if and only if $⟨{ℰ}^{\prime }⟩⊢⟨t⟩=⟨u⟩$. It would follow that $⟨{ℰ}^{\prime }⟩$ is a finite basis for the max-plus algebra, which cannot exist. We conclude that the presupposed finite basis for the algebra of closed ${\text{BCCSP}}_{\parallel }$ expressions modulo $\simeq$ can also not exist.

We use the proof-theoretic technique discussed in Section 3 to prove the following:

Throughout this section consider $A=\{a_1,\mathrm{\dots },a_{|A|}\}$, where $a=a_1,b=a_2$ and $s=a_3\mathrm{\cdots }{a}_{|A|}$. Note that $s=\epsilon$ if $|A|=2$. Let $n\ge 1$, then consider the term

Then we introduce the following infinite family of inequations:

Intuitively, for any closed substitution $\rho$ we see that $\rho (a{b}^{n}s.x)$ is simulated by one of the summands of $\rho (h_n)$ because of the added parallel composition with $x$. If $\rho (x)\to ̸$ then it is the first summand, and if $\rho (x)\stackrel{𝑎}{\to }$, then it is the second summand, etc. Thus, for each of the $|A|+1$ options there is a corresponding summand.

We argue that not all inequations in the family are derivable using a finite collection of inequations $ℰ$, which is sound modulo ${\precsim }_{𝖳}$ and contains terms up to depth $n\ge 1$. First, we give some intuition why this is the case. Consider term $a{b}^{n}s.x$, for which we know that $a{b}^{n}s.x\stackrel{a{b}^{n}s}{\to }x$. However, $h_n$ cannot perform trace $a{b}^{n}s$ and reach a term with an occurrence of $x$. We introduce a new notion, named the $\mathrm{𝖿𝗋𝗈𝗇𝗍}$ of a term, to formally express this.

This means that whenever we have a substitution $\sigma$ such that $\sigma (x)\stackrel{𝑎}{\to }$, then $x\in \mathrm{𝖿𝗋𝗈𝗇𝗍}(t)$ implies $\sigma (t)\stackrel{𝑎}{\to }$. Additionally, it follows that if $|t|=0$, then $var(t)=\mathrm{𝖿𝗋𝗈𝗇𝗍}(t)$. Using this definition we obtain the following proposition.

Continuing our intuitive argument, consider $t=a{b}^{n}s.x$ and derivation $ℰ⊢a{b}^{n}s.x⪯u$ where $u{\precsim }_{𝖳}{h}_n$. Either we directly apply an axiom $v⪯w\in ℰ$ on $a{b}^{n}s.x$, so $\sigma (v)=a{b}^{n}s.x$ and $\sigma (w)=u$, or $ℰ⊢b^{n}s.x⪯u^{\prime }$ and $u=a.u^{\prime }$. To proceed, we need a property of $\mathrm{𝖿𝗋𝗈𝗇𝗍}$:

If $ℰ⊢b^{n}s.x⪯u^{\prime }$ and $u=a.u^{\prime }$, we can infer, from $b^{n}s.x{\precsim }_{𝖳}{u}^{\prime }$ and Lemma 26, that $u^{\prime }\stackrel{b^{n}s}{\to }{u}^{\prime \prime }$ and $x\in \mathrm{𝖿𝗋𝗈𝗇𝗍}(u^{\prime \prime })$, so that $a.u^{\prime }\stackrel{a{b}^{n}s}{\to }{u}^{\prime \prime }$ and $x\in \mathrm{𝖿𝗋𝗈𝗇𝗍}(u^{\prime \prime })$. If axiom $v⪯w\in ℰ$ is applied such that $\sigma (v)=a{b}^{n}s.x$ and $\sigma (w)=u$, then some part of $a{b}^{n}s.x$ must be encapsulated in a variable $y\in var(v)$, i.e. $v=(a{b}^{n}s)[..i].y$ for some . To see this, let us first introduce the notion of $\mathrm{𝟎}$-nested summand.

Using this new notion, we can prove the following lemma.

Hence, even if $v$ was of the form $v_1\parallel v_2$, thanks to Lemma 28 we can always eliminate one of the two parallel components, and repeat the reasoning on the remaining component until we reach a term $v^{\prime }{⊑}_{\mathrm{𝟎}}v$ such that $y\in \mathrm{𝖿𝗋𝗈𝗇𝗍}(v^{\prime })$. Consequently, $y$ is in the front of $v$ after performing trace $(a{b}^{n}s)[..i]$ and $x$ is in the front of $\sigma (y)$ after performing the remaining part of the trace, namely $(a{b}^{n}s)[i+1..]$. If $|A|\ge 3$, then we can infer from $v{\precsim }_{𝖳}w$ and Lemma 26 that $y$ is in the front after performing the same trace in $w$. Hence, $\sigma (w)\stackrel{a{b}^{n}s}{\to }{u}^{\prime }$ for some $u^{\prime }$ with $x\in \mathrm{𝖿𝗋𝗈𝗇𝗍}(u^{\prime })$. To complete our reasoning, we need a special case of Lemma 26 if $|A|=2$, covering the case in which variable $y$ is in the front of $v$ after performing trace $a{b}^k$ for some . Note that the following lemma holds for $|A|>2$ due to Lemma 26.

From Lemma 29 we know that $w$ can perform trace $a{b}^n[..k]$ for some for which $y\in \mathrm{𝖿𝗋𝗈𝗇𝗍}(w)$. We argue that $k=i$ must hold, because of the constraints of $\sigma (w)$ in regards to the depth and soundness.

Hence, we can conclude that, in all cases, $u=\sigma (w)\stackrel{a{b}^n}{\to }{u}^{\prime }$ for some term $u^{\prime }$ with $x\in \mathrm{𝖿𝗋𝗈𝗇𝗍}(u^{\prime })$.

Theorem 21 then follows by applying the same reasoning used to conclude Section 3.

The infinite family of inequations in (3) results in an infinite family of equations as:

Then, following a similar reasoning as used for Proposition 25, we can prove the invariance under equational derivation also in the case of equivalences.