Kaustuv Chaudhuri
email: kaustuv.chaudhuri@inria.fr

Matteo Cimini
email: mcimini@indiana.edu

Dale Miller
email: dale.miller@inria.fr

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To

Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the π-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of co-inductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. Since the logic behind Abella also supports λ-tree syntax and generic reasoning using the ∇-quantifier, our treatment of the π-calculus is both direct and natural.

Introduction

To formally show that two processes are bisimilar, we must exhibit a bisimulation relating them. A bisimulation is a relation between processes-i.e., a set of pairs of process expressions-that progresses to itself (formally defined in Section 2.1). The cost of naively computing a bisimulation can be proportional to its size, so for an effective use of the bisimulation proof method it is important to control the size of the computed relations. The size of a bisimulation depends on the complexity of the underlying transition system; if the transition system is unbounded, bisimulations are typically infinite sets.

One well known and general approach, originally due to Milner [START_REF] Milner | Communication and Concurrency[END_REF], of reducing the size of a computed relation is to represent them up to a different relation that identifies redundant pairs of process expressions. Only one representative of each equivalence class of redundant pairs needs to be used in the bisimulation relation. Depending on the identification of redundant pairs, we obtain different bisimulation-up-to techniques. For instance, if we identify process expressions up to bisimilarity, then the bisimulation up to bisimilarity relation allows process expressions to be freely rewritten to bisimilar expressions in the bisimulation-up-to relation. Such a technique can have a large impact: for instance, every bisimulation between the CCS processes ! ! a and ! a is infinite, whereas the singleton relation between them is a bisimulation up to bisimilarity. In some process calculi, particularly for higher-order π-calculi, even defining bisimulation relations can be difficult or impossible without recourse to up-to-techniques. The size reduction also directly improves automating bisimilarity checks, and, can help to produce more compact proof certificates for bisimilarity.

This paper is concerned with providing formal proofs of metatheoretic properties of both CCS and the πcalculus. Of particular importance are proving theorems that guarantee soundness for a number of bisimulationup-to techniques. A bisimulation-up-to relation is sound if it relates only bisimilar processes, i.e., when it is included in the bisimilarity relation. A bisimulation-up-to relation is generally not itself a bisimulation; indeed, the redundant pairs identified by the up-to-techniques need not be coherent with the closure properties of bisimulation. Soundness is not merely of academic interest; without a formal proof of the soundness of a bisimulation-up-to technique, one cannot build a complete formal proof of the bisimilarity of two processes using the up-to-technique.

A rather interesting aspect of formalizing bisimulation-up-to-and indeed of bisimulation itself-is the nature of formal co-inductive proofs. Many formal proof systems today provide some kind of co-inductive reasoning capabilities, and each system carries its own restrictions and limitations. There is also the mathematical sense of co-induction, usually based on some standard theory such as Tarski's theory of fixed points, that uses mathematical concepts: sets, relations, lattices, and so on. Generally speaking, the informal ("pen-and-paper") notions of bisimulation, such as Milner's original definition, are formulated in the latter mathematical style, so to formalize the notions we are faced with a choice: do we use the informal definitions directly in terms of a formalization of the mathematical concepts, or do we use the built-in notions of relations and fixed points provided by the framework? By way of an analogy, consider two approaches to capturing Peano arithmetic. The first approach starts with ZF set theory, defines the notion of injective and bijective functions, equivalence classes (cardinals) of sets under bijections, finite sets, and finally, natural numbers as finite cardinals. On top of such a theory, one can start to build up a theory of arithmetic. The alternative approach, used by, e.g., Gentzen [START_REF] Gentzen | New version of the consistency proof for elementary number theory[END_REF], starts with a stronger proof system, such as the sequent calculus for first-order logic extended with a few simple rules used to account for induction and term equality. Arithmetic can then be attempted directly in such a sequent calculus.

Both formalization choices can be justifiable depending on the intended use of the formalization. In this work, we propose to use, as much as possible, the built-in notions of relations and fixed points provided by the framework, for the following reasons: (1) users of these systems are much more likely to be familiar with the built-in notions than with a particular mathematical library; (2) tools and techniques for automation in these systems are more likely to use the built-in representations; and (3) formalizing bisimulation-up-to, in particular, is an interesting challenge problem for co-inductive reasoning in formal proof systems. We refer to our approach here as lightweight in just the same way that the sequent calculus approach to arithmetic is lightweight when compared to the approach based on set theoretic constructions.

Concretely, we use the intuitionistic logic G [START_REF] Gacek | Nominal abstraction[END_REF] which has a proof-theoretic treatment of least and greatest fixpoints among other features. Bisimilarity is represented in G as the greatest fixpoint of the progress condition for a given transition system. This representation has already been used to formalize the metatheory of bisimilarity, such as the proof that it is a congruence [START_REF]The Abella web-site[END_REF]. We build on this approach by defining the bisimilarity-up-to relation as a greatest fixpoint of the progress condition augmented by a given up-to-technique. Because the bisimilarity-up-to relation contains every bisimulation-up-to relation, we can formally establish the soundness of the bisimulation-up-to technique by showing that the bisimilarity-up-to relation is included in the bisimilarity relation. This theorem is proved by direct co-induction on the greatest fixpoint definitions in the Abella implementation [START_REF]The Abella web-site[END_REF] of G. It is worth remarking that such lightweight approaches to formalization have surprising consequences at times: for example, the bisimulation we define below for the π-calculus is open bisimulation. If, however, we change our formalized logic from intuitionistic to classical logic, the same specification of bisimulation becomes late bisimulation [START_REF] Tiu | Proof search specifications of bisimulation and modal logics for the π-calculus[END_REF].

One of the main benefits of this syntactic approach to metatheory is that we can exploit the features of the G logical framework to represent, declaratively and succinctly, the rules of the transition system specified in the relational SOS format. The most striking of these features is the use of λ-tree syntax [START_REF] Miller | Programming with Higher-Order Logic[END_REF] (a version of higher-order abstract syntax) to represent process expressions with binding constructs, such as the name restriction and bound actions in the π-calculus. The logic G has a sophisticated treatment of the equational theory of λ-terms, built from the notions of nominal abstraction and the ∇-quantifier [START_REF] Gacek | Nominal abstraction[END_REF].

The main contributions of this paper are as follows.

• We show that it is indeed possible to formally establish the soundness of significant bisimulation-up-to techniques for standard process calculi even when the transition systems for these calculi is specified directly using an inductive definition and the bisimilarity relations are given transparent co-inductive definitions. (Section 3.)

• For the specific case of CCS, we give a novel formalization of the faithful contexts technique that is used to show the substitutivity of single hole contexts, and thereby the soundness of the up-to-context and up-to-bisimilarity-and-context techniques. (Section 4.)

• We show that the definitions can be extended, rather uniformly, to the case of process calculi with mobility and restriction, such as the π-calculus; in particular, our formalization of soundness for bisimulation up to bisimilarity for the π-calculus is completely new. (Section 5.)

Following a standard recipe, the proof of soundness for most techniques is built as a composition of two lemmas: for any bisimilarity-up-to relation R, we first show that ∼ R ∼ ⊆ ∼ (where ∼ is the bisimilarity relation), and then show that R ⊆ ∼ R ∼. The first of these lemmas is proved by a co-induction and its proof is modular: the changes required for particular up-to-techniques are confined to easily identifiable subproofs.

The second of these lemmas has a trivial proof. An indirect benefit of our formalization is that we clarify and make precise a number of points in the published informal descriptions of the bisimulation-up-to technique, while remaining faithful to the spirit of these informal proofs. Indeed, even the structures of the formal and the informal proofs are similar.

The complete Abella development accompanying this paper is available at the following URL [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF]:

http://abella-prover.org/upto/ An extensive tutorial on Abella is also available [START_REF] Baelde | Abella: A system for reasoning about relational specifications[END_REF].

Background

Bisimilarity and Up-To-Techniques

Bisimilarity is generally defined for labelled transition systems (LTS). In this section and the next two, we consider in detail the standard LTS for a restriction-free variant of the calculus of communicating systems (CCS) [START_REF] Milner | Communication and Concurrency[END_REF], where processes (P, Q, . . . ) and actions (µ) are given by the following grammar (here a ranges over some fixed set of names).

Act ∋ µ ::= a a τ Proc ∋ P, Q, . . . ::= 0 P | Q P + Q µ. P ! P By standard convention, we shall write simply µ in lieu of µ. 0. We use a standard LTS for CCS processes with transitions of the form P µ -→ Q, which is as in [22, Figure 6.1] except using the rules for the replication operator as presented in [25, Table 1.5]. The following are the standard definitions of bisimulation and bisimilarity for this (and any other) LTS.

Definition 1 (Progression) Given relations R, S ⊆ Proc × Proc, we say that R progresses to S, written R S, if and only if for every pair of processes P, Q with P R Q,

• whenever P µ -→ P ′ , there must be a Q ′ with Q µ -→ Q ′ such that P ′ S Q ′ ; and • whenever Q µ -→ Q ′ ,
there must be a P ′ with P µ -→ P ′ such that P ′ S Q ′ . Definition 2 (Bisimulation) A relation R ⊆ Proc × Proc is said to be a bisimulation if and only if it is a fixpoint of progression (i.e., R R).

Definition 3 (Bisimilarity)

The union of all bisimulation relations for a given LTS is called bisimilarity and is denoted with ∼. Two processes P and Q are said to be bisimilar if and only if there exists a bisimulation relating them.

