BRICSRS-94-43Aceto&Jeffrey:ACompleteAxiomatizationofTimedBisimulation
BRICS
Basic Research in Computer Science
A Complete Axiomatization of
Timed Bisimulation for a Class of Timed Regular Behaviours
(Revised Version)
Luca Aceto Alan Jeffrey
BRICS Report Series RS-94-43
ISSN 0909-0878 December 1994
Copyright c 1994, BRICS, Department of Computer Science University of Aarhus. All rights reserved.
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.
See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:
BRICS
Department of Computer Science University of Aarhus
Ny Munkegade, building 540 DK - 8000 Aarhus C
Denmark
Telephone: +45 8942 3360 Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk
A complete axiomatization of timed bisimulation for a class of timed regular behaviours
(Revised version)
Luca Aceto
BRICS y
Department of Mathematics and Computer Science Aalborg University
Fredrik Bajersvej 7E 9220 Aalborg , Denmark
Alan Jerey
zSchool of Cognitive and Computing Sciences University of Sussex, Brighton BN1 9QH, UK
Abstract
One of the most satisfactory results in process theory is Milner's axiom- atization of strong bisimulation for regular CCS. This result holds for open terms with nite-state recursion. Wang has shown that timed bisimulation can also be axiomatized, but only for closed terms without recursion. In this paper, we provide an axiomatization for timed bisimulation of open terms with nite-state recursion.
Key words and phrases.
Complete axiomatizations, !-complete- ness, equational logic, timed bisimulation equivalence, regular processes, timed CCS.1 Introduction
Much research in concurrency theory has recently been devoted to the devel- opment of extensions of standard process algebras like CCS 16], CSP 11] and ACP 3] with constructs allowing for the modelling of timing aspects in the behaviour of processes. By now, most process algebras have a timed counter- part (see, e.g., 1, 6, 18, 21]), and the development of results and techniques for these languages is becoming comparable with that for the standard process description languages. For example, complete axiomatizations of behavioural
On leave from School of Cognitive and Computing Sciences, University of Sussex, Brighton BN1 9QH, UK. Email: luca@iesd.auc.dk.
yBasic Research in Computer Science, Centre of the Danish National Research Foundation.
zSupported by SERC project GR/H 16537. Additional funding was received from EC BRA 7166 . Email: alanje@cogs.susx.ac.uk.
congruences for subsets of timed process algebras have been presented in, e.g., 10, 14, 18, 22]|showing that behavioural congruences which deal with timing considerations are as mathematically tractable as the standard untimed ones.
Two of the most beautiful results in the theory of process algebras are the complete axiomatizations of strong bisimulation equivalence and observational congruence for regular CCS processes provided by Milner in his classic papers 15] and 17], respectively. These results have put the notions of behaviour used in the theory of CCS on an equal footing with the one common in formal language theory, and have contributed to the realization that the notion of processis at least as elegant and mathematically tractable as that of language.
The main purpose of this paper is to show that the techniques developed by Milner in 15, 17] can be adapted to provide a complete axiomatization of the notion of timed bisimulation equivalence, due to Wang Yi 21], over a class of regular timed CCS processes 12, 22]. More precisely, we shall oer a complete axiomatization of timed bisimulation over the language of action guarded reg- ular expressions studied in 12]. This complete axiomatization is obtained by combining an improved version of the laws which were shown in 22] to char- acterize timed bisimulation over nite trees with standard laws for recursively dened processes, viz, laws to unwind recursive denitions of expressions, and a version of unique xed-point induction.
The paper is organized as follows. Section 2 is devoted to preliminaries, and background material on timed CCS and timed bisimulation. The axiomatiza- tion of timed bisimulation is presented and discussed in Section 3, where its soundness is also proved. The proof of completeness of the axiomatization is given in detail in Section 4, and relies on an adaptation of the techniques used by Milner in 15, 17].
As this is not an introductory paper on timed CCS, we have taken the liberty to refer the reader to the original papers by Wang Yi for motivations and examples. We hope, however, that the paper will still be suciently readable for the uninitiated reader.
2 Timed regular behaviours and timed bisimulation
The language for expressions that we shall consider in this paper is a generaliza- tion of the regular subcalculus of Wang Yi's timed CCS 21, 23]. This language has been investigated by Holmer, Larsen and Wang Yi in 12], and we shall mostly follow the notation and denitions given in that reference.
As usual, we shall assume a countably innite set of action names, ranged over by
a
andb
, and a distinguished action 62. Let Act = fg, be the set of actions, ranged over by and.Following 13], we dene a monoid (
X
+0) to be:left-cancellative i (
x
+y
=x
+z
))(y
=z
), andanti-symmetrici (
x
+y
= 0))(x
=y
= 0).Examples of left-cancellative anti-symmetric monoids include:
The singleton set (
1
+0).
The natural numbers (
N
+0).The non-negative rationals (
Q
++
0).
The non-negative reals (
R
++0).
The countable ordinals (
!
1+0).We can dene a partial order on
X
as:x
y
i 9z : x
+z
=y
It is simple to verify thatis a partial order if (
X
+0) is a left-cancellative anti-symmetric monoid. A time domain is a left-cancellative anti-symmetric monoid (Tim+0), ranged over byt
,u
andv
, such that is a total order.Dene:
t
^u
= the minimum oft
andu t
_u
= the maximum oft
andu
and whent
u
:t
;u
= the uniquev
such thatu
+v
=t
Let Tim+= Timnf0g be the set of positive delays, ranged over by
c
,d
ande
. Let Lab = Actf"
(c
)jc
2Tim+g be the set of labels, ranged over by . Let Var be a countably innite set of process variables, ranged over byx
,y
andz
.The set of regular process expressions over Act, Tim and Var is given by the following grammar:
E
::=0
jx
j:E
j"
(t
):E
jE
+E
jx
(x
=E
)The interested reader is referred to 21, 23] for intuition on the operators used in the above denition.
We shall assume the standard notions of free and bound variables in expres- sions, with
x
(x
= ) as the binding construct. The set of free variables in an expressionE
is denoted by fvE
. Throughout this paper we shall restrict our- selves to considering regular process expressions in which recursions are action guarded, a notion that is dened below.Denition
A variablex
is action guarded inE
ix
2AG
(E
), dened:AG
(0
) = VarAG
(x
) = Varnfx
gAG
(:E
) = VarAG
("
(t
):E
) =AG
(E
)AG
(E
+F
) =AG
(E
)\AG
(F
)AG
(x
(x
=E
)) =AG
(E
)fx
gA regular process expression
E
is well-formed i for every subexpression ofE
of the formx
(x
=F
),x
is action guarded inF
.0
;";(!c)0 :P
;!P a:P
;";(!c)a:P
"
(c
+t
):P
;";(!c)"
(t
):P P
;";(!c)P
0"
(t
):P
;";(t;+!c)P
0P
;!P
0"
(0):P
;!P
0P
;!P
0P
+Q
;!P
0Q
;!Q
0P
+Q
;!Q
0P
;";(!c)P
0Q
;";(!c)Q
0P
+Q
;";(!c)P
0+Q
0E
fx
(x
=E
)=x
g;!P
x
(x
=E
);!P
Figure 1: The operational semantics for
TC
0For example, the expression (
x
(x
=:x
))+y
is well-formed, while the expres- sionx
(x
="
(c
):x
) is not. The above denition departs slightly from the one given in 12, Denition 2.1]. In particular, the expression (x
(x
=:x
)) +y
would not be well-formed according to the denition of 12] because the free variabley
does not occur within a subexpression of the form:F
.The set of all well-formed regular process expressions is
TC
, ranged over byE
,F
andG
. The set of all closed, well-formed regular process expressions isTC
0, ranged over byP
,Q
andR
. Elements of this set will often be referred to as processes.Following Milner 17], we shall identify expressions which dier only by the renaming of bound variables. We shall also write
E
fF
1:::F
n=x
1:::x
ng for the result of simultaneously substitutingF
i for each free occurrence ofx
i inE
, renaming bound variables as necessary.The operational semantics for
TC
0is given by the labelled transition system (TC
0Lab!) in Figure 1. The interested reader is referred to 21, 23] for comments on the rules. Note that, following Wang Yi 21, 23],"
(0) has been excluded from the semantics of processes.To conclude this introductory section, we shall now dene the notion of timed bisimulation equivalence21].
Denition
A relation RoverTC
0 is atimed bisimulation iP
RQ
implies, for all :whenever
P
;!P
0 then, for someQ
0,Q
;!Q
0 andP
0RQ
0.whenever
Q
;!Q
0 then, for someP
0,P
;!P
0 andP
0RQ
0.The relation of timed bisimulation equivalence, denoted by , is the largest timed bisimulation.
The interested reader is referred to the aforementioned papers by Wang Yi, and to 12] for intuition and examples of processes that are equivalent or inequivalent
with respect to . The denition of can be extended to expressions in the standard way as follows:
Denition
LetE
andF
be expressions with free variables inx
~=x
1:::x
m. ThenE
F
i for all vectors ~P
=P
1:::P
m,E
fP=
~x
~gF
fP=
~x
~g.Proposition 1 (21, Theorem 5.1])
Timed bisimulation equivalence forms a congruence overTC
.In the remainder of this paper, we shall present a complete axiomatization of
over
TC
.3 Axiomatization and soundness
In 21] various equational laws were proved to hold for Wang Yi's timed CCS modulo timed bisimulation equivalence, and in 22] a set of such axioms was shown to be complete over the language of recursion-free
TC
0 processes with delays from the time domain of the positive reals. We shall now present an axiomatization which will be proven complete forover the whole ofTC
, i.e., complete for regular process expressions with action guarded recursion. The detailed proof of completeness occupies Section 4 of this paper.Wang's axiomatization for recursion-free
TC
0 processes is given by the ax- iom systemF in Figures 2 and 3. Our axiomatization for regularTC
processexpressions is given by the axiom systemE in Figures 2 and 4.
The axioms (S1){(S4) are the standard laws for a complete axiomatization of strong bisimulation equivalence over nite trees 9]. Together with axioms (R1) and (R2), these form a complete axiomatization of strong bisimulation equivalence for guarded regular CCS terms 15]. (In fact, the axiomatization in 15] can be obtained as a special case of that in Figure 2 by taking the time domain to be the singleton set (
1
+0).)
The axioms (TD), (TA) and (T0) correspond to the operational properties of time determinacy, time additivity and zero delay. These axioms are present in Wang's 21, 22] axiomatization. As we shall see in Section 4, the axiom systemGgiven in Figure 2 is powerful enough to prove Milner's 15] Equational Characterization Theorem for timed regular expressions. However, G is not powerful enough to give a complete axiomatization for recursion-free timed expressions.
Wang 21, 22] added the axioms (MP), (AP) and (NP) to G to provide a complete axiomatization for recursion-free
TC
0 processes. These axioms cor- respond to the operational properties of maximal progress and persistency, and are discussed in detail by Wang. However, the resulting axiom system F, given in Figure 3, is not powerful enough to give a complete axiomatization for recursion-freeTC
process expressions.Our axiomatization replaces (AP) and (NP) with one new persistency axiom (P). In Section 4 we show thatE is complete for timed bisimulation equivalence over
TC
process expressions. In Section 5 we show that E is strictly stronger than F, and thus that Wang's axiomatization is not complete for openTC
process expressions.
(S1)
E
+F
=F
+E
(S2)
E
+ (F
+G
) = (E
+F
) +G
(S3)
E
+E
=E
(S4)
E
+0
=E
(TD)
"
(t
):
(E
+F
) ="
(t
):E
+"
(t
):F
(TA)
"
(t
+u
):E
="
(t
):"
(u
):E
(T0)
"
(0):E
=E
(R1)
x
(x
=E
) =E
fx
(x
=E
)=x
g(R2) If
F
=E
fF=x
g, thenF
=x
(x
=E
), ifx
is action guarded inE
Figure 2: The axiom systemG(MP)
:E
+"
(c
):F
=:E
(AP)
a:E
+"
(t
):a:E
=a:E
(NP)
"
(t
): 0
=0
Figure 3: The axiom systemF is G plus (MP), (AP) and (NP)
(MP)
:E
+"
(c
):F
=:E
(P)
E
+"
(t
):E
=E
Figure 4: The axiom systemE is G plus (MP) and (P)
We shall write E `
E
=F
whenE
=F
may be proved from E together with the structural rules for = to be a congruence, and similarly forF `E
=F
andG `E
=F
.To conclude this section, we shall show thatE is indeed sound with respect to timed bisimulation equivalence over
TC
.Proposition 2 (Soundness)
For allTC
expressionsEF
, E `E
=F
im- pliesE
F
.Proof
. All the laws in E have been shown sound by Wang Yi in 22]. The only exception is the persistency axiom (P), the soundness of which is established by the timed bisimulation:(f(
Q
+PQ
)j9c : P
;";(!c)Q
gf(PP
)jP
2TC
0g)where denotes composition of relations. The proof that this relation is a bisimulation depends on the properties of time determinacy, time additivity and persistency of the operational semantics for
TC
0, and the soundness of(T0). (The interested reader is referred to 21] and 20] for details on these
properties). 2
4 Completeness
In this section, we shall present the proof of completeness of the set of lawsE over
TC
. The structure of the proof of this result will follow closely the most beautiful arguments used by Milner in 15, 17] to prove the completeness of the axiomatizations for strong bisimulation and observational congruence over regular CCS processes.The structure of the completeness proof will be as follows: rst of all, we shall show that every
TC
expressionE
provably satises a certain kind of equa- tion set. This is what Milner calls the Equational Characterization Theorem.Next, we shall show that if
E
F
andE
provably satises an equation set, whileF
provably satises another equation set, then bothE
andF
provably satisfy a common equation set. Finally, we show that whenever twoTC
ex- pressions provably satisfy the same equation set, then E proves that they are equal.Denition
An equation set ~x
= ~E
is a nite non-empty sequence of declara- tionsx
1 =E
1:::x
n =E
n, where thex
is are pairwise distinct variables, and theE
is areTC
expressions.A vector ~
F
=F
1:::F
n satises ~x
= ~E
i 8i : F
iE
ifF=
~x
~g.For an equational theory T, a vector ~
F
=F
1:::F
n T-provably satisesx
~= ~E
i 8i :
T `F
i=E
ifF=
~x
~g.An expression
E
(T-provably) satisesx
~ = ~F
i we can nd a vector ~E
which (T-provably) satises ~x
= ~F
andE
E
1 (T `E
=E
1).We refer to
x
1 as the leading variable of the equation setx
~= ~F
. For example, the equation set:x
1="
(1):a:x
2+"
(3):y x
2 ="
(2):b:x
1 (1) is satised byx
(z
="
(1):a:"
(2):b:z
+"
(3):y
).Denition
An equation setx
~= ~E
is standard i eachE
i is of the form:X
j2Ji
"
(t
j):
j:x
j+ Xk2Ki
"
(u
k):w
kwhere the vectors
x
~ andw
~ are disjoint. By convention, we indentify eachE
iwith
0
when the index setsJ
i andK
i are both empty. We callx
~ the formal variables ofx
~= ~E
, andw
~ the free variables of ~x
= ~E
.For example, the above equation set (1) is standard, but the following is not:
x
1="
(1):x
2+"
(3):y x
2 =a:"
(2):b:x
1Proposition 3
Ifx
~ = ~E
is standard andw
is not a formal variable, then we can nd a standardx
~= ~F
such that 8i :
G `F
i =E
ifE
1=w
g.Proof
. Dene ~F
as:F
i Xj2Ji
"
(t
j):
j:x
j+Xk2Ki wk6=w
"
(u
k):w
k+X
k2Ki wk=w j02J1
"
(u
k+t
j0):
j0:x
j0+Xk2Ki wk=w k02K1
"
(u
k +u
k0):w
k0It is simple to show that this is standard, and that8
i :
G`F
i =E
ifE
1=w
g. 2Proposition 4
Ifx
is action guarded inE
and G `E
=F
thenx
is action guarded inF
.Proof
. Show thatAG
( ) is a model for the equational theoryG. 2Proposition 5
We shall use the following standard results about substitution:1.
G
fF=
~x
~gfE=w
gG
fE=w
gfF
~fE=w
g= x
~g, ifw
does not occur inx
~, andx
~ are not free inE
.2.
F
fG=w
gfE=
~x
~gF
fG
fE=
~x
~g=w
gfE=
~x
~g, ifx
~ are not free in ~E
.Proof
. Routine structural induction. 2Theorem 6 (Equational Characterization)
For anyE
we can nd a stan- dard equation setx
~ = ~G
whichE
G-provably satises. MoreoverE
and the equation setx
~= ~G
have the same free variables.Proof
. An induction onE
. The only dicult case is whenE
x
(w
=F
).In this case, by induction we nd a ~
x
= ~H
whichF
G-provably satises, and wlog we can assume thatw
is not a formal variable of ~x
= ~H
, and that ~x
are not free inE
. Thus we have a ~F
such that:G`
F
1 =F
(2)8
i :
G`F
i =H
ifF=
~x
~g (3) Dene:E
iF
ifE=w
g (4)Let ~
G
be the standard equation set given by Proposition 3 such that:G`
G
i=H
ifH
1=w
g (5) Sincew
is action guarded inF
, by Proposition 4 it must be action guarded inH
1fF=
~x
~g, so, asw
62x
~, must be action guarded inH
1, so cannot be free inH
1. Then:G`
E
=
F
fE=w
g (R1)=
F
1fE=w
g (2)=
E
1 (4)and:
G `
E
1=
F
1fE=w
g (4)=
H
1fF=
~x
~gfE=w
g (3)=
H
1fE=w
gfF
~fE=w
g= x
~g (Propn 5.1)=
H
1fE=w
gfE=
~x
~g (4)=
H
1fE=
~x
~g (w
62fvH
1)and so:
G`
E
i=
F
ifE=w
g (4)=
H
ifF=
~x
~gfE=w
g (3)=
H
ifE=w
gfF
~fE=w
g= x
~g (Propn 5.1)=
H
ifE=w
gfE=
~x
~g (4)=
H
ifH
1fE=
~x
~g=w
gfE=
~x
~g (above)=
H
ifH
1=w
gfE=
~x
~g (Propn 5.2)=
G
ifE=
~x
~g (5)Thus we have found a standard ~
x
= ~G
whichE
G-provably satises. 2 Theorem 6 shows that every expressionE
inTC
G-provably satises a standard equation set ~x
= ~G
. The second stepping stone towards the promised complete- ness theorem is a result showing that ifE
F
, whereF
G-provably satises a standard equation set ~y
= ~H
, then there exists a third standard equation setE-provably satised by both
E
andF
. Note that this part of the completeness proof requires the axioms (MP) and (P).Theorem 7
LetE
andE
0 be expressions inTC
such thatE
E
0. Assumethat
E
E-provably satises a standard equation setx
~ = ~F
, andE
0 E-provably satises a standard equation setx
~0= ~F
0. Then there exists a standard equation setE-provably satised by bothE
andE
0.Proof (Following Milner)
. Assume that:F
i Xj2Ji
"
(t
j):a
j:x
j+ Xk2Ki
"
(u
k)::x
k+ Xl2Li
"
(v
l):w
l (6)F
i00 Xj02Ji0 0
"
(t
0j0):a
j0:x
0j0+ Xk02Ki0 0
"
(u
0k0)::x
0k0 + Xl02L0i 0
"
(v
0l0):w
l00 (7) AsE
E-provably satises ~x
= ~F
andE
0 E-provably satises ~x
0 = ~F
0, we can nd ~E
and ~E
0such that:E
=E
(8)8
i :
E `E
i =F
ifE=
~x
~g (9)E `
E
0 =E
10 (10)8
i :
E `E
i0 =F
i0fE
~0= x
~0g (11) Let ~w
denote the set of free variables occurring in eitherE
orE
0. Choose a vector ~a
of distinct actions, one actiona
w for eachw
2w
~, that do not occur inE
andE
0. (This is always possible as the set of action names is countably innite.) Take the vector ~P
of processes given byP
wa
w: 0
. AsE
E
0, itfollows, in particular, that
E
fP=
~w
~gE
0fP=
~w
~g. Thus, by (8) and (10), we have thatE
1fP=
~w
~gE
10fP=
~w
~g.Let R be the relation f(
ii
0)jE
ifP=
~w
~gE
i00fP=
~w
~gg, let ~z
be the vector of fresh variables fz
ii0 ji
Ri
0g (withz
11 as leading variable), and dene the vectors ~G
, ~H
and ~H
0 as:G
ii0 X j2Jij02Ji00 jRj0aj=a0j0"
(t
j _t
0j0):a
j:z
jj0+Xk2Kik2Ki00 kRk0
"
(u
k _u
0k0)::z
kk0+Xl2Lil02L0i0 wl=w0l0
"
(v
l_v
l00):w
l(12)H
ii0E
i (13)H
ii00E
i00 (14)Note that the equation set ~
z
= ~G
is standard by construction. We now show that the vector ~H
E-provably satises ~z
= ~G
. To this end, we prove, rst of all, that, for eachi
Ri
0, every summand ofG
ii0fH=
~z
~g can be absorbed intoH
ii0. We consider three cases, depending on the form taken by the summand ofG
ii0fH=
~z
~g.For any
i
Ri
0,j
2J
i andj
02J
i00 such thatj
Rj
0 anda
j =a
0j0:E`
H
ii0=
E
i (13)=
F
ifE=
~x
~g (9)=
F
ifE=
~x
~g+"
(t
j):a
j:E
j (S1{S3,6)=
F
ifE=
~x
~g+"
(t
j):
(a
j:E
j+"
((t
j_t
0j0);t
j):a
j:E
j) (P)=
F
ifE=
~x
~g+"
(t
j):a
j:E
j+"
(t
j):"
((t
j_t
0j0);t
j):a
j:E
j (TD)=
F
ifE=
~x
~g+"
(t
j):a
j:E
j+"
(t
j+ ((t
j_t
0j0);t
j)):a
j:E
j (TA)=
F
ifE=
~x
~g+"
(t
j):a
j:E
j+"
(t
j_t
0j0):a
j:E
j (t
+ (u
;t
) =u
)=
F
ifE=
~x
~g+"
(t
j_t
0j0):a
j:E
j (S1{S3,6)=
E
i+"
(t
j_t
0j0):a
j:E
j (9)=
H
ii0+"
(t
j _t
0j0):a
j:H
jj0 (13)=
H
ii0+"
(t
j _t
0j0):a
j:z
jj0fH=
~z
~g (substitution) Similarly, for anyi
Ri
0,k
2K
i andk
02K
i00 such thatk
Rk
0:E `
H
ii0 =H
ii0 +"
(u
k _u
0k0)::z
kk0fH=
~z
~g and for anyi
Ri
0,l
2L
i andl
02L
0i0 such thatw
l=w
0l0:E`
H
ii0 =H
ii0+"
(v
l_v
l00):w
lfH=
~z
~gWe remark here that the proof of the above equality makes an essential use of axiom (P), and could not have been carried out using Wang's persistency axioms (AP) and (NP).
Thus each summand of
G
ii0fH=
~z
~g can be absorbed intoH
ii0, and by (S1){(S4):
E`
H
ii0 =H
ii0+G
ii0fH=
~z
~g (15) We now show that the converse also holds, namely thatH
ii0 can be absorbed intoG
ii0fH=
~z
~g. To this end, by (9) and (13), it is sucient to prove that each summand ofF
ifE=
~x
~g can be absorbed intoG
ii0fH=
~z
~g. Again, we distinguish three cases depending on the form the summand takes.For any
i
Ri
0 andj
2J
i, either:
t
ju
k, for everyk
2K
i, or:there exists
k
2K
i such thatt
j> u
k. We proceed to show that in either case:E `
G
ii0fH=
~z
~g=G
ii0fH=
~z
~g+"
(t
j):a
j:x
jfE=
~x
~gCase 8
k
2K
i: t
ju
k. In this case, by the operational semantics forTC
0, it follows that:F
ifE=
~x
~gfP=
~w
~g;";(t!j);a!jE
jfP=
~w
~gAs
E
ifP=
~w
~gE
i00fP=
~w
~gand G is sound for, we have thatF
ifE=
~x
~gfP=
~w
~gF
i00fE=
~x
~0gfP=
~w
~gSo, as the actions in ~
a
were chosen to be fresh:F
i00fE
~0= x
~0gfP=
~w
~g;"(;t!j);a!jE
j00fP=
~w
~gfor some
j
0 witht
jt
0j0,a
j =a
0j0 andE
jfP=
~w
~gE
j00fP=
~w
~g. By the denition of the relationR, it follows thatj
Rj
0. Thus:E`
G
ii0fH=
~z
~g=
G
ii0fH=
~z
~g+"
(t
j_t
0j0):a
j:H
jj0 (S1{S3,12)=
G
ii0fH=
~z
~g+"
(t
j):a
j:H
jj0 (t
jt
0j0)=
G
ii0fH=
~z
~g+"
(t
j):a
j:E
j (13)=
G
ii0fH=
~z
~g+"
(t
j):a
j:x
jfE=
~x
~g (substitution)Case 9
k
2K
i: t
j> u
k. Choosek
such thatu
k is minimal in the setf
u
h jh
2K
ig. Then, by the operational semantics forTC
0:F
ifE=
~x
~gfP=
~w
~g;";(u;k!);!E
kfP=
~w
~g Therefore, as in the previous case, we have:F
iE
~= x
~P=
~w
~ "(u )E
kP=
~w
~for some
k
0 2K
i00 withu
ku
0k0 andk
Rk
0. In fact, by symmetry and the fact thatu
k is minimal in the set fu
h jh
2K
ig, it is easy to see thatu
k =u
0k0. Thus:E`
G
ii0fH=
~z
~g=
G
ii0fH=
~z
~g+"
(u
k_u
0k0)::H
kk0 (S1{S3,12)=
G
ii0fH=
~z
~g+"
(u
k)::H
kk0 (u
k =u
0k0)=
G
ii0fH=
~z
~g+"
(u
k):
(:H
kk0+"
(t
j ;u
k):a
j:H
jj0) (MP,t
j> u
k)=
G
ii0fH=
~z
~g+"
(u
k)::H
kk0+"
(u
k):"
(t
j ;u
k):a
j:H
jj0 (TD)=
G
ii0fH=
~z
~g+"
(u
k)::H
kk0+"
(u
k+ (t
j;u
k)):a
j:H
jj0 (TA)=
G
ii0fH=
~z
~g+"
(u
k)::H
kk0+"
(t
j):a
j:H
jj0 (t
+ (u
;t
) =u
)=
G
ii0fH=
~z
~g+"
(u
k_u
0k0)::H
kk0+"
(t
j):a
j:H
jj0 (u
k =u
0k0)=
G
ii0fH=
~z
~g+"
(t
j):a
j:H
jj0 (S1{S3,12)=
G
ii0fH=
~z
~g+"
(t
j):a
j:E
j (13)=
G
ii0fH=
~z
~g+"
(t
j):a
j:x
jfE=
~x
~g (substitution) Note that the above reasoning uses the equation (MP).Thus:
E `
G
ii0fH=
~z
~g=G
ii0fH=
~z
~g+"
(t
j):a
j:x
jfE=
~x
~gSimilarly, for any
i
Ri
0andk
2K
i, it is not too dicult to prove that:E`
G
ii0fH=
~z
~g=G
ii0fH=
~z
~g+"
(u
k)::x
kfE=
~x
~g We are now left to show that for anyi
Ri
0 andl
2L
i:E`
G
ii0fH=
~z
~g=G
ii0fH=
~z
~g+"
(v
l):w
lfE=
~x
~g (16) As before, we prove this statement by considering the following two sub-cases:
v
lu
k, for everyk
2K
i, or:there exists
k
2K
i such thatv
l> u
k.The proof of (16) when there exists
k
2K
i such thatv
l> u
k follows the lines spelled out in detail above. We shall thus concentrate on presenting a detailed proof of (16) in the casev
lu
k, for everyk
2K
i.Assume that