Lean and Full Congruence Formats for Recursion

TL;DR

This paper distinguishes between lean and full congruence formats for recursion in process semantics, proving bisimilarity's congruence properties in various structural operational semantics formats.

Contribution

It introduces a formal distinction between lean and full congruence formats and proves bisimilarity's congruence properties within these frameworks.

Findings

Bisimilarity is a lean congruence for recursion in ntyft/ntyxt formats.

Bisimilarity is a full congruence in tyft/tyxt formats.

The paper clarifies the conditions under which bisimilarity preserves process equivalence.

Abstract

In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions. I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.

Equations

$$\begin{array}[]{l}p_{i}\sqsubseteq q_{i}~{}\mbox{for all}~{}i=1,...,n\\ ~{}~{}\Rightarrow~{}~{}f(p_{1},...,p_{n})\sqsubseteq f(q_{1},...,q_{n})\end{array}\vspace{-2ex}$$

$$\begin{array}[]{r}S_{Y}[\sigma]\sqsubseteq S_{Y}^{\prime}[\sigma]~{}\mbox{for all}~{}Y\mathbin{\in}W~{}\mbox{and}~{}\sigma\!:W\rightarrow{\rm T}(\Sigma)\\ \Rightarrow~{}~{}\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}$}\sqsubseteq\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}\!\!X|S^{\prime}\!\!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}$}\end{array}$$

$$a.x\stackrel{a}{⟶}x\frac{x\stackrel{a}{⟶}{x}^{\prime }}{x\Vert y\stackrel{a}{⟶}{x}^{\prime }\Vert y}\frac{y\stackrel{a}{⟶}{y}^{\prime }}{x\Vert y\stackrel{a}{⟶}x\Vert y^{\prime }}$$

$$\displaystyle\frac{\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}\!\!S_{X}|S\!\!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}$}\mathrel{\mathrel{\hbox{$\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}$}}}z}{\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}$}\mathrel{\mathrel{\hbox{$\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}$}}}z}$$

Full text

I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.

I Introduction

Structural Operational Semantics [45, 47] is one of the main methods for defining the meaning of system description languages like CCS [45]. A system or process is represented by a closed term built from a collection of operators, process variables and usually a recursion construct, and the behaviour of a process is given by its collection of (outgoing) transitions, each specifying the action the process performs by taking this transition, and the process that results after doing so. The transitions between states are obtained from a set of proof rules called transition rules.

For purposes of representation and verification, several behavioural equivalence relations have been defined on processes, of which the most well-known is (strong) bisimilarity [45]. To allow compositional system verification, such equivalences need to be congruences for the operators under consideration, meaning that the equivalence class of an $n$-ary operator $f$ applied to arguments $p_{1},\ldots,p_{n}$ is completely determined by the equivalence classes of these arguments.

Equally important is that the chosen equivalence relation $\sim$ is a congruence for recursion. Recursion allows the specification of a process as a canonical solution of an equation $X=E(X)$.111The particular solution supplied by structural operational semantics is the one whose transitions are determined by the transition rules. Here $E(X)$ is an expression that may contain the variable $X$. If $W$ is the collection of other variables occurring in $E(X)$, not bound by the recursive specification, then the canonical solution of $X=E(X)$ is a $W$-ary function that returns a process for each valuation of these variables as processes. I call $\sim$ a lean congruence for recursion if each such operator satisfies the above-mentioned congruence requirement.

Take for example $E(X)$ to be $a.X+Y$ in the language CCS of Milner [45]. Then $W=\{Y\}$. Let $\sim$ be bisimilarity, so that $b.0\sim b.0+b.0$ [45]. Now the lean congruence requirement for $\sim$ insists that the selected solutions of the recursive equations $X=a.X+b.0$ and $X=a.X+(b.0+b.0)$, obtained from $X=a.X+Y$ by substituting each of these bisimilar processes for $Y$, are again bisimilar.

The lean congruence requirement plays a key rôle in the study of expressiveness of system description languages [34]. There, correct translations of one language into another up to a semantic equivalence $\sim$ are defined; and expressiveness hierarchies—one for each choice of $\sim$—are defined in terms of those translations. However, a correct translation can exist only when $\sim$ is a lean congruence for the source language, as well as for the source’s image within the target language.

If $F(X)$ is an expression like $E(X)$, for simplicity assuming that neither contains variables other than $X$, and $E(p)\sim F(p)$ regardless which process $p$ is substituted for the variable $X$, then the full congruence property demands that the selected solutions of the equations $X=E(X)$ and $X=F(X)$ are again equivalent. As a CCS example, suppose that a process is given as the solution of the equation $X=a.X+a.X$. Using the idempotence of $+$ under bisimilarity, one can now proceed to think of the same process, up to bisimilarity, as the solution of $X=a.X$. This type of reasoning is a central component in system verification by equivalence checking [8, 18, 7, 38], as applied in successful verification toolsets such as CADP [25] and mCRL2 [38]. Yet it is valid only if bisimilarity is a full congruence for recursion.

In order to streamline the process of proving that a certain equivalence is a congruence for certain operators, and to guide sensible language definitions, syntactic criteria (congruence formats) for the transition rules in structural operational semantics have been developed, ensuring that the equivalence is a congruence for any operator specified by rules that meet these criteria. The first of these was proposed by Robert de Simone in [49, 50] and is now called the De Simone format. A generalisation featuring transition rules with negative premises is the GSOS format of Bloom, Istrail & Meyer [12], and a generalisation with lookahead is the tyft/tyxt format of Groote & Vaandrager [40]. The ntyft/ntyxt format of Groote [37] allows both negative premises and lookahead and generalises the GSOS as well as the tyft/tyxt format. All this work provides congruence formats for (strong) bisimilarity. Congruence formats for other strong semantic equivalences—treating the internal action $\tau$ like any other action—appear in [11, 22].222These congruence formats also apply to behavioural preorders, and then ensure that such a preorder is a precongruence. Formats for weak semantics—abstracting from internal activity—can be found, e.g., in [51, 10, 19, 52, 53, 33, 24, 21].

Extensions to probabilistic systems appear for instance in [9, 42, 41, 26, 44, 6, 17]. Rule formats ensuring properties of operators other than being a (pre)congruence appear in [46] (commutativity), [16] (associativity), [3] (zero and unit elements), [4] (distributivity) and [2] (idempotence). Overviews on work on congruence formats and other rule formats, with many more references, can be found in [5, 39].

Yet, to the best of my knowledge, no one has proposed a congruence format for recursion. This hiatus is addressed here. I establish that bisimilarity is a lean congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format.333Some of those languages have a 3-valued transition system semantics, where bisimilarity becomes an asymmetric preorder. Here I establish that it is a precongruence. I did not succeed in showing that it is even a full congruence for all ntyft/ntyxt languages; nor did I find a counterexample. Even for GSOS languages this remains an open question. However, I show that bisimilarity is a full congruence for recursion for all tyft/tyxt languages.

My proof strategy follows the traditional method of [12, 40, 13]. However, for this to work smoothly, I present a new formulation—better fitted to my application—of the well-founded semantics of transition system specifications with negative premises, and show its consistency with previous formulations.

I could not establish the full congruence result directly, without using the lean congruence result as an intermediate step, even when restricting the latter to the tyft/tyxt format. Thus, I see no way around a sequence of two proofs with a large overlap.

The method of modal decomposition [23] yields alternative congruence proofs for operators specified in the tyft/tyxt and GSOS formats [23]. Extending this method to deal with recursion might be a way to extend my full congruence result to transition rules with negative premises.

Providing (lean and full) congruence formats for recursion for equivalences and preorders other than bisimilarity, as well as for weak versions of bisimilarity [45, 36]—supporting abstraction from internal actions—remains an important open problem.

II Transition system specifications and their meaning

In this paper ${\it Var}$ and $A$ are two sets of variables and actions. Many concepts that will appear are parameterised by the choice of ${\it Var}$ and $A$, but as in this paper this choice is fixed, a corresponding index is suppressed.

Definition 1** **(Signatures)

A function declaration is a pair $(f,n)$ of a function symbol $f\not\in{\it Var}$ and an arity $n\in\mbox{\bbb N}$.444This work generalises seamlessly to operators with infinitely many arguments. Such operators occur, for instance, in [14, Appendix A.2]. Hence one may take $n$ to be any ordinal. An operator, like the summation or choice of CCS [45], that actually takes any set of arguments, needs to be simulated by a family of operators with a sequence of arguments (but yielding the same value upon reshuffling of the arguments), one for each cardinality of this set. A function declaration $(c,0)$ is also called a constant declaration. A signature is a set of function declarations. The set $\mbox{\bbb T}(\Sigma)$ of terms with recursion over a signature $\Sigma$ is defined inductively by:

• •

${\it Var}\subseteq\mbox{\bbb T}(\Sigma)$,

• •

if $(f,n)\mathbin{\in}\Sigma$ and $t_{1},...,t_{n}\mathbin{\in}\mbox{\bbb T}(\Sigma)$ then $f(t_{1},...,t_{n})\mathbin{\in}\mbox{\bbb T}(\Sigma)$,

• •

If $V_{S}\subseteq{\it Var}$, $~{}S:V_{S}\rightarrow\mbox{\bbb T}(\Sigma)$ and $X\in V_{S}$, then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\in\mbox{\bbb T}(\Sigma).