Fact 4 [START_REF] Sangiorgi | π-Calculus: A Theory of Mobile Processes[END_REF] Every bisimulation is reflexive and symmetric. Bisimilarity is (i) the greatest fixpoint of progression, (ii) the largest bisimulation, (iii) an equivalence and a congruence (i.e., if P ∼ Q then, for every process context

C, C[P ] ∼ C[Q]).
In order to show that two processes are bisimilar, it suffices to exhibit a set of pairs of process expressions that is a bisimulation. Because bisimulation is a fixpoint of progression, any derivatives of a process pair in a bisimulation must also be in the bisimulation. In order to automatically compute a bisimulation between a pair of processes, we have to exhaustively check all the iterated derivatives of the processes for bisimulation. Worse, since we include the replication operator, the underlying LTS is unbounded and hence the space of derivatives of a process is generally infinite. To make the exhaustive exploration of such spaces tractable, we would have to reason about processes algebraically; however, we are prevented from using any of the algebraic properties of processes-not even structural congruences-to simplify the derivatives being enumerated. Thus, even in simple cases such as ! ! a ∼ ! a or !(a + b) ∼ ! a | ! b, exhibiting an explicit bisimulation relation is extremely tedious and not mechanizable.

It is therefore natural to consider a refinement of the definition of bisimulation that allows the derivatives to be suitably rewritten. To this extent, Milner introduced the notion of bisimulation-up-to relations [START_REF] Milner | Communication and Concurrency[END_REF], which are not necessarily themselves bisimulations.

Definition 5 (Up-To-Technique

) A relation U ⊆ Proc × Proc × Proc × Proc is called an up-to-technique. Given a relation R ⊆ Proc × Proc, the relation R up-to U, written R U , is such that P R U Q iff there exist P ′ , Q ′ ∈ Proc such that U(P, P ′ , Q, Q ′ ) and P ′ R Q ′ .
Definition 6 (Up-To) Given R ⊆ Proc × Proc and U ⊆ Proc × Proc × Proc × Proc, we say that R is a bisimulation up to U if and only if R R U . The union of all relations that are bisimulations up to U is called the bisimilarity up to U and is depicted ∼ U .

Note that the up-to-techniques are suitably general and they can relate their four arguments at will. For many situations, however, it is sufficient to consider only a binary up-to-technique that rewrites each derivative of a bisimilar pair independently, which gives us a simpler variant of the above definitions.

Definition 7 (Binary

Up-To) Given relations R, U ⊆ Proc × Proc, we say that R is a bisimulation up to U iff, for the relation V defined by V(P, P ′ , Q, Q ′ ) U(P, P ′ ) ∧ U(Q, Q ′ ), it is the case that R R V . Bisimilarity up to U is similarly defined.
Since the up-to-techniques are not constrained in any way in these definitions, a bisimulation-up-to needs not itself be a bisimulation. However, if it were to be contained in a bisimulation, then it would suffice as evidence for bisimilarity.

Definition 8 (Soundness)

We say that an up-to-technique U is sound when a bisimulation up to U is contained in a bisimulation; equivalently ∼ U ⊆ ∼.

A sound up-to-technique should be understood as identifying redundancies in a bisimulation and allowing the whole relation to be quotiented by that redundancy. Such techniques allow the removal of those pairs of process expressions that are only up-to-variants of the derivatives of another pair in the relation. In other words, any bisimulation-up-to relation for a sound up-to-technique can be suitably enlarged by adding all the up-to-variants of the pairs in the relation to get a bisimulation. Conversely, any bisimulation can be seen as just a bisimulation up to syntactic equality of process expressions.

Fact 9 Let = ⊆ Proc × Proc stand for the syntactic equality of process expressions (which we will call the reflexivity technique). Then, ∼ and ∼ = coincide.

Formalization in G (Abella)

The informal mathematical definitions of Section 2.1 can be directly formalized in the logic G that has built-in support for reasoning about least and greatest fixpoints [START_REF] Gacek | Nominal abstraction[END_REF]. The proof theory of G has been well developed over a sequence of papers [START_REF] Gacek | Nominal abstraction[END_REF][START_REF] Miller | A proof theory for generic judgments[END_REF] and will not be revisited here. Instead, we will directly use the implementation of G in the Abella theorem prover [START_REF]The Abella web-site[END_REF]. Since the SOS rules of CCS and the π-calculus are representable as Horn clauses, they can be accommodated as ordinary inductive definitions in Abella. 1 As a notational convention, all Abella concrete syntax is depicted using a monospaced font.

The following signature represents processes and actions with the concrete types proc and action respectively.

Kind name , action , proc type .

% Action c o n s t r u c t o r s

Type tau action . Type up , dn name -> action .

% P r o c e s s c o n s t r u c t o r s

Type null proc . Type plus , par proc -> proc -> proc . Type act action -> proc -> proc . Type repl proc -> proc .

