2.3.2　APTC with Left Parallel Composition

We provide the transition rules of APTC as follows，which are applicable to all truly concurrent behavioral equivalences，including pomset bisimulation，step bisimulation，hp-bisimulation and hhp-bisimulation.Where≬is the whole concurrency operator，‖is the parallel operator， is the left parallel operator，|is the communication merge， Θis the conflicts elimination operator，and ◁is the auxiliary unless operator.

The transition rules of left parallel compositionare presented as follows.With a little abuse，we extend the causal order relation≤on E to include the original partial order（denoted by ＜）and concurrency（denoted by=）.

The new axioms for parallelism are listed in Table 2.2.

Definition 2.22（Basic terms of APTC with left parallel composition）.The set of basic terms of APTC，denoted B（APTC），is inductively defined as follows：

（1）E ⊂B（APTC）.

（2）If e∈E and t∈ B（APTC），then e·t∈ B（APTC）.

（3）If t，s∈ B（APTC），then t+ s∈ B（APTC）.

（4）If t，s∈ B（APTC），then t s∈ B（APTC）.

Theorem 2.7（Generalization of the algebra for left parallelism with respect to BATC）.The algebra for left parallelism is a generalization of BATC.

Theorem 2.8（Congruence theorem of APTC with left parallel composition）.Truly concurrent bisimulation equivalences～ p，～ s，～hp，and～hhp are all congruences with respect to APTC with left parallel composition.

Theorem 2.9（Elimination theorem of parallelism with left parallel composition）.Let p be a closed APTC with left parallel composition term.Then there is a basic APTC term q such that APTC ├p=q.

Theorem 2.10（Soundness of parallelism with left parallel composition modulo truly concurrent bisimulation equivalences）.Let x and y be APTC with left parallel composition terms.If APTC ├x=y，then

（1）x～ s y.

（2）x～ p y.

（3）x～hp y.

（4）x～hhp y.

Theorem 2.11（Completeness of parallelism with left parallel composition modulo truly concurrent bisimulation equivalences）.Let x and y be APTC terms.

（1）If x～ s y，then APTC ├x=y.

（2）If x～ p y，then APTC ├x=y.

（3）If x～hp y，then APTC ├x=y.

（4）If x～hhp y，then APTC ├x=y.

The axioms of encapsulation operator are shown in Table 2.3.

Theorem 2.12（Conservativity of APTC with respect to the algebra for parallelism with left parallel composition）.APTC is a conservative extension of the algebra for parallelism with left parallel composition.

Theorem 2.13（Congruence theorem of encapsulation operator ∂ H）.Truly concurrent bisimulation equivalences～ p，～ s，～hp，and～hhp are all congruences with respect to encapsulation operator ∂ H.

Theorem 2.14（Elimination theorem of APTC）.Let p be a closed APTC term including the encapsulation operator ∂ H.Then there exists a basic APTC term q such that APTC ├p=q.

Theorem 2.15（Soundness of APTC modulo truly concurrent bisimulation equivalences）.Let x and y be APTC terms including encapsulation operator ∂ H.If APTC ├x=y，then

（1）x～s y.

（2）x～p y.

（3）x～hp y.

（4）x～hhp y.

Theorem 2.16（Completeness of APTC modulo truly concurrent bisimulation equivalences）.Let p and q be closed APTC terms including encapsulation operator ∂ H，then

（1）If p～ s q，then p=q.

（2）If p～ p q，then p=q.

（3）If p～hp q，then p=q.

（4）If p～hhp q，then p=q.