A term $c()$ is abbreviated as $c$. A function $S$ as appears in the last clause is called a recursive specification. A recursive specification $S$ is often displayed as $\{X\mathbin{=}S_{X}\mid X\mathbin{\in}V_{S}\}$. An occurrence of a variable $y$ in a term $t$ is free if it does not occur in a subterm of $t$ of the form \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} with $y\in V_{S}$. Let ${\it var}(t)$ denote the set of variables occurring free in a term $t\in\mbox{\bbb T}(\Sigma)$, and let $\mbox{\bbb T}(\Sigma,W)$ be the set of terms $t$ over $\Sigma$ with ${\it var}(t)\subseteq W$. ${\rm T}(\Sigma):=\mbox{\bbb T}(\Sigma,\emptyset)$ is set of closed terms over $\Sigma$.

Example 1

Let $\Sigma$ contain three unary functions $a.\_$, $b.\_$ and $d.\_$, and one infix-written binary function $\|$. Let $X,Y,z\mathbin{\in}{\it Var}$. Then $S=\{~{}X=(a.X)\|(b.Y),\quad Y=(d.Y)\|(X\|z)~{}\}$ is a recursive specification, so \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\in}\mbox{\bbb T}(\Sigma). Since $V_{S}\mathbin{=}\{X,Y\}$, the only variable that occurs free in this term is $z$.

As illustrated here, I often choose upper case letters for bound variables (the ones occurring in a set $V_{S}$) and lower case ones for variables occurring free; this is a convention only.

A recursive specification $S$ is meant to denote a $V_{S}$-tuple (in the example above a pair) of processes that—when filled in for the variables in $V_{S}$—forms a solution to the equations in $S$.555When $S$ contains free variables from a set $W$, this solution is parameterised by the choice of a valuation of these variables as processes, thereby becoming a $W$-ary function. The term \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} denotes the $X$-component of such a tuple.

Definition 2** **(Substitution)

A $\Sigma$-substitution $\sigma$ is a partial function from ${\it Var}$ to $\mbox{\bbb T}(\Sigma)$; it is closed if it is a total function from ${\it Var}$ to ${\rm T}(\Sigma)$. If $\sigma$ is a substitution and $S$ any syntactic object, then $S[\sigma]$ denotes the object obtained from $S$ by replacing, for $x$ in the domain of $\sigma$, every free occurrence of $x$ in $S$ by $\sigma(x)$, while renaming bound variables if necessary to prevent name-clashes. In that case $S[\sigma]$ is called a substitution instance of $S$. A substitution instance $t[\sigma]$ where $\sigma$ is given by $\sigma(x_{i})=u_{i}$ for $i\in I$ is denoted as $t[u_{i}/x_{i}]_{i\in I}$, and for $S$ a recursive specification \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!t|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} abbreviates t[\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Y|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}/Y]_{Y\in V_{S}}.

Example 2

Extend $\Sigma$ from Ex. 1 with a constant $c$. Then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[b.c/z]=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|{X{=}(a.X)|(b.Y),;Y{=}(d.Y)|(X|b.c)}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}, \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[X/z]=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|{Z{=}(a.Z)|(b.Y),\quad Y{=}(d.Y)|(Z|X)}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} and \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[b.c/Y]=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}.

Structural operational semantics [47] defines the meaning of system description languages whose syntax is given by a signature $\Sigma$. It generates a transition system in which the states, or processes, are the closed terms over $\Sigma$—representing the remaining system behaviour from that state—and transitions between processes are supplied with labels. The transitions between processes are obtained from a transition system specification, which consists of a set of transition rules.

Definition 3** **(Transition system specifications)

Let $\Sigma$ be a signature. A positive $\Sigma$-literal is an expression t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}t^{\prime} and a negative $\Sigma$-literal an expression t{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a\;$\hskip 2.5pt}\hfil}}}}} with $t,t^{\prime}\in\mbox{\bbb T}(\Sigma)$ and $a\in A$. For $t,t^{\prime}\in\mbox{\bbb T}(\Sigma)$ the literals t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}t^{\prime} and t{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a\;$\hskip 2.5pt}\hfil}}}}} are said to deny each other. A transition rule over $\Sigma$ is an expression of the form $\frac{H}{\alpha}$ with $H$ a set of $\Sigma$-literals (the premises or antecedents of the rule) and $\alpha$ a positive $\Sigma$-literal (the conclusion). The terms at the left- and right-hand side of $\alpha$ are the source and target of the rule. A rule $\frac{H}{\alpha}$ with $H=\emptyset$ is also written $\alpha$. A literal or transition rule is closed if it contains no free variables. A transition system specification (TSS) is a pair $(\Sigma,R)$ with $\Sigma$ a signature and $R$ a set of transition rules over $\Sigma$; it is positive if all antecedents of its rules are positive.

The concept of a (positive) TSS presented above was introduced in Groote & Vaandrager [40]; the negative premises t{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a\;$\hskip 2.5pt}\hfil}}}}} were added in Groote [37]. The notion generalises the GSOS rule systems of [12] and constitutes the first formalisation of Plotkin’s Structural Operational Semantics (SOS) [47] that is sufficiently general to cover many of its applications.

The following definition (from [28]) tells when a transition is provable from a TSS. It generalises the standard definition (see e.g. [40]) by (also) allowing the derivation of transition rules. The derivation of a transition t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}t^{\prime} corresponds to the derivation of the transition rule $\frac{H}{t\stackrel{{\scriptstyle a}}{{\longrightarrow}}t^{\prime}}$ with $H\mathbin{=}\emptyset$. The case $H\mathbin{\neq}\emptyset$ corresponds to the derivation of t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}t^{\prime} under the assumptions $H$.

Definition 4** **(Proof)

Let $P=(\Sigma,R)$ be a TSS. A proof of a transition rule $\frac{H}{\alpha}$ from $P$ is a well-founded, upwardly branching tree of which the nodes are labelled by $\Sigma$-literals, such that:

• •

the root is labelled by $\alpha$, and

• •

if $\beta$ is the label of a node $q$ and $K$ is the set of labels of the nodes directly above $q$, then

• –

either $K=\emptyset$ and $\beta\in H$,

• –

or $\frac{K}{\beta}$ is a substitution instance of a rule from $R$.

If a proof of $\frac{H}{\alpha}$ from $P$ exists, then $\frac{H}{\alpha}$ is provable from $P$, notation $P\vdash\frac{H}{\alpha}$.

A TSS is meant to specify an LTS in which the transitions are closed positive literals. A positive TSS specifies a transition relation in a straightforward way as the set of all provable transitions.666Readers interested only in the restriction of my results to TSSs without negative premises—giving rise to 2-valued transition relations—can safely skip the remainder of this section, and identify p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} with $p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p^{\prime}$. In the proofs of Prop. 3 and Thm. 2 also p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and $p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\lambda}p^{\prime}$ equal $p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p^{\prime}$, for any $\lambda$; so the induction on $\lambda$ can be skipped, as well as the auxiliary Claims 3 and 1, and the proof proceeds directly by induction on $\pi$. But as pointed out in Groote [37], it is not so easy to associate a transition relation to a TSS with negative premises. In [32] several solutions to this problem were reviewed and evaluated. Arguably, the best method to assign a meaning to all TSSs is the well-founded semantics of Van Gelder, Ross & Schlipf [27], which in general yields a 3-valued transition relation $T:{\sf T}(\Sigma)\times A\times{\sf T}(\Sigma)\rightarrow\{\mbox{\sl present},\mbox{\sl undetermined},\mbox{\sl absent}\}$. I present such a relation as a pair \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!CT,PT\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} of 2-valued transition relations—the sets of certain and possible transitions—with $CT\subseteq PT$. When insisting on 2-valued transition relations, the best method is the same, declaring meaningful only those TSSs whose well-founded semantics is 2-valued, meaning that $CT=PT$.

Below I give a new presentation of the well-founded semantics, strongly inspired by previous accounts in [48, 13, 32]. As Def. 4 does not allow the derivation of negative literals, to arrive at an approximation $AT^{+}$ of the set of transitions that are in the transition relation intended by a TSS $P$, one could start from an approximation $AT^{-}$ of the closed negative literals that ought to be generated, and define $AT^{+}$ as the set of closed positive literals provable from $P$ under the hypotheses $AT^{-}$. Intuitively,

if $AT^{-}$ is an under- (resp. over-)approximation of the closed negative literals that “really” hold, then $AT^{+}$ will be an under- (resp. over-)approximation of the intended (2-valued) transition relation, and 2. 2.

if $AT^{+}$ is an under- (resp. over-)approximation of the intended transition relation, then the set of all closed negative literals that do not deny any literal in $AT^{+}$ is an over- (resp. under-)approximation of the closed negative literals that agree with the intended transition relation.

Definition 5** **(Over- and underappr. of transition relations)

Let $P$ be a TSS. For ordinals $\lambda$ the sets $CT^{+}_{\lambda}$ and $PT^{+}_{\lambda}$ of closed positive literals, and $CT^{-}_{\lambda}$, $PT^{-}_{\lambda}$ of closed negative literals are defined inductively by:

$PT^{-}_{\lambda}$

is the set of literals

that do not deny any

$\beta\in CT^{+}_{\kappa}$ with $\kappa<\lambda$

$\beta\in PT^{+}_{\lambda}$ iff $P\vdash\frac{PT^{-}_{\lambda}}{\beta}$.

$CT^{-}_{\lambda}$

is the set of literals

that do not deny any