Actions consist of τ actions, represented by tau, and dual pairs of output and input actions, represented by the up and dn constructors, respectively. The abstract type name is used to draw the names for actions. Processes are constructed in the obvious way; as an example, the process !( The labelled transition system (LTS) for CCS is encoded as an inductive definition one for single steps of the transition, shown in Figure 1. The definition is syntax-directed on the input processes and the actions. Note that the cases of the definition are overlapping, so the one relation is non-deterministic. For replication, in particular, there are two possible transitions, one where the replicated process makes a visible action (the sixth clause) and the other where two copies of the same process interact internally to expose only a tau action (the final clause). This presentation of replication, which is taken from [25, Table 1.5], differs somewhat from Milner's original formulation, which would have replaced these two clauses with the following single clause:

Define one : proc -> action -> proc -> prop by one ( act A P ) A P ; one ( plus P1 P2 ) A Q := one P1 A Q ; one ( plus P1 P2 ) A Q := one P2 A Q ; one ( par P Q ) A ( par P1 Q ) := one P A P1 ; one ( par P Q ) A ( par P Q1 ) := one Q A Q1 ; one ( repl P ) A ( par ( repl P ) Q ) := one P A Q ; one ( par P Q ) tau ( par P1 Q1 ) := exists X , one P ( up X ) P1 /\ one Q ( dn X ) Q1 ; one ( repl P ) tau ( par ( repl P ) ( par Q R ) ) := exists X , one P ( up X ) Q /\ one P ( dn X ) R . We find it easier to work with the presentation in Figure 1. The two styles of definition agree up to structural congruence.

We can then directly define the full bisimilarity-up-to relation by co-induction.

CoDefine bisim_up_ t o : ( proc -> proc -> proc -> proc -> prop ) -> ( proc -> proc -> prop ) by bisim_up_ to Tech P Q := ( forall A P1 , one P A P1 -> exists Q1 , one Q A Q1 /\ exists P2 Q2 , Tech P1 P2 Q1 Q2 /\ bisim_up_t o Tech P2 Q2 ) /\ ( forall A Q1 , one Q A Q1 -> exists P1 , one P A P1 /\ exists P2 Q2 , Tech P1 P2 Q1 Q2 /\ bisim_up_t o Tech P2 Q2 ) .
The definition of bisim_up_to is higher-order: its first argument is the up-to-technique, which is used to rewrite the derivatives of the two steps. The reasoning logic G of Abella is a first-order logic, so allowing this kind of higher-order definition requires some explanation. In Abella, such higher-order definitions are allowed only if both of the following conditions are met:

• The higher-order arguments, i.e., the arguments with type containing prop, must always be the same universally quantified variable in both head and every recursive occurrence in the body of every clause.

• Such arguments can, moreover, not be used in any subformula to the left of the implication in the body.

These restrictions amount to imposing a module-like protocol, wherein every instance of the defined atom might be seen as being produced, uniformly, by instancing a common schematic form. In the rest of this paper, we will use the following notations for the types to avoid spacing problems:

proc2 for proc -> proc -> prop proc4 for proc -> proc -> proc -> proc -> prop As an example of an up-to-technique, we can consider reflexivity, which when used as an argument to bisim_up_to gives us the usual definition of bisimilarity (cf. Fact 9). We can then define the soundness of a given up-to-technique as follows.

Define is_sound : proc4 -> prop by is_sound Tech := forall P Q , bisim_up_ t o Tech P Q -> bisim P Q .

Abella will emit a warning about this definition of is_sound that the higher-order argument variable Tech is being used to the left of an implication. While the definition itself does not affect the consistency, it is easy to use such definitions to defeat the syntactic stratification checker of Abella that guarantees that all inductive or co-inductive definitions indeed denote a corresponding least or greatest fixed point. Therefore, Abella will prevent the user from using is_sound to construct any other definitions; it can only be used in the sense of a syntactic macro, with no associated induction or co-induction principles. Practically, these restrictions on higher-order arguments amount to preventing the definitions of up-to-techniques that themselves make use of particular properties of the up-to-technique (such as soundness).

Up-To-Bisimilarity

The bisimilarity relation ∼ is itself an excellent example of a binary up-to-technique. In this section we discuss in detail our formulation of bisimilarity up to bisimilarity and its soundness proof in Abella.

Intuitively, a bisimulation up to bisimilarity allows us to perform the co-inductive step in reasoning about bisimulation not just with the derivatives of the starting pair of processes, but also with any pair that is pointwise bisimilar to them. As we have seen in the previous section, in order to formulate this technique all we need to do is to define the appropriate predicate that encodes the bisimilarity-up-to technique, which is straightforward: For the sake of clarity, let us be explicit about the associated up-to-technique.

B(P 1 , P 2 , Q 1 , Q 2 ) P 1 ∼ P 2 ∧ Q 1 ∼ Q 2 .

This is directly represented in Abella:

Define bisim_t : proc4 by bisim_t P1 P2 Q1 Q2 := bisim P1 P2 /\ bisim Q1 Q2 .

To prove the soundness of B, i.e., that ∼ B ⊆ ∼, one typically uses two lemmas, one establishing that ∼ ∼ B ∼ ⊆ ∼, and the other that ∼ B ⊆ ∼ ∼ B ∼. In fact, this kind of factoring of a soundness proof for an arbitrary up-to-technique is common enough that we first define the two lemmas generically. We omit full Abella proofs in this paper because they can be found in [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF]. Instead, in the rest of this section we will discuss some details of these proofs. We begin with the main soundness theorem bisim_sound. bisim_sound: To illustrate how proofs are written in Abella, let us begin with the last of these theorems, a straightforward consequence of bisim_sound_fst and bisim_sound_snd. In order to express this composition in Abella, we first have to unfold the definitions is_sound_fst, is_sound_snd, and is_sound to expose the implications. Abella does not unfold definitions automatically because unfolding is a core component of its treatment of induction and co-induction measures.

Since Abella's reasoning logic is first-order, one cannot prove this composition generically in a manner such as:

forall ( Tech : proc4 ) , i s _ s o u n d _ f s t Tech -> i s _ s o u n d _ s n d Tech -> is_sound Tech .
The type of Tech contains prop, but forall can only quantify over terms whose types do not contain prop.

As a consequence, every instance of this theorem has to be stated and (re-)proved separately. For such usage patterns a real module system in Abella would have avoided the repetition. Fortunately, the repeated proof is tiny and identical for every case, even if the associated definition of the step or the bisimulation-up-to relations were to change.

bisim_sound_snd:

The proof of this lemma only relies on the reflexivity of bisimilarity, which is the lemma bisim_refl in our formalization [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF] (cf. Fact 4). After expanding the definition of bisim_sound_snd and assuming the hypothesis bisim_up_to bisim_t P Q, we are left with the obligation exists R S , bisim P R /\ bisim_up_t o bisim_t R S /\ bisim S Q

At this point, we instantiate R and S with P and Q respectively, and appeal to reflexivity of bisimilarity in order to discharge the two conjuncts bisim P P and bisim Q Q. The remaining conjunct is exactly the assumption of the lemma. It hardly merits remarking that this proof too is a direct representation of its informal version and can be employed for different techniques and different equivalence relations, as long as they are reflexive.

bisim_sound_fst:

The core component of the soundness theorem is the lemma bisim_sound_fst, which we now discuss in some detail. The proof must proceed by co-induction, which is implemented in Abella using a tactic that introduces a co-inductive hypothesis (labelled CH):

forall P Q , ( exists R S , bisim P R /\ bisim_up_t o bisim_t R S /\ bisim S Q ) -> bisim P Q +
The + at the end is a co-inductive size annotation which asserts that the atom bisim P Q has resulted from at least one unfolding of the conclusion of the theorem bisim_sound_fst. In order to enforce this restriction, the goal of the theorem is rewritten to:

forall P Q , ( exists R S , bisim P R /\ bisim_up_t o bisim_t R S /\ bisim S Q ) -> bisim P Q #
where the # annotation asserts that co-inductive progress has not been made.

We can now introduce the variables and antecedents of the goal (using the intros tactic), leaving the residual goal bisim P Q #. In order to finish the proof, we must take at least one co-inductive step by unfolding the (co-)definition of bisim, which will change the size annotation from a # to a + and thereby enables appeals to the CH. (The soundness of this approach to co-induction is addressed in [START_REF] Gacek | A Framework for Specifying, Prototyping, and Reasoning about Computational Systems[END_REF].)

Unfolding the definition of bisim (and then the resulting bisim_up_to refl_t) will result in two subgoals corresponding to steps from P and from Q respectively. We discuss only one of these here as the other is symmetrical and similar. The goal here is:

forall A P1 , one P A P1 -> ( exists Q1 , one Q A Q1 + /\ ( exists P2 Q2 , refl_t P1 P2 Q1 Q2 + /\ bisim P2 Q2 +) ) .

Observe that the + annotation propagates to the three conjuncts. At this point we can introduce the antecedent one P A P1 as a new hypothesis. The rest of the proof consists of an alternation of two different kinds of reasoning: (1) for each action A, we must find a corresponding instantiation for Q1 that makes one Q A Q1 true, and (2) for each such Q1, we must relate it to the derivative P1 in order to make the CH applicable.

Finding the derivative Q1: Let us recall that we already assumed the following hypotheses (with names written with colons to the left) before we initially unfolded the goal bisim P Q #:

H1 : bisim P R H2 : bisim_up_t o bisim_t R S H3 : bisim S Q
where R and S are the variables introduced by destructing the exists in the antecedent. From these assumptions, we can make the following chain of inferences: for each action taken by P, there will be a corresponding action from R (by H1), which in turn implies the same action from S (by H2), and then finally from Q (by H3). For the most part, this chain of inferences merely requires unfolding the definitions of bisim and bisim_up_to (which is achieved using the case tactic), and then plumbing the bodies together. At this point, we will be able to instantiate Q1 in the goal and discharge the first conjunct that results. Discharging the second conjunct about refl_t merely requires instantiating P2 and Q2 with P1 and Q1 respectively. This leaves just the third conjunct, bisim P1 Q1 +.

Relating the derivatives: Note that this goal now matches the head (i.e., the rightmost atom in the chain of implications) of the CH. We can therefore backchain the CH to the goal giving us the residual subgoal:

exists R1 S1 , bisim P1 R1 /\ bisim_up_ t o bisim_t R1 S1 /\ bisim S1 Q1
It is important to note that we used the CH to reason about the derivatives of the original processes, which is why the CH needed to be universally closed. Each of these conjuncts is nearly found among the assumptions that resulted earlier from unfolding H1, H2, and H3. However, they are not exactly present and we need to appeal to additional properties of bisimilarity that need to be established earlier. In particular, we will need to appeal to both symmetry and transitivity of bisimilarity (cf. Fact 4) to complete the chain of inferences. This is not surprising, as bisimilarity up to bisimilarity is the greatest fixpoint of a progression from a relation R to ∼ R ∼. (Only transitivity is explicitly mentioned as a necessary condition in [22, Lemma 6.2.3]; this point is not as relevant to the up-to-bisimilarity technique, since bisimilarity is an equivalence, but it becomes important for other techniques.)

Discussion: An important feature of this proof is that it is schematic in two orthogonal senses. First, were we to consider a different up-to-technique, only the reasoning about relating the derivatives needs to be replaced. Second, replacing the LTS for CCS with a different one preserves the general structure of the proof; only the number of cases might differ depending on the definition of bisimilarity and the step relation of the LTS. The essence of the soundness of each up-to-technique is just reasoning about relating the derivatives of two parallel steps, which is the only component of the soundness proof that differs. It is readily apparent in reading the accompanying formal development available at [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF] that we are able to maintain this schema when proving the corresponding theorems for open bisimilarity of the π-calculus and even for weak bisimilarity of CCS and the π-calculus.

In [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF] we offer some examples of using bisimilarity up to bisimilarity to show that two CCS processes are bisimilar. Specifically, we have the full proof of ! ! a ∼ ! a and !(a + b) ∼ ! a | ! b using the up-to-bisimilarity technique and its soundness. It is nearly impossible to construct a bisimulation for these cases directly as the relations are infinite and have a rather convoluted internal structure. On the other hand, we can construct the evidence for them being bisimilar up to bisimilarity formally by a direct co-inductive proof.

Up-to Context

While bisimulation up to bisimilarity is an excellent tool for reducing the size of the computed relations, and is perhaps the best known example of an up-to-technique [START_REF] Milner | Communication and Concurrency[END_REF], it still does not allow compositional reasoning about bisimulation. The up-to-context technique [22, Section 6.2.2] is better suited for this kind of reasoning: it uses contextual closure to factor out a common context in the derivatives and hone on the relevant subprocesses.

A process context C is a process expression with a single hole occurring in the position of a process subexpression, and C[P ] represents that process expression that results from replacing the hole with P . We represent contexts in Abella using the type cx with the following signature.

Kind cx type . Type hole cx . Type act_d action -> cx -> cx . Type plus_l , par_l cx -> proc -> cx . Type plus_r , par_r proc -> cx -> cx .

Context substitutions are defined inductively using the ternary relation at, with the interpretation at C P Q if and only if C[P ] = Q when C, P, Q stand respectively for C, P , Q. Note that we do not allow the context hole to be present under a replication, so ! a.[ ] is not an example of a valid context; this restriction is explained below.

We follow closely the definition in [22, Section 6.2.2] in our definition of the up-to-context technique.

Definition 11 (Up-To-Context)

The relation K ⊆ Proc × Proc × Proc × Proc is given as follows:

K(P 1 , P 2 , Q 1 , Q 2 ) ∃C. C[P 2 ] = P 1 ∧ C[Q 2 ] = Q 1 .
Note that this is the first place where it is important that both pairs in a bisimulation are rewritten at once, since we must factor out a common context; thus, it is not possible to define this relation using binary up-to-techniques. This technique is readily formalized in Abella. The proof of soundness of the up-to-context technique is a bit more involved than that of up-to-bisimilarity. Since a common context is factored out of the derivatives of the two candidate processes, it is important to show that this kind of factoring is coherent with the bisimilarity relation itself. In fact, we need a stronger property: we need to know that ∼ K (i.e., bisim_up_to context_t) is substitutive, that is, whenever P ∼ K Q that also C[P ] ∼ K C[Q] for any context C. We write this as follows in Abella:

One important note is that if we were to attempt to extend the definition of contexts to allow holes under replication, then the contexts would not remain faithful. In fact, this remains the case even if replication is guarded by action prefixes. For a simple example,2 consider the context C = ! a.[ ]. Then, for any process P , we have C[P ] a -→ C[P ] | P , but the derivative cannot be represented in the form C ′ [P ]. This limitation may be relaxed somewhat with the use of variadic contexts, but it is unclear how, if at all, the notion of faithful contexts would extend to it.

Proving substitutivity: We can then return to showing that the context_t technique is substitutive.

forall P1 P2 C Q1 Q2 , at C P1 Q1 -> at C P2 Q2 -> bisim_up_t o context_t P1 P2 -> bisim_up_ t o context_t Q1 Q2 .
We proceed here by co-induction. After unfolding the definitions in the conclusion, we then immediately appeal to ccs_faithful to obtain a result about the first assumption, at P0 C P. This gives us two cases. In the first case, the process P stays unchanged during one P0 A R, in which case we directly obtain the required result for Q0 from the definition of faithful contexts. In the second case, we proceed by case-analysis for the possible transitions of P, and in each case, we use the definition of faithful contexts to construct a matching step for Q. The proof here critically relies on the fact that at and concatenate are deterministic to correlate the contexts that are existentially quantified in the definition of faithful contexts to those resulting from unfolding bisim_up_to context_t.

Soundness: Once we know that bisim_up_to context_t is substitutive, it is then a simple corollary that context_t must be sound. From the definition of context_up_to, we know that there is a common context in the derivatives that is factored out and the remainder are bisimilar up to context. By substitutivity, the derivatives must therefore themselves be bisimilar up to context. The required result follows trivially from the co-inductive hypothesis.

Theorem c o n t e x t _ s o u n d : is_sound context_t .

The full details of the proof can be found in [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF].

Combining up-to-bisimilarity and up-to-context. The nature of co-induction in G and Abella is general enough to allow for the combination of multiple up-to-techniques. In this paper we do not formalize the general theory of when two up-to-techniques can be combined, as done informally in [START_REF] Pous | Enhancements of the bisimulation proof method[END_REF] and largely formalized in Coq in [START_REF] Pous | Weak bisimulation upto elaboration[END_REF][START_REF] Pous | Complete lattices and upto techniques[END_REF]. Instead, we illustrate an important combination of the up-to-bisimilarity and up-to-context techniques (cf. [22, Definition 6.2.11]).

Definition 13 (Up-To-Bisimilarity-And-Context)

The relation BK, a subset of Proc × Proc × Proc × Proc, is as follows.

BK (P 1 , P 3 , Q 1 , Q 3 ) ∃P 2 , Q 2 . B (P 1 , P 2 , Q 1 , Q 2 ) ∧ K(P 2 , P 3 , Q 2 , Q 3 ).
This technique is readily formalized in Abella:

Define b i s i m _ c o n t e x t _ t : proc4 by b i s i m _ c o n t e x t _ t P1 P3 Q1 Q3 := exists P2 Q2 , bisim_t P1 P2 Q1 Q2 /\ context_t P2 P3 Q2 Q3 . Theorem s o u n d _ b i s i m _ c o n t e x t _ t : is_sound b i s i m _ c o n t e x t _ t .
We can prove this relation sound by a combination of the approaches of Section 3 and this section, by using the factorization to handle reasoning up to bisimilarity and the congruence of bisimilarity to reason up to context. The proof is omitted here for space reasons, but can be found in [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF].

Examples: Also in [START_REF] Chaudhuri | The Abella formalization of bisimulation-up-to for CCS and the π-calculus[END_REF] are the following illustrative examples: ! ! a.P ∼ ! a.P and !(a.P + b.P ) ∼ ! a.P | ! b.P , for every process P . This universal quantification over the continuation processes requires both up-to-context and up-to-bisimilarity reasoning, unlike the examples at the end of Section 3 where up-to-bisimilarity sufficed.

From CCS to the π-Calculus

We now summarize how the definitions and theorems above for CCS can be lifted to accommodate the binding structures of the π-calculus. It is striking how little the formalization in Abella needs to change to accommodate such binding structures. Reasoning about names and name restriction in the π-calculus is directly achieved using G's nominal abstraction [START_REF] Gacek | Nominal abstraction[END_REF], ∇-quantifier [START_REF] Miller | A proof theory for generic judgments[END_REF], and λ-tree syntax [START_REF] Miller | Programming with Higher-Order Logic[END_REF]. While we cannot given a formal presentation of these extensions to logic, their accumulation into one logic yields a system in which names of bound variable are not semantically interesting and are, in fact, impossible to accept. Instead of using the names of binders, Abella and G have flexible and more declarative ways to treat binders that involve the nesting of term-level λ-abstractions and the ∀, ∃, and ∇ quantifiers.

Processes in the π-calculus are as follows (where x, y, . . . range over names):

P, Q, . . . ::= 0 P | Q P + Q ! P τ. P x (y) . P

x y . P (νx) P .

The first four constructs are common to CCS, while the remaining ones-τ actions, input, output, and name restriction-are different for the π-calculus. These new constructs are encoded in G using λ-tree syntax as follows.

Type taup proc -> proc .

Type out name -> name -> proc -> proc . Type in name -> ( name -> proc ) -> proc . Type nu ( name -> proc ) -> proc .

As an example, the process (νx) (!(x (y) . P + Q) | x k . R) is represented as:

nu x \ ( par ( repl ( plus ( in x P ) Q ) ) ( out x k R ) )
where k, P, Q, R represent k, P , Q, R respectively. The form x\ T is concrete syntax in Abella-borrowed from λProlog [START_REF] Miller | Programming with Higher-Order Logic[END_REF]-for the λ-term λx. T , so (νx) P is written simply as nu x\ P, which parses as nu (x\ P) by Abella's precedence rules. Note that the type of P is name -> proc, so the bound name y is not explicitly mentioned in the encoding; it could be made explicit by writing the input-prefixed process as in x (y\ P y), but in this case P y indicates an explicit dependency of P on the input variable y. If we were to write it instead as in x (y\ P), then the lack of dependency of P on y would be interpreted to mean that y cannot be free in P . This kind of intrinsic encoding of syntactic side-conditions is a feature of λ-tree syntax that we will rely on pervasively. Indeed, the key feature of the LTS for the π-calculus is the notion of a bound step, which is usually treated in informal presentations of the π-calculus (such as in [START_REF] Sangiorgi | π-Calculus: A Theory of Mobile Processes[END_REF]) using a notion of α-variance over the traces and derivatives. In G and Abella we can avoid this distraction by using λ-tree syntax also for the bound actions. Concretely, the (late) transitions for the π-calculus are formalized in terms of the mutually inductive definitions of bound actions (oneb) and other steps (one), of which only the interesting cases are shown below. The cases for communication highlight how bound input actions match up with (closed) output actions. The definition of bisimilarity-up-to for the π-calculus extends the related definition for CCS by incorporating additional cases to deal with bound steps. The number of cases in the definition of bisim_up_to grows from two to six, two each for closed, bound input, and bound output actions.

Two important features of the continuations of bound actions are highlighted using particular colors in this definition. The continuations of bound inputs (dn X) are defined using the forall-quantifier: to show that two processes, both of which can do a bound input on the same named channel, are in a given bisimulation, one should show that for every instance (i.e., using the ∀ quantifier of G) of the bound value, the two instantiated continuations are also in that bisimulation. Similarly, continuations of bound outputs (up X) are treated with the nabla-quantifier because showing that two processes, both of which can do a bound output on the same named channel, are in a given bisimulation, requires selecting a fresh new name (using the ∇ quantifier of G) and showing that the two continuations, instantiated with that name, are also in that bisimulation. The adequacy of this encoding of open bisimulation [START_REF] Sangiorgi | π-Calculus: A Theory of Mobile Processes[END_REF] for the π-calculus is shown in [START_REF] Tiu | Proof search specifications of bisimulation and modal logics for the π-calculus[END_REF].

The remaining definitions of the preceding sections can be generalized to handle the π-calculus and the theorems and proofs can be adjusted (by hand) in a straightforward and predictable fashion. Indeed, the definitions of the up-to-techniques does not change at all, and only the proofs of the soundness theorems need to be modified to accommodate the additional cases of bisimilarity-up-to in the π-calculus.

Up-To-Bisimilarity:

The proof of soundness for the up-to-bisimilarity technique for the π-calculus is structurally identical to that for CCS (in Section 3, except with three times as many cases. For the most part it was straightforward to adapt the CCS proof to the π-calculus proof by hand. However, this is another instance where having some kind of modular proof language would have been an immense benefit. Much of the argumentation is common across the different cases of bisimulation, but the proof text needs to be manually duplicated.

Nevertheless, a major benefit of using the Abella framework is that none of the overhead of moving from a process calculus with binding manifested in the encodings of syntax. In particular, the usual side conditions that appear in informal presentations of the LTS for the π-calculus, particularly in the open and close rules for name restrictions, is manifested directly by λ-dependencies. This is best illustrated by the penultimate clause of the oneb relation, which we write here in a slightly more explicit form.

; oneb ( nu ( y \ M y ) ) ( y \ up X y ) ( y \ N y ) := nabla y , one ( M y ) ( up X y ) ( N y )

This clause, which implements the close rule of the LTS, directly links bound name y in the label up X y and the continuation process N y to the restricted name y in the input process. Note here that using a forall would be invalid, since we need to know that the restricted name y is distinct from all the other free names in M y.

Up-To-Context: Extending the soundness result to the up-to-context and up-to-bisimilarity-and-context for the π-calculus is a much more involved proposition. In fact, even defining the notion of a process context in the π-calculus is tricky, because contexts are allowed to capture free names. Some of the free names of P in C[P ] may be captured by input actions prefixes (in), while others may be captured by restrictions (nu).

A more pressing issue is that the proof of substitutivity of a π-calculus context cannot appeal to the notion of faithful contexts, because that is a purely first-order notion. One alternative would be to use evolutions and initial contexts as developed in [START_REF] Pous | Enhancements of the bisimulation proof method[END_REF], but we leave it to future work.

Related Work

The π-calculus has been formalized several times before. An early formalization [START_REF] Honsell | π-calculus in (co)inductive type theories[END_REF] used Coq to specify and prove properties of strong late bisimilarity: that formalization built formal mechanisms to support notions such as "freshness" within a scope, substitution of names, occurrences of names in expressions, etc. A similar approach is followed in [START_REF] Gabbay | The π-calculus in FM[END_REF] but instead of Coq, the nominal set theory of [START_REF] Gabbay | A new approach to abstract syntax with variable binding[END_REF] was used to develop those formal mechanisms. An Isabelle implementation of the nominal logic approach was used in [START_REF] Bengtson | Formalising the π-calculus using nominal logic[END_REF] to formalize and prove some of the metatheory of the π-calculus. This paper follows the papers [START_REF] Miller | Foundational aspects of syntax[END_REF][START_REF] Miller | A proof theory for generic judgments: An extended abstract[END_REF][START_REF] Tiu | A proof search specification of the π-calculus[END_REF] which used the λ-tree syntax approach to specification in order to capture the nominal and binding structures of the π-calculus: those formal mechanisms are captured differently using the natural interplay of nested quantifiers and λ-bindings in expressions.

This paper is also not the first attempt to formalize the bisimilarity-up-to technique. The oldest, largest, and possibly the most comprehensive of these formalizations has been done in Coq [START_REF] Pous | Weak bisimulation upto elaboration[END_REF][START_REF] Pous | Complete lattices and upto techniques[END_REF][START_REF] Bonchi | Checking NFA equivalence with bisimulations up to congruence[END_REF]; indeed, this framework has been set up to tackle the much harder problem of weak bisimilarity-up-to, which is well known to have a rather subtle definition [START_REF] Sangiorgi | The problem of "weak bisimulation up to[END_REF][START_REF] Pous | Enhancements of the bisimulation proof method[END_REF]. The main difference from our approach in this present work is that this formalization in Coq builds the theory of bisimulation from scratch, starting from a formalization of the mathematics of relations, fixpoints, and so on. While this allows the framework to remain general, it does not use the co-induction of Coq; in particular, the definition of bisimulation is not a co-fixpoint in Coq. Moreover, the current state of the Coq development uses only illustrative examples of simple LTS, instead of standard ones such as that of CCS or the π-calculus.

Arguably, the implementation of co-recursion in Coq cannot be used directly for bisimulation-up-to (or even bisimulation) because of a rather inflexible syntactic productivity check. The approach of [START_REF] Endrullis | Circular coinduction in Coq using bisimulation-up-to techniques[END_REF] is the most recent example of approaches that try to circumvent this check by means of rewriting techniques. Many such approaches can be seen as instances of a general family of parametrized co-induction [START_REF] Hur | The power of parameterization in coinductive proof[END_REF]. Such approaches have at least two limitations currently: first, the encoding of bisimulation is not directly related to the SOS specification of an LTS, and so requires an additional informal step of "compiling" the LTS; and second, this approach has no built-in support for names and binding.

A recent paper [START_REF] Madiot | Bisimulations up-to: Beyond first-order transition systems[END_REF] shows that reasoning about the up-to-techniques that the present paper addresses for the π-calculus can be transported onto the ordinary theory of bisimulation-up-to that targets calculi with no binding. To enable this result, the authors offer an accurate encoding from the richer LTS of the π-calculus into a version of it that avoids binding. This type of approach follows a development that is very different from a direct and natural informal proof. For instance, the states of the target LTS of this encoding are processes enriched with additional information, so achieving the soundness results requires new up-to-techniques to deal with this new state. Our approach is considerably more conservative; we stay closer to the standard informal development of up-to-techniques for the π-calculus.

As we stated in Section 1, showing that two process calculus expressions are bisimilar typically involves demonstrating two facts: (1) that those process expressions are within a particular bisimulation-up-to relation and ( 2) that such a bisimulation-up-to relation is, in fact, sound. In this paper, we have focused only on this second problem. The first problem is more related to model checking than sophisticated interactive theorem proving. The Bedwyr model checker [START_REF] Baelde | The Bedwyr system for model checking over syntactic expressions[END_REF][START_REF]The Bedwyr model checker[END_REF] has been used to perform state exploration over labelled transition systems involving process calculi such as CCS and the π-calculus. Since the logic G underlying Abella also provides a formal foundation for the logic underlying Bedwyr, theorems proved by the latter can be accepted directly by the former. In this way, Abella and Bedwyr can be used together to provide a trusted basis for establishing bisimulation results.

Conclusions

Since the proof theory literature has now adequately addressed the necessary features of relational programming, least and greatest fixpoints, and binding structures in terms, and since the Abella theorem prover directly supports those innovations, Abella seems to be a natural setting to formalize the metatheory of bisimulationup-to. We have shown this to be the case in this paper. In particular, we have shown that (1) the mathematical definitions of important relations could be written directly within the logic of Abella; (2) the available informal theorems and proofs could be used to provide detailed outlines for the fully formal proofs; (3) we could lift in a straightforward fashion our definitions, theorems, and proofs involving a system without bindings to a system with bindings; and (4) we believe that we have written our formalism in a modular fashion that will allow us to attack the metatheory of a number of other up-to-techniques.

  a. b)|b is encoded by the term par (repl (act (up a) (act (dn b) null))) (act (up b) null), if we add constants a,b of type name to the signature to represent the free names of the process !(a. b) | b.

Figure 1 :

 1 Figure 1: The LTS for CCS as a definition

  Define refl_t : proc4 by refl_t P P Q Q . CoDefine bisim : proc2 by bisim P Q := bisim_up_ t o refl_t P Q .

Definition 10 (

 10 Up-To-Bisimilarity) The relation B ⊆ Proc × Proc × Proc × Proc is determined by

  Define i s _ s o u n d _ f s t : proc4 -> prop by i s _ s o u n d _ f s t Tech := forall P Q , ( exists R S , bisim P R /\ bisim_up_ t o Tech R S /\ bisim S Q ) -> bisim_up_ t o Tech P Q . Define i s _ s o u n d _ s n d : proc4 -> prop by i s _ s o u n d _ s n d Tech := forall P Q , bisim_up_ t o Tech P Q -> ( exists R S , bisim P R /\ bisim_up_ t o Tech R S /\ bisim S Q ) .

For

  the specific up-to-technique B, we can then show soundness directly by instantiating Tech with bisim_t. Theorem b i s i m _ s o u n d _ f s t : i s _ s o u n d _ f s t bisim_t . Theorem b i s i m _ s o u n d _ s n d : i s _ s o u n d _ s n d bisim_t . Theorem bisim_soun d : is_sound bisim_t .

  Define at : ctx -> proc -> proc -> prop by at hole P P ; at ( plus_l C R ) P ( plus Q R ) := at C P Q ; at ( plus_r R C ) P ( plus R Q ) := at C P Q ; at ( par_l C R ) P ( par Q R ) := at C P Q ; at ( par_r R C ) P ( par R Q ) := at C P Q ; at ( act_d A C ) P ( act A Q ) := at C P Q .

  Define context_t : proc4 by context_t P1 P2 Q1 Q2 := exists C , at C P2 P1 /\ at C Q2 Q1 .

  Define one : proc -> action -> proc -> prop , oneb : proc -> ( name -> action ) -> ( name -> proc ) -> prop by /* c l o s e d _ a c t i o n s */ one ( taup P ) tau P ; one ( out X Y P ) ( up X Y ) P ... /* c o m m u n i c a t i o n */ ; one ( par P Q ) tau ( par ( M Y ) T ) := exists X , oneb P ( dn X ) M /\ one Q ( up X Y ) T ; one ( par P Q ) tau ( par R ( M Y ) ) := exists X , oneb Q ( dn X ) M /\ one P ( up X Y ) R ... /* bound a c t i o n s */ ; oneb ( in X M ) ( dn X ) M ; oneb ( plus P Q ) A M := oneb P A M ; oneb ( plus P Q ) A M := oneb Q A M ; oneb ( par P Q ) A ( x \ par ( M x ) Q ) := oneb P A M ; oneb ( par P Q ) A ( x \ par P ( N x ) ) := oneb Q A N ; oneb ( nu M ) ( up X ) N := nabla y , one ( M y ) ( up X y ) ( N y ) ; oneb ( repl P ) A ( x \ par ( repl P ) ( M x ) ) := oneb P A M .

We will not need to use Abella's two-level logic support in this paper.

Suggested by Damien Pous in private communication

Acknowledgements This work was funded, in part, by the ERC Advanced Grant ProofCert and by the Inria Associated Team grant RAPT. We thank the anonymous reviewers for their comments on an earlier draft of this paper.

Define s u b s t i t u t i v e : proc2 -> prop by s u b s t i t u t i v e _ r e l Rel := forall P1 P2 C Q1 Q2 , at C P1 Q1 -> at C P2 Q2 -> Rel P1 P2 -> Rel Q1 Q2 .

Faithful contexts:

We cannot directly show by co-induction that substitutive (bisim_up_to context_t) because we need to argue about the actions of a process in an arbitrary context and how it relates to the actions of the process itself. Unless contexts are well-behaved, there is no reason to think that these sets of actions have any relation. Fortunately, in the case of CCS we can show that the contexts are faithful [START_REF] Sangiorgi | On the bisimulation proof method[END_REF], which allows us to characterize precisely the actions of a process in a context.

Definition 12 (Faithful Contexts)

A set of contexts S is said to be faithful if for every C ∈ S, processes P, R, and label µ, if

• there is a C ′ ∈ S, a process P ′ , and a label µ ′ such that

The third option in the definition above is needed to account for the possibility that the hole in a context is in a summand that will be discarded in a step. The definition of faithful contexts in [START_REF] Sangiorgi | On the bisimulation proof method[END_REF] handled this situation in a slightly different form, using contexts with at most one hole. It turns out that allowing for no holes in contexts is unwieldy as any theorem involving contexts now has to either account for this possibility or rule it out somehow. We therefore stay with our simpler case of contexts with exactly one hole and just suitably alter the definition of faithful contexts. The two variants of the definition are equivalent, and either definition would have sufficed for our ultimate goal of showing substitutivity of the up-to-context technique.

We prove that all CCS contexts are faithful in Abella directly by induction on the structure of contexts. Fortunately, since at is defined in a syntax-directed way on contexts, it is sufficient to induct on derivations of at directly. The Abella theorem and the start of its proof is then as follows.

% % induct on : at C P P0 induction on 1. intros . case H1 .

The proof proceeds in a systematic fashion by induction on the structure of contexts, which is uniquely determined by the cases of the at relation. We require one important lemma about context concatenation: if

Our proof is greatly simplified by the fact that the at relation is deterministic in its second and third arguments, i.e., that C[P 1 ] = C[P 2 ] if and only if P 1 = P 2 . If we were to use contexts with at most one hole, then we would need an additional nested induction to rule out the no-hole case.


Comments on: "Continuous initial observability of nonlinear delay parabolic equations" by Rong Jae Choi, Young Chel Kwun and Jong Seo Park Rabah Rabah IRCCyN UMR 6597, 1 rue de la Noë, BP 92101, 44321 Nantes Cedex 3, France Email: rabah@emn.fr

Abstract. It is shown that the assumptions of the main result of the cited paper can never be satisfied.

Mathematical Subject Classification: 93C20, 93B07.

In the paper [START_REF] Choi | Continuous initial observability of nonlinear delay parabolic equations[END_REF] the problem of continuous initial observability is considered for the delayed infinite dimensional system

   x(t) = S(t)φ(0) + t 0 S(t -s)F (s, x s )ds, t ∈ [0, T ], x(t) = φ(t), t ∈ [-h, 0], y(t) = Πx(t), (1)
where S(t) is a C 0 -semigroup given on a Hilbert space, namely X = L 2 (Ω), where Ω is a bounded domain in R n , Π is a bounded linear operator from X to the Hilbert space Y , F is a noon linear function. In order to investigate this problem, authors consider the linear non delayed part of the system:

   ẋ(t) = Ax(t) x(0) = φ(0) y(t) = Πx(t). (2)
The main assumptions are: the semigroup S(t) is analytical and compact (assumption H3) and the system (2) is initially continuously observable (assumption H1). Under those assumptions conditions of initial continuous observability of the system (1) are given.

We claim that the necessary condition of initial continuous observability of the system (2) is that the semigroup S * (t) is onto or that each operator S(t) has a bounded inverse operator defined on Im S(t). If S(t) is compact, then S * (t) is compact and cannot be onto in an infinite dimensional Hilbert space. If S(t) is analytical then Im S * (t) ⊂ D(A * ) and then the operators S * (t) cannot be onto.

1

We need a precise definition of the initial observability because the definition given in [START_REF] Choi | Continuous initial observability of nonlinear delay parabolic equations[END_REF] is not clear. We refer to [START_REF] Carmichael | State parameter estimation for nonlinear systems[END_REF][START_REF] Quinn | An approach to non-linear control problem using fixed-point methods, degree theory and pseudo-inverses[END_REF][START_REF] Curtain | An introduction to infinite dimensional linear systems theory[END_REF].

Definition 1 Let H be the operator defined by:

H : X → L 2 (0, T ; Y ), (Hx)(t) = Πx(t) = ΠS(t)φ(0). The system (2) is said initially observable if ker H = {0}, that is the left inverse H -1 exists. It is said contiuously initially observable if H -1 is bounded.
Note that the adjoint operator H * is given by

H * : L 2 (0, T ; Y ) → X, H * y(.) = T 0 S * (t)Π * y(t)dt.
This gives that the system (2) is contiuously initially observable iff the dual system is exactly controllable.

It is well known that a necessary condition of exact controllability is that the corresponding semigroup is onto for all t ≥ 0 (cf. for example [START_REF] Louis | On exact controllability in Hilbert space[END_REF][START_REF] Rabah | Commandabilité des systèmes linéaires à retard constant dans les espaces de Banach[END_REF][START_REF] Rabah | Exact controllability and complete stabilizability for linear systems in Hilbert spaces[END_REF]). That is a necessary condition of continuous initial observability is that the operators S * (t) are onto. Hence, the system (2) can never be continously initially observable if the semigroup S(t) is analytical or compact in an infinite dimensional Hilbert space. The assumptions in the main result of [START_REF] Choi | Continuous initial observability of nonlinear delay parabolic equations[END_REF] are contradictory.


F Delahaye

Chu Vh

Gordon Dl

Hannan Mm

Kanj Ss

Lejko-Zupanc

Mestres Ca

Pachirat O 12

P Pappas

Lamas C 13

Tan R 15

Tattevin P 16

One-year outcome following biologic or mechanical valve replacement for infective endocarditis

Keywords:

Structured abstract

Background

Nearly half of patients require cardiac surgery during the acute phase of infective endocarditis (IE). We describe the characteristics of patients according to the type of valve replacement (mechanical or biological), and examine whether the type of prosthesis was associated with in-hospital and 1-year mortality.

Methods and Results

Among 5,591 patients included in the International Collaboration on Endocarditis Prospective

Cohort Study, 1,467 patients with definite IE were operated on during the active phase and had a biological (37%) or mechanical (63%) valve replacement.

Patients who received bioprostheses were older (62 vs 54 years), more often had a history of cancer (9% vs 6%), and had moderate or severe renal disease (9% vs 4%); proportion of health care-associated IE was higher (26% vs 17%); intracardiac abscesses were more frequent (30% vs 23%). In-hospital and 1-year death rates were higher in the bioprosthesis group, 20.5% vs 14.0% (p=0.0009) and 25.3% vs 16.6% (p<.0001), respectively.

In multivariable analysis, mechanical prostheses were less commonly implanted in older patients (odds ratio: 0.64 for every 10 years), and in patients with a history of cancer (0.72), but were more commonly implanted in mitral position (1.60).

Bioprosthesis was independently associated with 1-year mortality (hazard ratio: 1.298).

Conclusions

Patients with IE who receive a biologic valve replacement have significant differences in clinical characteristics compared to patients who receive a mechanical prosthesis. Biologic valve replacement is independently associated with a higher in-hospital and 1-year mortality, a result which is possibly related to patient characteristics rather than valve dysfunction.

INTRODUCTION

Despite improvements in diagnosis, antibiotic treatment and surgery, infective endocarditis (IE) remains a serious disease, with 50% of patients requiring cardiac surgery during the acute phase of IE and a 20% in-hospital mortality.[1-3] Cardiac surgery for IE typically involves valve replacement with a mechanical or xenograft biologic prosthesis, although valve repair and homograft replacements may be used. The main advantage of mechanical prostheses is their longevity, but they require lifelong treatment with anticoagulants and the subsequent bleeding risks. Bioprostheses do not require long-term anticoagulation, but have a shorter durability, particularly in the mitral position. In its 2009 guidelines on IE, the European Society of Cardiology did not favour any specific valve substitute but recommended a tailored approach for each individual patient and clinical situation. [START_REF] Habib | Guidelines on the prevention, diagnosis, and treatment of infective endocarditis (new version 2009): The task force on the prevention, diagnosis, and treatment of infective endocarditis of the european society of cardiology (ESC). Endorsed by the european society of clinical microbiology and infectious diseases (ESCMID) and the international society of chemotherapy (ISC) for infection and cancer[END_REF] The American College of Cardiology and the American Heart Association Valvular Disease Guidelines have stated that in general, a mechanical prosthesis is reasonable in patients under 65 years of age, while a bioprosthesis is favored in patients 65 years of age or older for both the aortic and the mitral positions, but do not provide specific recommendations for surgery in IE. [START_REF] Bonow | focused update incorporated into the ACC/AHA 2006 guidelines for the management of patients with valvular heart disease: A report of the american college of cardiology/american heart association task force on practice guidelines (writing committee to revise the 1998 guidelines for the management of patients with valvular heart disease): Endorsed by the society of cardiovascular anesthesiologists, society for cardiovascular angiography and interventions, and society of thoracic surgeons[END_REF] There are limited data to support the choice of either type of prosthesis in IE. [START_REF] Newton | What type of valve replacement should be used in patients with endocarditis?[END_REF] The characteristics of patients receiving biological or mechanical prosthesis and the association between type of valve prosthesis and outcome are not clearly defined. Thus, the objectives of this observational study were to describe the characteristics of patients according to the type of prosthesis and to examine the relationship between prosthesis type and 1-year mortality. A standard case report form was used at all sites to collect data. The case report form included 275 variables and was developed by ICE according to standard definitions. [START_REF] Cabell | Progress toward a global understanding of infective endocarditis. Early lessons from the international collaboration on endocarditis investigation[END_REF] Data were collected during the index hospitalization and then entered at the coordinating centre or by site investigators using an Internet-based data entry system. Clinical characteristics including demographics, comorbid conditions, pre-existing valvular conditions, details regarding the current episode of IE (including source of acquisition, [START_REF] Friedman | Health care-associated bloodstream infections in adults: A reason to change the accepted definition of community-acquired infections[END_REF][START_REF] Benito | Health care-associated native valve endocarditis: Importance of non-nosocomial acquisition[END_REF] microbiology and echocardiography findings, complications, management, and outcome) were collected. All sites were queried to obtain 1-year outcome data for survival, with use of national death indices, medical records, or patient contact, as available.

METHODS

International Collaboration on Endocarditis -Prospective Cohort Study

Statistical analysis

The outcomes of interest in this study were in-hospital and 1-year mortality. Data are presented as means (standard deviations) for continuous variables and as frequencies (percentages) for categorical variables. Simple comparisons were made with the Wilcoxon rank-sum test or the Chi-square test as appropriate.

A generalized estimating equation method was used to determine factors that predicted implantation of a biological or a mechanical prosthesis. Variables found to have an association with the outcome of interest (p<0.05) on univariable analysis were considered for the final model in a backwards stepwise fashion. The final parameter estimates were converted to odds ratios (OR) with corresponding 95% confidence intervals (CI).

A proportional hazards regression model was used to determine if prosthesis type was associated with 1-year mortality. Variables that differed significantly (p<0.05) between the two prosthesis groups in univariable analysis and clinically sound variables were considered for the final model. Survival times were censored at 1 year or date of last contact. Risk estimates are presented as hazard ratios and 95% CI. Survival curves were produced by plotting the estimated survival distribution obtained from the proportional hazards regression model, stratified by type of prosthesis. Influence of age was studied both per ten-year intervals and with a cutoff of 65 years according to the ACC-AHA valvular disease guidelines.

A C C E P T E D M A N U S C R I P T

All tests were 2-sided, and statistical significance was determined at the 0.05 level. All statistical analyses were performed using SAS version 9.2 (SAS Institute, Cary, NC).

RESULTS

There were 5,668 patients with definite and possible IE enrolled in the ICE-PCS.

Based on pre-specified inclusion and exclusion criteria for this study, 1,467 patients, including 917 (63%) who received mechanical prostheses only and 550 (37%) who received bioprostheses only, were included in this study (Figure 1). 2).

After covariate adjustment, 1-year mortality estimates for biologic and mechanical prostheses were 24.7% and 20.5%, respectively (p = 0.0362).

DISCUSSION

In the present study, 1,467 patients received valve prostheses during the acute phase of IE with 37% receiving biologic valve replacement and 63% a mechanical prosthesis. Both inhospital and one-year mortality were higher in the bioprosthesis group. The higher mortality associated with bioprosthesis extended beyond the in-hospital acute phase of IE, and was independently associated with 1-year mortality in multivariable analysis. These results have relevance to current clinical practice, as biologic valve replacements were used in approximately 60% of valve replacement surgeries for IE in the United States from 2002 to

2008.[12]

A C C E P T E D M A N U S C R I P T

A few randomized trials have compared the outcome of biological versus mechanical prostheses, but none have included patients with IE. [START_REF] Bloomfield | Twelve-year comparison of a Bjork-Shiley mechanical heart valve with porcine bioprostheses[END_REF][START_REF] Hammermeister | Outcomes 15 years after valve replacement with a mechanical versus a bioprosthetic valve: Final report of the Veterans Affairs randomized trial[END_REF][START_REF] Vallejo | Long-term experience with multivalve replacement with the Medtronic-Hall mechanical prosthesis[END_REF] In a Veterans' Administration trial involving 575 patients undergoing single aortic or mitral valve replacement randomized to receive a biological or mechanical valve, the 15-year mortality after aortic valve replacement was higher with a bioprosthesis than mechanical prosthesis, but not after mitral valve replacement. [START_REF] Hammermeister | Outcomes 15 years after valve replacement with a mechanical versus a bioprosthetic valve: Final report of the Veterans Affairs randomized trial[END_REF] Bloomfield et al. randomized 533 patients to biological or mechanical prosthesis, and there was a non significant trend toward higher mortality after 12 years with the bioprosthesis. [START_REF] Bloomfield | Twelve-year comparison of a Bjork-Shiley mechanical heart valve with porcine bioprostheses[END_REF] However, in a meta-analysis of three trials, 5-year and 11-year mortality were not statistically different between the two types of prosthetic valves. [START_REF] Kassai | Comparison of bioprosthesis and mechanical valves, a meta-analysis of randomised clinical trials[END_REF] Other observational studies have compared the results of biologic or mechanical valve prosthesis for IE. In a previous study of 185 patients who received a valve prosthesis during the acute phase of IE, the 4-year mortality was higher in the bioprosthesis group. [START_REF] Reul | Bioprosthetic versus mechanical valve replacement in patients with infective endocarditis[END_REF] In a small study of patients undergoing aortic valve replacement for aortic valve IE, 5-year mortality of patients who received biologic replacements (bioprostheses or homografts) was two-fold higher than for patients who received mechanical valve replacement, yet the increased mortality was evident only in patients less than 65 years of age. [START_REF] Nguyen | Aortic valve replacement for active infective endocarditis: 5-year survival comparison of bioprostheses, homografts and mechanical prostheses[END_REF] Other studies have found no significant difference in mortality for biologic compared to mechanical valve replacement, but a higher rate of reoperation in younger patients who received biologic prosthesis. [START_REF] Moon | Treatment of endocarditis with valve replacement: The question of tissue versus mechanical prosthesis[END_REF][START_REF] Wos | Results of mechanical prosthetic valve replacement in active valvular endocarditis[END_REF] In a recent, retrospective study of patients on dialysis with IE who underwent valve surgery, no difference in longer term mortality was evident between type of valve prosthesis. [START_REF] Leither | Long-term survival of dialysis patients with bacterial endocarditis undergoing valvular replacement surgery in the United States[END_REF] However, this cohort included patients treated with surgery beyond the acute phase of IE and the very high one-year mortality rate may have overshadowed any valve-related effect. [START_REF] Leither | Long-term survival of dialysis patients with bacterial endocarditis undergoing valvular replacement surgery in the United States[END_REF] In the current study, the increased in-hospital and 1-year mortality associated with biologic valve replacement was evident only in patients younger than 65 years of age. This