$\beta\in PT^{+}_{\lambda}$

$\beta\in CT^{+}_{\lambda}$ iff $P\vdash\frac{CT^{-}_{\lambda}}{\beta}$.

Intuitively, $CT^{+}_{\lambda}$ is an underapproximation of the set of transitions that should be in the transition relation specified by $P$, and $PT^{+}_{\lambda}$ an overapproximation. Likewise, $CT^{-}_{\lambda}$ is an underapproximation of the set of closed negative literals that should hold, and $PT^{-}_{\lambda}$ an overapproximation. The approximations get better with increasing $\lambda$. To understand this inductively, note that $PT^{-}_{0}$ is the set of all closed negative literals, and thus surely an overapproximation. The induction step is given by considerations 1 and 2 above.

Lemma 1

$CT^{-}_{\kappa}\mathbin{\subseteq}CT^{-}_{\lambda}\mathbin{\subseteq}PT^{-}_{\lambda}\mathbin{\subseteq}PT^{-}_{\kappa}$ and $CT^{+}_{\kappa}\mathbin{\subseteq}CT^{+}_{\lambda}\mathbin{\subseteq}PT^{+}_{\lambda}\mathbin{\subseteq}PT^{+}_{\kappa}$ for $\kappa\mathbin{<}\lambda$.

Proof.

Let $\kappa<\lambda$. The definition of $PT_{\lambda}^{-}$ immediately yields $PT^{-}_{\lambda}\mathbin{\subseteq}PT^{-}_{\kappa}$. From this, applying Def. 5, one obtains $PT^{+}_{\lambda}\mathbin{\subseteq}PT^{+}_{\kappa}$, $CT^{-}_{\kappa}\mathbin{\subseteq}CT^{-}_{\lambda}$ and $CT^{+}_{\kappa}\mathbin{\subseteq}CT^{+}_{\lambda}$, respectively. The remaining claims follow by induction on $\lambda$.

As $PT^{-}_{0}$ is the universal relation, certainly $CT^{-}_{0}\mathbin{\subseteq}PT^{-}_{0}$, so $CT^{+}_{0}\mathbin{\subseteq}PT^{+}_{0}$.

Let $\lambda$ be a limit ordinal. Then $PT^{-}_{\lambda}=\bigcap_{\mu<\lambda}PT^{-}_{\mu}$. For any $\kappa,\mu<\lambda$ one has $CT^{-}_{\kappa}\subseteq PT^{-}_{\mu}$ by induction. Namely $CT^{-}_{\kappa}\subseteq CT^{-}_{\mu}\subseteq PT^{-}_{\mu}$ if $\kappa\leq\mu<\lambda$, and $CT^{-}_{\kappa}\subseteq PT^{-}_{\kappa}\subseteq PT^{-}_{\mu}$ if $\mu\leq\kappa<\lambda$. Hence $CT^{-}_{\kappa}\subseteq\bigcap_{\mu<\lambda}PT^{-}_{\mu}=PT^{-}_{\lambda}$ for any $\kappa<\lambda$, and hence $CT^{+}_{\kappa}\subseteq PT^{+}_{\lambda}$. With Def. 5 this implies $CT^{-}_{\lambda}\mathbin{\subseteq}PT^{-}_{\lambda}$ and hence $CT^{+}_{\lambda}\mathbin{\subseteq}PT^{+}_{\lambda}$.

Now let $\lambda=\mu{+}1$. By induction $CT^{+}_{\mu}\mathbin{\subseteq}PT^{+}_{\mu}$. With Def. 5 this implies $CT^{-}_{\mu}\mathbin{\subseteq}PT^{-}_{\lambda}$, and hence $CT^{+}_{\mu}\subseteq PT^{+}_{\lambda}$. With Def. 5 this implies $CT^{-}_{\lambda}\mathbin{\subseteq}PT^{-}_{\lambda}$ and hence $CT^{+}_{\lambda}\mathbin{\subseteq}PT^{+}_{\lambda}$. ∎∎

Since the closed literals over $\Sigma$ form a proper set, there must be an ordinal $\kappa$ such that $PT^{-}_{\lambda}\mathbin{=}PT^{-}_{\kappa}$ for all $\lambda\mathbin{>}\kappa$, and hence also $PT^{+}_{\lambda}\mathbin{=}PT^{+}_{\kappa}$, $CT^{-}_{\lambda}\mathbin{=}CT^{-}_{\kappa}$ and $CT^{+}_{\lambda}\mathbin{=}CT^{+}_{\kappa}$.

Definition 6

Such an ordinal $\kappa$ is called closure ordinal. Let $PT^{-}\mathbin{:=}PT^{-}_{\kappa}$, $PT^{+}\mathbin{:=}PT^{+}_{\kappa}$, $CT^{-}\mathbin{:=}CT^{-}_{\kappa}$ and $CT^{+}\mathbin{:=}CT^{+}_{\kappa}$.

Remark 1

$PT^{-}\mathbin{=}\bigcap_{\lambda}PT^{-}_{\lambda}$, taking the intersection over all ordinals. Likewise, $PT^{+}\mathbin{=}\bigcap_{\lambda}PT^{+}_{\lambda}$, $CT^{-}\mathbin{=}\bigcup_{\lambda}CT^{-}_{\lambda}$ and $CT^{+}=\bigcup_{\lambda}CT^{+}_{\lambda}$.

Remark 2

$PT^{-}$ is the set of literals that do not deny any literal in $CT^{+}$, and likewise for $CT^{-}$ and $PT^{+}$. Moreover, $CT^{-}\subseteq PT^{-}$ and $CT^{+}\subseteq PT^{+}$.

Definition 7** **(Well-founded semantics)

The 3-valued transition relation \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!CT^{+}\!,PT^{+}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} constitutes the well-founded semantics of $P$.

Below I show that the above account of the well-founded semantics is consistent with the one in [32], and thereby with the ones in [13, 48, 27].

Definition 8** **(Well-supported proof [32])

Let $P=(\Sigma,R)$ be a TSS. A well-supported proof from $P$ of a closed literal ${\alpha}$ is a well-founded tree with the nodes labelled by closed literals, such that the root is labelled by $\alpha$, and if $\beta$ is the label of a node and $K$ is the set of labels of the children of this node, then:

• •

either $\beta$ is positive and $\frac{K}{\beta}$ is a substitution instance of a rule in $R$;

• •

or $\beta$ is negative and for each set $N$ of closed negative literals with $P\vdash\frac{N}{\gamma}$ for $\gamma$ a closed positive literal denying $\beta$, a literal in $K$ denies one in $N$.

$P\vdash_{\it ws}\alpha$ denotes that a well-supported proof from $P$ of $\alpha$ exists.

Proposition 1

Let $P$ be a TSS. Then P\vdash_{\it ws}p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q iff (p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q)\in CT^{+}, and P\vdash_{\it ws}p{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a\;$\hskip 2.5pt}\hfil}}}}} iff (p{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a\;$\hskip 2.5pt}\hfil}}}}})\in CT^{-}.

Proof.

$\Rightarrow$: Let $\pi$ be a well-supported proof of a closed literal $\alpha$. By consistently applying the same closed substitution to all literals occurring in $\pi$, one can assume, without loss of generality, that all literals in $\pi$ are closed. With structural induction on $\pi$ I show that $\alpha\in CT^{+}\cup CT^{-}$.

Suppose $\alpha$ is positive and $\frac{K}{\alpha}$ is the closed substitution instance of the rule of $P$ applied at the root of $\pi$. Then for each $\beta\in K$ the literal $\beta$ is ws-provable from $P$ by means of a strict subproof of $\pi$. By induction $\beta\in CT^{+}\cup CT^{-}$. As $CT^{+}$ is $CT^{+}_{\kappa}$ for some ordinal $\kappa$, it is closed under deduction. Hence $\alpha\in CT^{+}$.

Suppose $\alpha$ is negative. Let $\beta$ be closed positive literal denying $\alpha$. By Def. 8, each set $N$ of closed negative literals with $P\vdash\beta$ contains a literal $\gamma_{N}$ denying a literal $\delta_{N}$ that is ws-provable from $P$ by means of a strict subproof of $\pi$. By induction $\delta_{N}\mathbin{\in}CT^{+}$. Hence $\gamma_{N}\mathbin{\notin}PT^{-}$. Consequently $\beta\mathbin{\notin}PT^{+}$. Hence $\alpha\mathbin{\in}CT^{-}$.

$\Leftarrow$: Suppose $\alpha\in CT_{\lambda}^{+}\cup CT^{-}_{\lambda}$. With induction on $\lambda$ I show that $P\vdash_{\it ws}\alpha$. First suppose $\alpha\in CT_{\lambda}^{-}$. Let $N$ be a set of closed negative literals with $P\vdash\frac{N}{\gamma}$ for $\gamma$ a closed positive literal denying $\alpha$. Assume that $N\subseteq PT^{-}_{\lambda}$. Then $\gamma$ would be in $PT^{+}_{\lambda}$, contradicting the definition of $CT^{-}_{\lambda}$. So $N$ contains a literal that is not in $PT^{-}_{\lambda}$, i.e., denies a literal $\delta_{N}$ in $CT^{+}_{\kappa}$ for some $\kappa<\lambda$. By induction, $P\vdash_{\it ws}\delta_{N}$. It follows that $P\vdash_{\it ws}\alpha$.