A C C E P T E D M A N U S C R I P T

early, increased mortality in younger patients was a surprising finding. Furthermore, the odds ratio associated with bioprosthetic valve type was modest relative to other variables related to 1-year mortality. Although it is unlikely that biologic prostheses had valve degeneration or failure within 1-year follow up, data regarding post-operative echocardiographic assessment of the prostheses were not available. The selection of mechanical or biologic prosthetic valve in the setting of IE involves multiple considerations, including surgeon's preference and experience, size and expected hemodynamics of the prosthetic valve, patient's predicted longevity and valve durability, and risk of bleeding complications related to long-term anticoagulation. Although biologic valve replacement remained statistically associated with higher mortality after adjustment for certain chronic medical conditions, other variables which may have influenced type of valve prosthesis were not available for analysis in this study. This study has several other limitations. Since this is an observational study, the results are subject to selection bias such that unidentified variables may have influenced surgical decision-making regarding the type of prosthesis implanted. We could not ascertain whether in-hospital or 1-year mortality was due to a mechanical cardiac, infectious, or unrelated cause. Data regarding the use of anticoagulation after valve replacement and relapse of IE were not collected in this study, yet may have influenced outcome.

Implantation of a biologic prosthesis in

A C C E P T E D M A N U S C R I P T

In conclusion, in a large, contemporary cohort of patients undergoing valve replacement surgery for active IE, bioprosthetic valve replacement was associated with higher in-hospital and 1-year mortality, particularly in patients younger than 65 years of age. Further

  a younger patient may reflect other comorbid condition with reduced expected survival. On the other hand, among patients > 65 years of age, other medical conditions may be a greater determinant of mortality than the type of prosthesis implanted. The low C-statistic for the survival model may also indicate that baseline clinical characteristics associated with the acute IE episode are NOT strongly associated with 1 year survival in patients treated with surgery. Previous survival analyses have focused largely on in-hospital or shorter term mortality, but intermediate term mortality may be related to other factors not captured at baseline.

Figure 1 -Figure 2 -

 12 Figure 1 -Disposition of subjects enrolled in the ICE-PCS cohort

Fig. 2 A

 2 Fig. 2

Patient Selection, Data Collection and Outcomes

	Data from the International Collaboration on Endocarditis -Prospective Cohort Study
	(ICE-PCS) were used for this study. Methods of this prospective, multicenter, international
	registry of IE have been previously reported.[7, 8] Between January 2000 and December
	2006, 5,668 patients from 64 centres in 28 countries were enrolled. The ICE-PCS database is maintained at the Duke Clinical Research Institute, which serves as the coordinating centre for ICE studies, with institutional review board approval from Duke University School of Medicine. All patients from sites meeting criteria for participation were included in ICE-PCS. Sites had to meet the following criteria: (1) minimum enrolment of 12 cases per year in a centre with access to cardiac surgery; (2) patient identification procedures in place to ensure consecutive enrolment and to minimize ascertainment bias; (3) high-quality data, including M A N U S C R I P T query resolution; and (4) institutional review board and/or ethics committee approval or
	waiver based on local standards. Patients were identified prospectively and consecutively enrolled in ICE-PCS if they met criteria for possible or definite IE based on modified Duke criteria.[9] Only the first episode of IE recorded for an individual patient was used in the analysis. Patients with definite IE who underwent valve surgery during the active phase of IE and who had biological A C C E P T E D or mechanical valve replacement were included. Exclusion criteria were: age <18 years old;
	intravenous drug user; patients treated with valve repair rather than replacement or who
	received a homograft or an autograft; patients receiving both a mechanical prosthesis and a
	bioprosthesis and patients whose 1-year survival data were missing.

  Only three variables independently predicted the implantation of a biological or a mechanical prosthesis. Compared to bioprostheses, mechanical prostheses were less commonly implanted in patients with increased age (OR: 0.64 for every 10 years; 95% CI:

	0.561 -0.733), and in patients with a history of cancer (OR: 0.72; 95% CI: 0.526 -0.979), but were more commonly utilized in mitral valve replacements (OR: 1.60; 95% CI: 1.289 -1.996). Multivariable analysis of 1-year mortality predictors is presented in Table 2. Bioprosthesis use was independently associated with 1-year mortality; the risk of death was M A N U S C R I P T increased by 30% (hazard ratio: 1.298 [1.011 -1.665]; p = 0.0406). The hazard ratio was
	bioprostheses were less commonly implanted (34% vs 66%; p=0.002). Intracardiac abscesses A C C E P T E D
	were more frequent in the bioprosthesis group (30% vs 23%; p=0.0044). Both in-hospital and
	1-year death rates were higher in the bioprosthesis group, 20.6% vs 14.0% (p=0.0009) and
	25.3% vs 16.6% (p<.0001), respectively. For patients undergoing isolated aortic valve
	replacement, 1-year mortality after biologic versus mechanical valve replacement was 21.9%
	and 13.1% respectively; for patients undergoing isolated mitral valve replacement, 1-year
	mortality after biologic valve replacement was 26.3% compared to 20.3% for mechanical
	valve replacement.