Now suppose $\alpha\in CT_{\lambda}^{+}$. Then $P\vdash\frac{CT^{-}_{\lambda}}{\alpha}$. By the case above $P\vdash_{\it ws}\beta$ for each $\beta\in CT^{-}_{\lambda}$. Hence $P\vdash_{\it ws}\alpha$. ∎∎

The above result, together with Theorem 1 in [32], and the observation in [32] that literals t\mathrel{{\mathrel{\hbox{\mathop{\hbox to30.41106pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle missing\;$\hskip 2.5pt}}}}}}{a}t^{\prime} can be eliminated from consideration (as done here), implies that the well-founded semantics given above agrees with the one from [32].

In [32] it was shown that $\vdash_{\it ws}$ is consistent, in the sense that no TSS admits well-supported proofs of two literals that deny each other. This also follows directly from the material above. A TSS $P$ is called complete [32] if for each $p$ and $a$, either P\vdash_{\it ws}p{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a\;$\hskip 2.5pt}\hfil}}}}} or P\vdash_{\it ws}p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q for some $q$. This implies that $CT^{-}$ is exactly the set of closed negative literals that do not deny any literal in $CT^{+}$. Hence $CT^{-}=PT^{-}$ and thus $CT^{+}=PT^{+}$. So the 3-valued transition system associated to a complete TSS is 2-valued.

Below I write $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\lambda}q$ for $(p\mathbin{\stackrel{{\scriptstyle a}}{{\longrightarrow}}}q)\mathbin{\in}CT^{+}_{\lambda}$, P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda} for (p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}})\mathbin{\in}CT^{-}_{\lambda}, P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q for $(p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q)\in PT^{+}_{\lambda}$ and P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}_{\lambda} for (p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}})\in PT^{-}_{\lambda}. Moreover, $p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q$, resp. p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q, will abbreviate $p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\kappa}q$, resp. p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\kappa}q, where $\kappa$ is the closure ordinal of Def. 6.

In my forthcoming lean congruence proof I will apply structural induction on “the proof of a transition $p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\lambda}q$ or p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q from $P$”. There I will mean the proofs of $\frac{CT^{-}_{\lambda}}{p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q}$ and $\frac{PT^{-}_{\lambda}}{p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q}$, respectively, as this is what constitutes the evidence for the statement P\vdash p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}_{\lambda}q, resp. P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q.

III The bisimulation preorder

The goal of this paper is to show that bisimilarity is a congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Traditionally [45], bisimilarity is defined on 2-valued transition systems only, whereas the structural operational semantics of a language specified by a TSS can be 3-valued. Rather than limit my results to languages specified by complete TSSs, I use an extension of the notion of bisimilarity to 3-valued transition systems. Such an extension, called modal refinement, is provided in [43]. There, 3-valued transition systems are called modal transition systems.

Definition 9** **(Bisimilarity)

Let $P$ be a TSS. A bisimulation $\mathrel{\cal R}$ is a binary relation on the states of ${\rm T}(\Sigma)$ such that, for $p,q\in{\rm T}(\Sigma)$ and $a\in A$,

• •

if $p\mathrel{\cal R}q$ and $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p^{\prime}$, then there is a $q^{\prime}$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$ and $p^{\prime}\mathrel{\cal R}q^{\prime}$,

• •

if $p\mathrel{\cal R}q$ and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a $p^{\prime}$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and $p^{\prime}\mathrel{\cal R}q^{\prime}$.

A process $q\mathbin{\in}{\rm T}(\Sigma)$ is a modal refinement of $p\mathbin{\in}{\rm T}(\Sigma)$, notation $p\sqsubseteq_{B}q$, if there exists a bisimulation $\mathrel{\cal R}$ with $p\mathrel{\cal R}q$. I call $\sqsubseteq_{B}$ the bisimulation preorder, or bisimilarity. The kernel of $\sqsubseteq$, given by ${\equiv_{B}}:={\sqsubseteq_{B}}\cap{\sqsupseteq_{B}}$, is bisimulation equivalence.

Clearly, modal refinement is reflexive and transitive, and hence a preorder. The underlying idea is that a process $p$ with a 3-valued transition relation \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!CT,PT\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is a specification of a process with a 2-valued transition relation, in which the presence or absence of certain transitions is left open. $CT$ contains the transitions that are required by the specification, and $PT$ the ones that are allowed. If $p\sqsubseteq_{B}q$, then $q$ may be closer to the eventual implementation, in the sense that some of the undetermined transitions have been resolved to present or absent. The requirements of Def. 9 now say that any transition that is required by $p$ should be (matched by a transition) required by $q$, whereas any transition allowed by $q$, should certainly be (matched by a transition) allowed by $p$.

In case $p$ and $q$ are 2-valued (i.e. implementations) the modal refinement relation is just the traditional notion of bisimilarity [45] (and thus symmetric).

While achieving a higher degree of generality of my lean congruence theorem by interpreting incomplete TSSs as modal transition systems, I do not propose incomplete TSSs as a tool for the specification of modal transition systems.

IV Congruence properties

In the presence of recursion, two sensible notions of precongruence come to mind. Let $\sqsubseteq$ be a preorder on the set ${\rm T}(\Sigma)$ of closed terms over $\Sigma$. For $\rho,\nu\!:\!{\it Var}\rightarrow{\rm T}(\Sigma)$ closed substitutions write $\rho\mathbin{\sqsubseteq}\nu$ iff $\rho(x)\mathbin{\sqsubseteq}\nu(x)$ for each $x\mathbin{\in}{\it Var}$.

Definition 10** **(Lean precongruence)

A preorder ${\sqsubseteq}\subseteq{\rm T}(\Sigma)\linebreak\times{\rm T}(\Sigma)$ is a lean precongruence iff $t[\rho]\sqsubseteq t[\nu]$ for any term $t\in\mbox{\bbb T}(\Sigma)$ and any closed substitutions $\rho$ and $\nu$ with $\rho\sqsubseteq\nu$.

Definition 11** **(Full precongruence)

A preorder ${\sqsubseteq}\mathbin{\subseteq}{\rm T}(\Sigma)\times{\rm T}(\Sigma)$ is a full precongruence iff it satisfies

[TABLE]

[TABLE]

for all functions $(f,n)\in\Sigma$, closed terms $p_{i},q_{i}\in{\rm T}(\Sigma)$, and recursive specifications $S,S^{\prime}:W\rightarrow\mbox{\bbb T}(\Sigma,W)$ with $X\in W\subseteq{\it Var}$.

A lean (resp. full) precongruence that is symmetric (i.e. an equivalence relation) is called a lean (resp. full) congruence. Clearly, each full (pre)congruence is also a lean (pre)congruence, and each lean (pre)congruence satisfies (1) above. Both implications are strict, as the following examples illustrate.

Example 3

Consider the TSS given by the rules

[TABLE]

where $a$ ranges over $A$, and the recursion rule from Def. 13 below. An infinite trace of a process $p$ is a sequence $a_{1}a_{2}\dots\in A^{\omega}$ such that there are processes $p_{1},p_{2},\dots$ with $p\stackrel{{\scriptstyle a_{1}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle a_{2}}}{{\longrightarrow}}p_{2}\stackrel{{\scriptstyle a_{3}}}{{\longrightarrow}}\dots$. Let $p\sqsubseteq q$ iff for each infinite trace $\sigma$ of $p$ there is an infinite trace of $q$ that has a suffix in common with $\sigma$. This is a preorder indeed. It is not hard to check that $\sqsubseteq$ is a precongruence for both action prefixing $a.\_\!\!\_\,$ and parallel composition $\_\!\!\_\|\_\!\!\_\,$, in the sense that (1) holds. However, it fails to be a lean congruence, because a.\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|X{=}c.X!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\equiv b.\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|X{=}c.X!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}, yet when filled in for $Y$ in \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Z|Z{=}Y\|Z\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} (which can be seen as $!Y$, an infinite parallel composition of copies of $Y$) the two are no longer equivalent.

I did not find a pair of a TSS and a preorder known from the literature showing the same. This suggests that most common preorders that are (pre)congruences for a selection of common operators are also lean (pre)congruences for recursion.

Example 4

Consider the TSS with a constant ${\bf 0}$ and action prefixing, and only the rules for recursion from Def. 13 and $a.x\stackrel{{\scriptstyle a}}{{\longrightarrow}}x$ for $a\in A$, with $\tau\in A$ the internal action. Consider any semantic equivalence $\sim$ satisfying $x\sim\tau.x$, and such that divergence \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|X{=}\tau.X\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} differs from deadlock or inaction ${\bf 0}$. Such semantic equivalences are abound in the literature and include the failures semantics of CSP [15, 29] and branching bisimilarity with explicit divergence [35, 29]. They are all lean congruences (at least when no other operators are present). Yet, since 0\sim\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|X{=}X!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\not\sim\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|X{=}\tau.X!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}, they fail to be full congruences.

A lean congruence is required for treating processes as equivalence classes of closed terms rather than as the closed terms themselves, in such a way that each term $t\mathbin{\in}\mbox{\bbb T}(\Sigma,W)$ with free variables drawn from the set $W$ models a $W$-ary operator on such processes. As explained in the introduction, this notion of congruence facilitates a formal comparison of the expressive power of system description languages [34]. However, it does not allow equivalence preserving modifications of recursive specifications themselves, as contemplated in the introduction. That requires a full congruence.

V The pure ntyxt/ntyft format with recursion

Definition 12** **(ntytt, ntyft, ntyxt, nxytt rules)