The clinical characteristics of patients receiving biologic or mechanical prostheses are presented in Table

1

. Compared to patients who received mechanical prostheses, those who received bioprostheses were older (61.6 SD 15.2 vs 53.6 SD 15.2 years; p<.0001), more often had a history of cancer (9% vs 6%; p=0.009) and moderate or severe renal disease (9% vs 4%; p<0.001). A higher proportion of bioprostheses were used in North and South America whereas in other regions of the world, mechanical prostheses were more frequently implanted.

There were a higher proportion of health care-associated IE cases in the bioprosthesis group (26% vs 17%; p<.0001). For aortic valve replacement, bioprostheses were implanted more frequently than mechanical prostheses (61% vs 39%; p=0.06) whilst for mitral valve surgery, significantly higher in patients < 65 years of age (1.620 [1.123-2.339]) but not in patients ≥ 65 years of age (0.845 [0.596-1.199]). Kaplan-Meier 1-year mortality estimates were 28.4% in the bioprosthesis group and 19.7% in the mechanical prosthesis group (p < 0.001) (Figure

Table 1 -Comparison of patients who received biological or mechanical prostheses

 1

	Variable	Level	Overall	Mechanical	Bioprosthetic P-value
			N	%	N	%	N	%
	Total		1467	100	917	62.5	550	37.5
	Age < 65 years old		950	64.8	682	71.8	268	28.2	<.0001
	Age ≥ 65 years old		517	35.2	235	45.4	282	54.6
	Age (N=1466)	Mean	1466	56.63	917	53.62	549	61.65	<.0001
		STD		15.66		15.16		15.21
	Gender (N=1465)	Men	1053	71.88	665	72.68	388	70.55	0.3794
	Region (N=1467)	North America	199	13.57	82	8.94	117	21.27
		South America	157	10.70	69	7.52	88	16.00
		Australia/New	227	15.47	156	17.01	71	12.91	<.0001
		Zealand/Africa
		Europe	830	56.58	571	62.27	259	47.09
		Asia/Mid East	54	3.68	39	4.25	15	2.73

Table 2 -Parameters independently influencing 1-year mortality (multivariable analysis)

 2

	Parameter	Hazard ratio 95% confidence limits p-value
	Biological vs. mechanical prosthesis	1.298	1.011 -1.665	0.0406
	Age in ten-year intervals	1.278	1.164 -1.404	<.0001
	Type of IE: prosthetic valve	1.312	1.012 -1.700	0.0404
	Elevated C-reactive protein	0.681	0.520 -0.891	0.0050
	Diabetes mellitus	1.461	1.110 -1.922	0.0069
	Haemodialysis-dependent	2.278	1.514 -3.428	<.0001
	Viridans group streptococci	0.577	0.381 -0.875	0.0096
	Healthcare-associated IE	1.430	1.082 -1.889	0.0118
	Mitral valve vegetation	1.542	1.217 -1.956	0.0003
	Congestive heart failure	1.681	1.322 -2.139	<.0001
	Intracardiac abscess	1.697	1.318 -2.184	<.0001
	Persistent positive blood cultures	1.575	1.080 -2.298	0.0184
	Europe vs. other regions	1.869	1.411 -2.476	<.0001
	C-index = 0.491

Acknowledgments

In addition to all of the named ICE investigators at each site, we would like to acknowledge the support given to this project from all of the personnel at each site and at the coordinating centre that have allowed this project to move forward.

Prospective Cohort Study (ICE-PCS) Dr. Wang is supported in part by AHA Mid-Atlantic Grant-in-Aid Award #12GRNT12030071. Dr Kanj declared honoraria for talks from Pfizer, Merck, Astra Zeneca, Astellas, Biologix and research funds from Astellas.

Other authors declared no conflict of interest.

T.M. van der Meer, MD, PhD (University of Amsterdam). New Zealand: Stephen Chambers, MD, MSc (University of Otago), David Holland, MB, ChB, PhD (Middlemore Hospital), Arthur Morris, MD (Diagnostic Medlab), Nigel Raymond, MB, ChB (Wellington Hospital), Kerry Read, MB, ChB (North Shore Hospital). David R. Murdoch, MD, MSc, DTM&H (University of Otago). Romania: Stefan Dragulescu, MD, PhD, Adina Ionac, MD, PhD, Cristian Mornos, MD (Victor Babes University of Medicine and Pharmacy). Russia: O.M. Butkevich, PhD (Learning-Scientific Centre of Medical Centre of Russian Presidential Affairs Government Medical Centre of Russian). Natalia Chipigina, PhD, Ozerecky Kirill, MD, Kulichenko Vadim, Tatiana Vinogradova, MD, PhD (Russian Medical State University) Saudi Arabia: Jameela Edathodu, MBBS, Magid Halim,MBBS (King Faisal Specialist Hospital & Research Center). Singapore: Yee-Yun Liew, Ru-San Tan, MBBS (National Heart Centre). Slovenia: Tatjana Lejko-Zupanc, MD, PhD, Mateja Logar, MD, PhD, Manica Mueller-Premru, MD, PhD (Medical Center Ljublijana). South Africa: Patrick Commerford, MD, Anita Commerford, MD, Eduan Deetlefs, MD, Cass Hansa, MD, Mpiko Ntsekhe, MD (University of Cape Town and Groote Schuur Hospital). Spain: Manuel Almela, MD, Yolanda Armero, MD, Manuel Azqueta, MD, Ximena Castañeda, MD, Carlos Cervera, MD, PhD, Ana del Rio, MD, PhD, Carlos Falces, MD, PhD, Cristina Garcia-de-la-Maria, PhD, Guillermina Fita, MD, Jose M. Gatell, MD, PhD, Magda Heras MD, PhD Jaime Llopis, MD, PhD, Francesc Marco, MD, PhD, Carlos A. Mestres, MD, PhD, José M. Miró, MD, PhD, Asuncion Moreno, MD, PhD, Salvador Ninot, MD, Carlos Paré, MD, PhD, Joan M. Pericas, MD, Jose Ramirez, MD, PhD, Irene Rovira, MD, Marta Sitges, MD, PhD (Hospital Clinic -IDIBAPS. University of Barcelona, Barcelona, Spain). University of Barcelona, Barcelona, Spain). Ignasi Anguera, MD, PhD, Bernat Font, MD, Joan Raimon Guma, MD (Hospitál de Sabadell). Javier Bermejo, Emilio Bouza, MD, PhD, Miguel Angel Garcia Fernández, MD, A C C E P T E D M A N U S C R I P T

No significant difference between the two groups for the following parameters:

A C C E P T E D M A N U S C R I P T