An ntytt rule is a rule in which the right-hand sides of positive premises are variables that are all distinct, and that do not occur in the source. An ntytt rule is an ntyxt rule if its source is a variable, an ntyft rule if its source contains exactly one function symbol and no multiple occurrences of variables, and an nxytt rule if the left-hand sides of its premises are variables.

The idea behind the names of the rules is that the ‘n’ in front refers to the presence of negative premises, and the following four letters refer to the allowed forms of left- and right-hand sides of premises and of the conclusion, respectively. For example, ntyft means a rule with negative premises (n), where left-hand sides of premises are general terms (t), right-hand sides of positive premises are variables (y), the source contains exactly one function symbol (f), and the target is a general term (t).

Definition 13

A TSS is in the ntyft/ntyxt format with recursion if for every recursive specification $S$ and $X\in V_{S}$ it has a rule

[TABLE]

and all of its other rules are ntyft or ntyxt rules.

Definition 14** **(Well-founded and pure rules; distance)

The dependency graph of an ntytt rule with \{t_{i}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a_{i}$\hskip 2.5pt}\hfil}}}}}y_{i}\mid i\mathbin{\in}I\} as set of positive premises is the directed graph with edges $\{\langle x,y_{i}\rangle\mid x\mathbin{\in}{\it var}(t_{i})\mbox{ for some }i\mathbin{\in}I\}$. A ntytt rule is well-founded if each backward chain of edges in its dependency graph is finite. A variable in a rule is free if it occurs neither in the source nor in the right-hand sides of the premises of this rule. A rule is pure if it is well-founded and does not contain free variables. A TSS is well-founded, resp. pure, if all of its rules are.

Let $r\mathbin{=}\frac{H}{t\stackrel{{\scriptstyle a}}{{\longrightarrow}}u}$ be a pure ntytt rule. The distance of a variable $y\in{\it var}(r)$ to the source of $r$ is the ordinal number given by

[TABLE]

Bol & Groote show that bisimilarity is a congruence for any language specified by a complete TSS in the well-founded ntyft/ntyxt format (without recursion) [13]. This generalises a result by Groote [37], showing the same for stratified TSSs in the well-founded ntyft/ntyxt format; here stratified is a more restrictive criterion than completeness, guaranteeing that a TSS has a well-defined meaning as a 2-valued transition relation. That result, in turn, generalises the congruence formats of Groote & Vaandrager [40] for the well-founded tyft/tyxt format (obtained by leaving out negative premises) and for the GSOS format of Bloom, Istrail & Meyer [12]. Both of these generalise the De Simone format [49, 50].

Fokkink and van Glabbeek show that for any complete TSS in tyft/tyxt (resp. ntyft/ntyxt) format there exists a pure (and thus well-founded) complete TSS in tyft (resp. ntyft) format that generates the same transition relation [20]. From this it follows that the restriction to well-founded TSSs can be dropped from the congruence formats of [13] and [40]. The result of [20] generalises straightforwardly to incomplete TSSs, and to formats with recursion.

Theorem 1

For each TSS in the tyft/tyxt (resp. ntyft/ntyxt) format with recursion there exists a pure TSS in the tyft (resp. ntyft) format with recursion, generating the same (3-valued) transition relation.

Proof.

[20, Theorem 5.4] shows that for each TSS $P$ in ntyft/ntyxt format there exists a TSS $P^{\prime}$ in pure ntyft format, such that for any closed transition rule $\frac{N}{\alpha}$ with only negative premises, one has $P\vdash\frac{N}{\alpha}\Leftrightarrow P^{\prime}\vdash\frac{N}{\alpha}$. This result generalises seamlessly to TSS in the ntyft/ntyxt format with recursion; I leave it to the reader to check that recursion causes no new complications in the proof.

[20] obtains the quoted result for complete TSSs from Thm. 5.4 by means of an application of [20, Prop. 5.2], which says that if $P$ and $P^{\prime}$ are TSSs such that $P\vdash\frac{N}{\alpha}\Leftrightarrow P^{\prime}\vdash\frac{N}{\alpha}$ for any closed transition rule $\frac{N}{\alpha}$ with only negative premises, then $P$ is complete iff $P^{\prime}$ is, and in that case they determine the same transition relation. This Prop. 5.2 was taken verbatim from [31, Prop. 29].

In [32], the journal version of [31], Prop. 29 was extended to also conclude, under the same assumption, that $P$ and $P^{\prime}$ determine the same 3-valued transition relation according to the well-founded semantics. Using this version of Prop. 29 instead of Prop. 5.2 yields the required result. ∎∎

The next two propositions (not used in the rest of the paper) tell that any language specified by TSS in the ntyft/ntyxt format with recursion satisfies two sanity requirements from [30]. The first is that, up to $\equiv_{B}$, the meaning of a closed term \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is the $X$-component of a solution of $S$:

Proposition 2

Let $P\mathbin{=}(\Sigma,R)$ be a TSS in the ntyft/ntyxt format with recursion and $S$ a recursive specification with $X\mathbin{\in}V_{S}$. Then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\equiv_{B}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}.

Proof.

P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q for some $a\in A$ and $q\in{\rm T}(\Sigma)$ iff P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q. ∎∎

For the second, invariance under $\alpha$-conversion, write t\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}u if the terms $t,u\in\mbox{\bbb T}(\Sigma)$ differ only in the names of their bound variables (the variables from $V_{S}$ within a subexpression of the form \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}).

Proposition 3

Let $P=(\Sigma,R)$ be a TSS in the ntyft/ntyxt format with recursion. Then p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q\Rightarrow p\equiv_{B}q for all $p,q\in{\rm T}(\Sigma)$.

Proof.

By Thm. 1 I may assume, without loss of generality, that $P$ is in the pure ntyft format with recursion. I show that \mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}} is a bisimulation on ${\rm T}(\Sigma)$—since \mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}} is also symmetric, this yields the required result.

Thus I need to show that, for $p,q\in{\rm T}(\Sigma)$ and $a\in A$,

• •

if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p^{\prime}$, then there is a $q^{\prime}$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$ and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime},

• •

if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a $p^{\prime}$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}.

To this end it suffices to establish, for all ordinals $\lambda$, that

if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\lambda}p^{\prime}$, then there is a $q^{\prime}$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$ and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}, 2. 2.

if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a $p^{\prime}$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}.

The desired result is then obtained by taking $\lambda$ to be the closure ordinal $\kappa$ of Def. 6. This I will do by induction on $\lambda$, at the same time establishing that

if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}, then P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}, 2. 1.

if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}, then P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}_{\lambda}.

So assume Claims 1–4 have been established for all $\kappa<\lambda$.

Suppose p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}. By Remark 2 there is no $q^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$. So by induction, using Claim 4 above, there is no $p^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\kappa}p^{\prime}$ for some $\kappa<\lambda$. By Def. 5 P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}_{\lambda}. This yields Claim 1.

Now suppose p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. I need to find a $p^{\prime}$ with P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}. This I will do by structural induction on the proof $\pi$ of p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} from $P$, making a case distinction based on the shape of $p$.

• •

Let $p=f(p_{1},\ldots,p_{n})$. Then $q=f(q_{1},\ldots,q_{n})$ where p_{i}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q_{i} for $i\mathbin{=}1,\ldots,n$. Let $\pi$ be a proof of P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from $P$. By Defs. 4 and 13, there must be a pure ntyft rule $r=\frac{H}{f(x_{1},...,x_{n})\stackrel{{\scriptstyle a}}{{\longrightarrow}}t}$ in $R$ and a closed substitution $\nu$ with $\nu(x_{i})\mathbin{=}q_{i}$ for $i\mathbin{=}1,...,n$ and $t[\nu]\mathbin{=}q^{\prime}$, such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H the transition P\vdash t_{y}[\nu]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}\nu(y) is provable from $P$ by means of a strict subproof of $\pi$, and P\vdash u[\nu]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}} for each (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}})\in H. Next, I define a substitution $\sigma:{\it var}(r)\rightarrow{\rm T}(\Sigma)$ such that

1. (i)

$\sigma(x_{i})=p_{i}$ for $i=1,\ldots,n$, 2. (ii)

\sigma(y)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(y) for each $y\mathbin{\in}{\it var}(r)$, 3. (iii)

P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}\sigma(y) for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H.

The definition of $\sigma(y)$ and the inference of (i)–(iii) above proceed with induction on the distance of $y\mathbin{\in}{\it var}(r)$ from the source of $r$,

Base case: Let $\sigma(x_{i}):=p_{i}$ for $i=1,\ldots,n$, so that Property (i) is satisfied. Regarding Property (ii), \sigma(x_{i})\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(x_{i}) for $i=1,\ldots,n$.

Induction step: When defining $\sigma(y)$ for some $y\mathbin{\in}{\it Var}$ with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H, by induction $\sigma(x)$ has been defined already for all $x\mathbin{\in}{\it var}(t_{y})$, so I may assume that \sigma(x)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(x) for all $x\mathbin{\in}{\it var}(t_{y})$ and hence t_{y}[\sigma]\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}t_{y}[\nu].

By induction on $\pi$, there is a $p_{y}$ with P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p_{y} and p_{y}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(y). Define $\sigma(y):=p_{y}$. Properties (ii) and (iii) now hold for $y$.

Take $p^{\prime}:=t[\sigma]$. So p^{\prime}\mathbin{=}t[\sigma]\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}t[\nu]\mathbin{=}q^{\prime} by Property (ii) of $\sigma$. For each premise (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}})\in H one has u[\sigma]\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}u[\nu] by Property (ii) of $\sigma$. So P\vdash u[\sigma]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}_{\lambda} by Claim 1. By Defs. 4 and 13, together with Property (iii) of $\sigma$, this implies P\vdash p=f(p_{1},\ldots,p_{n})\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}t[\sigma]=p^{\prime}.

• •

Let p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}. Then q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!\alpha(X)|S^{\prime}[\alpha]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} for some recursive specification $S^{\prime}:V_{S}\rightarrow\mbox{\bbb T}(\Sigma)$ with S_{Y}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}S^{\prime}_{Y} for all $Y\in V_{S}$, and an injective substitution $\alpha:V_{S}\rightarrow{\it Var}$ such that the range of $\alpha$ contains no variables occurring free in \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S^{\prime}_{Y}|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} for some $Y\in V_{S}$. Now \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S^{\prime}{\alpha(X)}|S^{\prime}[\alpha]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}. Let $\pi$ be a proof of P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from $P$. By Defs. 4 and 13 P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S^{\prime}{\alpha(X)}|S^{\prime}[\alpha]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} is provable from $P$ by means of a strict subproof of $\pi$. So by induction there is a $p^{\prime}$ such that P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}. By Defs. 4 and 13, P\vdash p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}.

This establishes Claim 2.

Next, suppose that p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}. By Def. 5 there is no $p^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}. Using Claim 2, there is no $q^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. By Remark 2, P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}. This yields Claim 3.

Claim 4 follows by structural induction on the proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from $P$, pretty much in the same way as Claim 2 above. ∎∎

Prop. 3 could be classified as “self-evident”. One reason to spell out the proof above is to obtain a template for bisimilarity proofs in the setting of the well-founded semantics. I will use this template in the forthcoming lean congruence proof.

VI A lean congruence result

The following congruence proof is strongly inspired by the one in [13].

Theorem 2

Bisimilarity is a lean precongruence for any language specified by a TSS in the ntyft/ntyxt format with recursion.

• Proof:

By Thm. 1 I may assume, without loss of generality, that $P=(\Sigma,R)$ is a TSS in the pure ntyft format with recursion. Let $\mathrel{\cal R}$ be the smallest lean precongruence containing bisimilarity, i.e., $\mathord{\mathrel{\cal R}}\subseteq{\rm T}(\Sigma)\times{\rm T}(\Sigma)$ is the smallest relation on processes satisfying

• –

if $p\sqsubseteq_{B}q$ then $p\mathrel{\cal R}q$,

• –

if $(f,n)\mathbin{\in}\Sigma$ and $p_{i}\mathbin{\mathrel{\cal R}}q_{i}$ for all $i\mathbin{=}1,...,n$, then $f(p_{1},\ldots,p_{n})\mathrel{\cal R}f(q_{1},\ldots,q_{n})$,

• –

and if $S:V_{S}\rightarrow\mbox{\bbb T}(\Sigma)$ with $Z\in V_{S}\subseteq{\it Var}$, and $\rho,\nu:{\it Var}\setminus V_{S}\rightarrow{\rm T}(\Sigma)$ satisfy $\rho(x)\mathrel{\cal R}\nu(x)$ for all $x\mathbin{\in}{\it Var}\setminus V_{S}$, then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\nu].

**A trivial structural induction on $t\mathbin{\in}\mbox{\bbb T}(\Sigma)$, using the last two clauses, shows that if $\rho,\nu\!:\!{\it Var}\mathbin{\rightarrow}{\rm T}(\Sigma)$ satisfy $\rho(x)\mathbin{\mathrel{\cal R}}\nu(x)$ for all $x\mathbin{\in}{\it var}(t)$, then $t[\rho]\mathrel{\cal R}t[\nu]$. (*)

As \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!_|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\rho]:V_{S}\rightarrow{\rm T}(\Sigma) and \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!_|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\nu]:V_{S}\rightarrow{\rm T}(\Sigma), this implies that in the last clause one even has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\nu] for all terms $t\in\mbox{\bbb T}(\Sigma,V_{S})$. ($)**

It suffices to show that $\mathrel{\cal R}$ is a bisimulation, because this implies ${\mathrel{\cal R}}\subseteq{\sqsubseteq_{B}}$, so that $\mathrel{\cal R}$ equals $\sqsubseteq_{B}$, and (*) says that $\mathrel{\cal R}$ is a lean precongruence. Thus I need to show that, for $p,q\in{\rm T}(\Sigma)$ and $a\in A$,

• –

if $p\mathrel{\cal R}q$ and $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p^{\prime}$, then there is a $q^{\prime}$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$ and p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime},

• –

if $p\mathrel{\cal R}q$ and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a $p^{\prime}$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and p^{\prime}\mathrel{\color[rgb]{1,0,0}\mathrel{\cal R}}q^{\prime}.

To this end it suffices to establish, for all ordinals $\lambda$, that

if $p\mathrel{\cal R}q$ and $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\lambda}p^{\prime}$, then there is a $q^{\prime}$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$ and p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime},** ** 2. 2.

if $p\mathrel{\cal R}q$ and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a $p^{\prime}$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and p^{\prime}\mathrel{\color[rgb]{1,0,0}\mathrel{\cal R}}q^{\prime}.

The desired result is then obtained by taking $\lambda$ to be the closure ordinal $\kappa$ of Def. 6. This I will do by induction on $\lambda$, at the same time establishing that

if $p\mathrel{\cal R}q$ and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}, then P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}, 2. 1.

if $p\mathrel{\cal R}q$ and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}, then P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}_{\lambda}.

So assume Claims 1–4 have been established for all $\kappa<\lambda$.

Suppose $p\mathrel{\cal R}q$ and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}. By Remark 2 there is no $q^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$. So by induction, using Claim 4 above, there is no $p^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\kappa}p^{\prime}$ for some $\kappa<\lambda$. By Def. 5 P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}_{\lambda}. This yields Claim 1.

Now suppose $p\mathrel{\cal R}q$ and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. I need to find a $p^{\prime}$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and $p^{\prime}\mathrel{\cal R}q^{\prime}$. This I will do by structural induction on the proof $\pi$ of q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from $P$. I make a case distinction based on the derivation of $p\mathrel{\cal R}q$.

• –

Let $p\sqsubseteq_{B}q$. Using that $\sqsubseteq_{B}$ is a bisimulation, there must be a process $p^{\prime}$ such that P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and $p^{\prime}\sqsubseteq_{B}q^{\prime}$, hence $p^{\prime}\mathrel{\cal R}q^{\prime}$. Since P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime}, certainly P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}, by Remark 1.

• –

Let $p=f(p_{1},\ldots,p_{n})$ and $q=f(q_{1},\ldots,q_{n})$ where $p_{i}\mathrel{\cal R}q_{i}$ for $i=1,\ldots,n$. Let $\pi$ be a proof of q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from $P$. By Defs. 4 and 13, there must be a pure ntyft rule $r=\frac{H}{f(x_{1},...,x_{n})\stackrel{{\scriptstyle a}}{{\longrightarrow}}t}$ in $R$ and a closed substitution $\nu$ with $\nu(x_{i})\mathbin{=}q_{i}$ for $i\mathbin{=}1,...,n$ and $t[\nu]\mathbin{=}q^{\prime}$, such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H the transition t_{y}[\nu]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}\nu(y) is provable from $P$ by means of a strict subproof of $\pi$, and P\vdash u[\nu]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}} for each (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}})\in H. Next, I define a substitution $\sigma:{\it var}(r)\rightarrow{\rm T}(\Sigma)$ such that

1. (i)

$\sigma(x_{i})=p_{i}$** for $i=1,\ldots,n$,** 2. (ii)

$\sigma(y)\mathrel{\cal R}\nu(y)$** for each $y\mathbin{\in}{\it var}(r)$,** 3. (iii)

P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}\sigma(y)** for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H.**

The definition of $\sigma(y)$ and the inference of (i)–(iii) above proceed with induction on the distance of $y\mathbin{\in}{\it var}(r)$ from the source of $r$,

Base case:** Let $\sigma(x_{i}):=p_{i}$ for $i=1,\ldots,n$, so that Property (i) is satisfied. Regarding Property (ii), $\sigma(x_{i})\mathrel{\cal R}\nu(x_{i})$ for $i=1,\ldots,n$.**

Induction step:** When defining $\sigma(y)$ for some $y\mathbin{\in}{\it Var}$ with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H, by induction $\sigma(x)$ has been defined already for all $x\mathbin{\in}{\it var}(t_{y})$, so I may assume that $\sigma(x)\mathrel{\cal R}\nu(x)$ for all $x\mathbin{\in}{\it var}(t_{y})$ and hence $t_{y}[\sigma]\mathrel{\cal R}t_{y}[\nu]$ by (*******).

By induction on $\pi$, there is a $p_{y}$ with P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p_{y} and $p_{y}\mathrel{\cal R}\nu(y)$. Define $\sigma(y):=p_{y}$. Properties (ii) and (iii) now hold for $y$.

Take $p^{\prime}:=t[\sigma]$. So $p^{\prime}\mathbin{=}t[\sigma]\mathrel{\cal R}t[\nu]\mathbin{=}q^{\prime}$ by (***) and Property (ii) of $\sigma$. For each premise (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}})\in H one has $u[\sigma]\mathrel{\cal R}u[\nu]$ by (*******) and Property (ii) of $\sigma$. So P\vdash u[\sigma]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}_{\lambda} by Claim 1. By Defs. 4 and 13, together with Property (iii) of $\sigma$, this implies

P\vdash p=f(p_{1},\ldots,p_{n})\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}t[\sigma]=p^{\prime}****.

• –

Let p\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\rho]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S[\rho]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} and q\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\sigma]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S[\sigma]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} where $S:V_{S}\rightarrow\mbox{\bbb T}(\Sigma)$ with $Z\in V_{S}\subseteq{\it Var}$, $\rho,\sigma\!:{\it Var}{\setminus}V_{S}\mathbin{\rightarrow}{\rm T}(\Sigma)$, and for all $x\in{\it Var}\setminus V_{S}$ one has $\rho(x)\mathrel{\cal R}\sigma(x)$. Let $\pi$ be a proof of q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from $P$. By Defs. 4 and 13 \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{Z}|S[\sigma]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} is provable from $P$ by means of a strict subproof of $\pi$. By ($) above one has **$\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\rho]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\sigma]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}$**. So by induction there is a **$p^{\prime}$** such that ****$P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\rho]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}{\lambda}p^{\prime}$**** and **$p^{\prime}\mathrel{\cal R}q^{\prime}$**. By Defs. ****4**** and ****13****, **$P\vdash p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Z|S[\sigma]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{$\scriptstyle--\rightarrow$}}}}{\lambda}p^{\prime}$.**

Next, suppose that $p\mathrel{\cal R}q$ and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}. By Def. 5 there is no $p^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}. Using Claim 2, there is no $q^{\prime}\mathbin{\in}{\rm T}(\Sigma)$ with P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. By Remark 2, P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}. This yields Claim 3.

Finally, suppose $p\mathrel{\cal R}q$ and $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\lambda}p^{\prime}$. I need to find a $q^{\prime}$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$ and p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime}. This I will do by structural induction on the proof $\pi$ of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from $P$. I make a case distinction based on the derivation of $p\mathrel{\cal R}q$.

• –

Let $p\sqsubseteq_{B}q$. Since $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\lambda}p^{\prime}$, certainly $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p^{\prime}$, by Remark 1. Using that $\sqsubseteq_{B}$ is a bisimulation, there must be a process $q^{\prime}$ such that P\vdash q\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q^{\prime} and $p^{\prime}\sqsubseteq_{B}q^{\prime}$, hence p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime}.

• –

Let $p\mathbin{=}f(p_{1},\ldots,p_{n})$ and $q\mathbin{=}f(q_{1},\ldots,q_{n})$ where $p_{i}\mathrel{\cal R}q_{i}$ for $i=1,\ldots,n$. Let $\pi$ be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from $P$. By Defs. 4, 5 and 13, there must be a pure ntyft rule $r=\frac{H}{f(x_{1},...,x_{n})\stackrel{{\scriptstyle a}}{{\longrightarrow}}t}$ in $R$ and a closed substitution $\sigma$ with $\sigma(x_{i})\mathbin{=}p_{i}$ for $i\mathbin{=}1,...,n$ and $t[\sigma]\mathbin{=}p^{\prime}$, such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H the transition t_{y}[\sigma]\mathbin{\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}_{\lambda}}\sigma(y) is provable from $P$ by means of a strict subproof of $\pi$, and P\vdash u[\sigma]{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}}_{\lambda} for each (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}})\in H. Next, I define a substitution $\nu\!:\!{\it var}(r)\mathbin{\rightarrow}{\rm T}(\Sigma)$ such that

1. (i)

$\nu(x_{i})=q_{i}$** for $i=1,\ldots,n$,** 2. (ii)

\sigma(y)\mathrel{\color[rgb]{0,0,1}\cal R}\nu(y)** for each $y\mathbin{\in}{\it var}(r)$,** 3. (iii)

P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}\nu(y)** for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H.**

The definition of $\nu(y)$ and the inference of (i)–(iii) above proceed with induction on the distance of $y\mathbin{\in}{\it var}(r)$ from the source of $r$,

Base case:** Let $\nu(x_{i}):=q_{i}$ for $i=1,\ldots,n$, so that Property (i) is satisfied. Regarding Property (ii), $\sigma(x_{i})\mathrel{\cal R}\nu(x_{i})$ for $i=1,\ldots,n$.**

Induction step:** When defining $\nu(y)$ for some $y\mathbin{\in}{\it Var}$ with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H, by induction $\nu(x)$ has been defined already for all $x\mathbin{\in}{\it var}(t_{y})$, so I may assume that \sigma(x)\mathrel{\color[rgb]{0,0,1}\cal R}\nu(x) for all $x\mathbin{\in}{\it var}(t_{y})$ *and hence t_{y}[\sigma]\mathrel{\color[rgb]{0,0,1}\cal R}t_{y}[\nu] by ().

By induction on $\pi$, there is a $q_{y}$ with P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}q_{y} and \sigma(y)\mathrel{\color[rgb]{0,0,1}\cal R}q_{y}. Define $\nu(y):=q_{y}$. Properties (ii) and (iii) now hold for $y$.

Take $q^{\prime}:=t[\nu]$. So p^{\prime}\mathbin{=}t[\sigma]\mathrel{\color[rgb]{0,0,1}\cal R}t[\nu]\mathbin{=}q^{\prime} by () and Property (ii) of $\nu$. For each premise (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}})\in H one has u[\sigma]\mathrel{\color[rgb]{0,0,1}\cal R}u[\nu] by (****) and Property (ii) of $\nu$. So P\vdash u[\nu]{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c\;$\hskip 2.5pt}\hfil}}}}} by Claim 3. Since $CT^{+}$ is closed under deduction, together with Property (iii) of $\nu$ this implies P\vdash q=f(q_{1},\ldots,q_{n})\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}t[\nu]=q^{\prime}.

• –

Let p\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\rho]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S[\rho]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} and q\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\nu]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|S[\nu]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} where $S:V_{S}\rightarrow\mbox{\bbb T}(\Sigma)$ with $Z\in V_{S}\subseteq{\it Var}$, $\rho,\nu\!:{\it Var}{\setminus}V_{S}\mathbin{\rightarrow}{\rm T}(\Sigma)$, and for all $x\in{\it Var}\setminus V_{S}$ one has $\rho(x)\mathrel{\cal R}\nu(x)$. Let $\pi$ be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from $P$. By Defs. 4, 5 and 13 \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{Z}|S[\rho]!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} is provable from $P$ by means of a strict subproof of $\pi$. By ($) above one has **$\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\rho]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\nu]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}$**. So by induction there is a **$q^{\prime}$** such that ****$P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\nu]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\scriptstyle a\hskip 2.5pt}\hfil}}}}}q^{\prime}$**** and **$p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime}$**. By Defs. ****4**** and ****13****, **$P\vdash q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Z|S[\nu]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\scriptstyle a\hskip 2.5pt}\hfil}}}}}q^{\prime}$.**

This yields Claim 4. $\Box$

The above result implies that any ntyft/ntyxt language with recursion satisfies congruence requirement (1) up to $\sqsubseteq_{B}$, but is not strong enough to yield (2).

VII A full congruence result

In this section I deal with positive TSSs only. Here the relations \mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda} and $\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{\mu}$ for ordinals $\lambda$ and $\mu$ all coincide, and ${\sqsubseteq_{B}}={\equiv_{B}}$. The following auxiliary concept was used in [45] to show that CCS satisfies Condition (2) of Def. 11.

Definition 15

A symmetric relation $\mathord{\mathrel{\cal R}}\subseteq{\rm T}(\Sigma)\times{\rm T}(\Sigma)$ is a bisimulation up to $\sim$ if $p\mathrel{\cal R}q$ and $P\vdash p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p^{\prime}$ imply that there is a $q^{\prime}$ with $P\vdash q\stackrel{{\scriptstyle a}}{{\longrightarrow}}q^{\prime}$ and $p^{\prime}\sim\mathrel{\cal R}\sim q^{\prime}$, for all $a\in A$. Here ${\sim\mathrel{\cal R}\sim}:=\{(r,s)\!\mid\exists r^{\prime}\!,s^{\prime}\!.~{}r\sim r^{\prime}\mathrel{\cal R}s^{\prime}\sim s\}$.

Proposition 4** **([45])

If $p\mathrel{\cal R}q$ for some bisimulation $\mathrel{\cal R}$ up to $\equiv_{B}$, then $p\equiv_{B}q$.

Proof.

Using the reflexivity of $\equiv_{B}$ it suffices to show that $\equiv_{B}\mathrel{\cal R}\equiv_{B}$ is a bisimulation. Using symmetry and transitivity of $\equiv_{B}$ this is straightforward. ∎∎

Theorem 3

Bisimilarity is a full congruence for any language specified by a TSS in the tyft/tyxt format with recursion.

• Proof:

By Thm. 1 I may assume, without loss of generality, that $P=(\Sigma,R)$ is a TSS in the pure tyft format with recursion. Let $S,S^{\prime}:W\rightarrow\mbox{\bbb T}(\Sigma,W)$ be recursive specifications with $S_{Y}[\sigma]\equiv_{B}S^{\prime}_{Y}[\sigma]$ for all $Y\in W$ and $\sigma:W\rightarrow{\rm T}(\Sigma)$.${}^{\mbox{\scriptsize\ref{onlytwo}}}$ I need to show that \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\equiv_{B}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} for all $X\in W$. Let $\mathord{\mathrel{\cal R}}\subseteq{\rm T}(\Sigma)\times{\rm T}(\Sigma)$ be the smallest relation on processes satisfying

• –

\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}** and \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} for all $X\in W$,**

• –

if $(f,n)\mathbin{\in}\Sigma$ and $p_{i}\mathbin{\mathrel{\cal R}}q_{i}$ for all $i\mathbin{=}1,...,n$, then $f(p_{1},\ldots,p_{n})\mathrel{\cal R}f(q_{1},\ldots,q_{n})$,

• –

and if ${S^{\prime\prime}}:V_{S^{\prime\prime}}\rightarrow\mbox{\bbb T}(\Sigma)$ with $Z\in V_{S^{\prime\prime}}\subseteq{\it Var}$, and $\rho,\nu:{\it Var}\setminus V_{S^{\prime\prime}}\rightarrow{\rm T}(\Sigma)$ satisfy $\rho(x)\mathrel{\cal R}\nu(x)$ for all $x\in{\it Var}\setminus V_{S^{\prime\prime}}$, then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Z|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\nu].

**A trivial structural induction on $t\mathbin{\in}\mbox{\bbb T}(\Sigma)$, using the last two clauses, shows that if $\rho,\nu:{\it Var}\rightarrow{\rm T}(\Sigma)$ satisfy $\rho(x)\mathrel{\cal R}\nu(x)$ for all $x\in{\it Var}$, then $t[\rho]\mathrel{\cal R}t[\nu]$. (*)

So in the first clause one even has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} for all $t\in\mbox{\bbb T}(\Sigma,W)$, (#)

and in the last clause \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}[\nu] for all $t\in\mbox{\bbb T}(\Sigma,V_{S^{\prime\prime}})$. ($)**

It suffices to show that $\mathrel{\cal R}$ is a bisimulation up to $\equiv_{B}$, because with Prop. 4 this implies ${\mathrel{\cal R}}\subseteq{\equiv_{B}}$. By construction $\mathrel{\cal R}$ is symmetric. So it suffices to show that,

if $p\mathrel{\cal R}q$ and P\vdash p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}p^{\prime}, then there is a $q^{\prime}$ with P\vdash q\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q^{\prime} and $p^{\prime}\mathrel{\cal R}\equiv_{B}q^{\prime}$,

for all $p,q\in{\rm T}(\Sigma)$ and $a\in A$, This I will do by structural induction on the proof $\pi$ of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}p^{\prime} from $P$. I make a case distinction based on the derivation of $p\mathrel{\cal R}q$.

• –

Let p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} and q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} with $X\mathbin{\in}W$. Let $\pi$ be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}p^{\prime} from $P$. By Definitions 4 and 13 \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}p^{\prime} is provable from $P$ by means of a strict subproof of $\pi$. By (#) above one has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}. So by induction there is an $r^{\prime}$ such that P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}r^{\prime} and $p^{\prime}\mathrel{\cal R}\equiv_{B}r^{\prime}$. Since \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!\_\!\_|S^{\prime}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is a substitution of the form $\sigma:W\rightarrow{\rm T}(\Sigma)$, one has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\equiv_{B}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S^{\prime}_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}. Hence there is a $q^{\prime}$ such that P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S^{\prime}_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}q^{\prime} and $r^{\prime}\equiv_{B}q^{\prime}\!$. So $p^{\prime}\mathrel{\cal R}\equiv_{B}q^{\prime}\!$. By Definitions 4 and 13 P\vdash q\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}}q^{\prime}\!.

• –

The case p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} and q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} goes likewise, swapping the rôles of $S^{\prime}_{X}$ and $S_{X}$, and using the substitution \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!\_\!\_|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}. 777This proof shows that in the full congruence property (2) one only needs to assume $S_{Y}[\sigma]\equiv_{B}S^{\prime}_{Y}[\sigma]$ for two specific substitutions $\sigma$: namely \sigma(Y):=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!Y|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}, resp. \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Y|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}.

• –

The remaining two cases proceed in the same way as in the proof of Claim 4 for Thm. 2, but suppressing $\lambda$ and with $\mathrel{\cal R}\equiv_{B}$ substituted for the blue occurrences of $\mathrel{\cal R}$. In the last case there are no further changes, so I will not repeat it here. The remaining case needs a few elaborations—these involve the blue coloured segments in the proof of Claim 4:

• –

Let $p\mathbin{=}f(p_{1},\ldots,p_{n})$ and $q\mathbin{=}f(q_{1},\ldots,q_{n})$ where $p_{i}\mathrel{\cal R}q_{i}$ for $i=1,\ldots,n$. Let $\pi$ be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}p^{\prime} from $P$. By Defs. 4 and 13, there must be a pure tyft rule $r=\frac{H}{f(x_{1},...,x_{n})\stackrel{{\scriptstyle a}}{{\longrightarrow}}t}$ in $R$ and a closed substitution $\sigma$ with $\sigma(x_{i})\mathbin{=}p_{i}$ for $i\mathbin{=}1,...,n$ and $t[\sigma]\mathbin{=}p^{\prime}$, such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H the transition t_{y}[\sigma]\mathbin{\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}}\sigma(y) is provable from $P$ by means of a strict subproof of $\pi$. Next, I define a substitution $\nu\!:\!{\it var}(r)\mathbin{\rightarrow}{\rm T}(\Sigma)$ such that

1. (i)

$\nu(x_{i})=q_{i}$** for $i=1,\ldots,n$,** 2. (ii)

$\sigma(y)\mathrel{\cal R}\equiv_{B}\nu(y)$** for each $y\mathbin{\in}{\it var}(r)$,** 3. (iii)

P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}\nu(y)** for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H.**

The definition of $\nu(y)$ and the inference of (i)–(iii) above proceed with induction on the distance of $y\mathbin{\in}{\it var}(r)$ from the source of $r$,

Base case:** Let $\nu(x_{i}):=q_{i}$ for $i=1,\ldots,n$, so that Property (i) is satisfied. Regarding Property (ii), $\sigma(x_{i})\mathrel{\cal R}\nu(x_{i})$ for $i=1,\ldots,n$.**

Induction step:** When defining $\nu(y)$ for some $y\mathbin{\in}{\it Var}$ with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}y)\in H, by induction $\nu(x)$ has been defined already for all $x\mathbin{\in}{\it var}(t_{y})$, so I may assume that $\sigma(x)\mathrel{\cal R}\equiv_{B}\nu(x)$ for all $x\mathbin{\in}{\it var}(t_{y})$, i.e., there exists a substitution $\rho\!:\!{\it var}(r)\mathbin{\rightarrow}{\rm T}(\Sigma)$ with $\sigma(x)\mathbin{\mathrel{\cal R}}\rho(x)\mathbin{\equiv_{B}}\nu(x)$ for all $x\mathbin{\in}{\it var}(t_{y})$. Now $t_{y}[\sigma]\mathbin{\mathrel{\cal R}}t_{y}[\rho]$ by (*******) and $t_{y}[\rho]\mathbin{\equiv_{B}}t_{y}[\nu]$ by Thm. 2.

By induction on $\pi$, there is an $r_{y}$ with P\vdash t_{y}[\rho]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}r_{y} and $\sigma(y)\mathrel{\cal R}\equiv_{B}r_{y}$. By the definition of bisimilarity, there is a $q_{y}$ with P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle c$\hskip 2.5pt}\hfil}}}}}q_{y} and $r_{y}\equiv_{B}q_{y}$. Define $\nu(y):=q_{y}$. Properties (ii) and (iii) now hold for $y$.

Take $q^{\prime}:=t[\nu]$. So $p^{\prime}\mathbin{=}t[\sigma]\mathrel{\cal R}\equiv t[\nu]\mathbin{=}q^{\prime}$ by (*******), Property (ii) of $\nu$, and Thm. 2. By Defs. 4 and 13, together with Property (iii) of $\nu$, this implies**

P\vdash q=f(q_{1},\ldots,q_{n})\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}}t[\nu]=q^{\prime}****. $\Box$

It remains an open question whether the above result can be generalised to the ntyft/ntyxt format with recursion. A direct combination of the proofs of Thms. 2 and 3 does not work, however. An attempt in this direction would substitute either $\mathrel{\cal R}\sqsubseteq_{B}$ or $\sqsubseteq_{B}\mathrel{\cal R}$ for the red \color[rgb]{1,0,0}\mathrel{\cal R} in Claim 2 in the proof of Thm. 2. Both attempts fail on the case p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} and q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} in the proof of Thm. 3.

The first attempt would from P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S^{\prime}{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} infer P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}r^{\prime} by bisimilarity, and then infer P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} by induction. However, one may not use induction, as the transition \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}r^{\prime} may be derived later than \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. In fact, if a variant of this approach would work, skipping \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}} from the definition of $\mathrel{\cal R}$, one could prove a false version of (2) that assumes the antecedent only for the single substitution \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!\_\!\_|S^{\prime}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} (cf. Footnote 7); it is trivial to find a counterexample in the GSOS format with unguarded recursion.

The second attempt would from P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S^{\prime}{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} infer P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S^{\prime}{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}r^{\prime} by induction, and then P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} by bisimilarity. The latter step is invalid, as \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}r^{\prime} is only an overapproximation of P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}r^{\prime}.