In this section we only consider branching bisimilarity ≃. In particular, the notion of normal form is understood with respect to ≃. Fix an arbitrary process definition and denote its size by d.
All the rest of this section is devoted to the proof of Lemma 43.
5.1 Proof of Lemma 43
The proof is by induction on n−k. The induction basis is for k=n. Whatever an admissible order is chosen, if k=n then it trivially holds that d-size(δ)≤d-size(X
k
), as the only possible γ-squeeze δ of X
n
is the empty process, whose weighted size is 0.
For the induction step, fix some k and an admissible order >, assuming that the lemma holds for all greater values of k, for all admissible orders.
Then fix a (
k−1)-unambiguous process
γ∈{
X
1…
X
k−1}
⊗, assuming that
γ has the greatest
k-extension, say
\(\gamma \cdot X_{k}^{a}\). The assumption guarantees existence of some
γ-squeeze of
X
k
, that is a process
δ satisfying
$$\begin{aligned} \gamma \cdot X_k^{a+1}\simeq \gamma \cdot X_k^a\cdot \delta. \end{aligned}$$
(16)
The proof is split into three cases:
-
a>0,
-
a=0 and X
k
has a γ-squeeze δ such that \(X_{k} \stackrel {}{\Longrightarrow }_{0} \delta\),
-
a=0 and X
k
has no γ-squeeze δ such that \(X_{k} \stackrel {}{\Longrightarrow }_{0} \delta\).
Consider the sequence of transitions
\(\gamma \cdot X_{k}^{a+1} \stackrel {}{\Longrightarrow }_{0} \gamma \cdot X_{k}^{a}\cdot \eta\) and assume that all transitions originating from
γ precede all transitions originating from
\(X_{k}^{a+1}\). Distinguish the very first transition of
X
k
, say
\(X_{k} \stackrel {}{\longrightarrow }_{0} \phi\), that decreases the exponent from
a+1 to
a:
$$ \gamma \cdot X_k^{a+1} \stackrel {}{\Longrightarrow }_0 \gamma \cdot X_k^{a+1}\cdot \theta \stackrel {}{\longrightarrow }_0 \gamma \cdot X_k^{a} \cdot {( \phi ||\theta)} \stackrel {}{\Longrightarrow }_0 \gamma \cdot X_k^{a} \cdot \eta. $$
(17)
Note that by Lemma 15 we have:
$$ \gamma \cdot X_k^{a+1} \simeq \gamma \cdot X_k^{a}\cdot {( \theta ||\phi)} . $$
(18)
Furthermore, as
\(\gamma \cdot X_{k}^{a+1}\) generates
θ, namely
\(\gamma \cdot X_{k}^{a+1} \stackrel {}{\Longrightarrow }_{0} \gamma \cdot X_{k}^{a+1} \cdot \theta\), and
a>0, we observe that
\(\gamma \cdot X_{k}^{a}\) generates
θ as well, and hence
$$\gamma \cdot X_k^{a} \simeq \gamma \cdot X_k^{a}\cdot \theta . $$
This allows us to obtain, using substitutivity and the equation (
18), a
γ-squeeze of
X
k
of size at most
d:
$$\gamma \cdot X_k^{a+1} \simeq \gamma \cdot X_k^{a}\cdot {( \theta ||\phi)} \ \simeq \ \gamma \cdot X_k^{a}\cdot \phi. $$
Knowing that
ϕ∈{
X
k+1…
X
n
}
⊗ and size(
ϕ)<
d, we easily deduce the required bound on the weighted size of
ϕ:
$${d}\text {-}\text {size}(\phi) \leq d \cdot d^{n-k-1} = d^{n-k} = {d}\text {-}\text {size}(X_k). $$
The proof of Case 1 is thus completed.
Case 2.1: a=0 and X
k
Has a γ-Squeeze δ such that \(X_{k} \stackrel {}{\Longrightarrow }_{0} \delta\)
This is the only case that we are not able to adapt to weak bisimilarity.
Recall that we have a fixed admissible order >, for which we should provide an estimation on the size of a
γ-squeeze
δ of
X
k
. The idea of the solution for this case is to do a proof for an admissible order >′ different than >, knowing that both orders are
k-consistent, which means that they agree on
k greatest elements. For instance, the two orders on the set {
A,
B,
C,
D,
E}:
$$A > B > C > D > E \quad\text{and} \quad A >' B >' D >' E >' C $$
are 2-consistent but not 3-consistent. The estimation on the size of a
γ-squeeze
δ will transfer easily to the original order >, as we will actually prove that size(
δ)≤
d. Our proof is based on the simple observation that if two orders are
k-consistent then for
l≤
k,
l-unambiguous prefixes with respect to both orders are the same, as well as squeezes of
X
l
.
The modified order, denoted >′, is any one that satisfies the following conditions:
1.
>′ is k-consistent with >, and
2.
all variables generated by X
k
are smaller with respect to >′ than all variables not generated by X
k
.
Note that the second condition is satisfiable: whenever
Y is generated by
X
k
and
Z is not, then there exists no sequence of decreasing transitions from
Y to
Z, thus
Y>
decr
Z is impossible. From now on we work with the order >′, so indexing of variables
X
i
, squeezes, normal forms, etc. are implicitly understood to be defined with respect to that order.
To make the notation more readable, we will constantly use symbols α,α′, etc. for processes containing exclusively variables smaller than X
k
that are not generated by X
k
, and symbols β,β′, etc. for those containing exclusively variables generated by X
k
.
Let
δ be a
γ-squeeze of
X
k
such that
\(X_{k} \stackrel {}{\Longrightarrow }_{0} \delta\). In the sequence of transitions
\(X_{k} \stackrel {}{\Longrightarrow }_{0} \delta\), distinguish the transition that makes
X
k
disappear, induced by a transition rule
\(X_{k} \stackrel {}{\longrightarrow }_{0} \omega\), say. We may thus write:
$$\begin{aligned} \gamma \cdot X_k\stackrel {}{\Longrightarrow }_0\gamma \cdot X_k\cdot \hat{\beta} \stackrel {}{\longrightarrow }_0\gamma \cdot {(\omega ||\hat{\beta})} \stackrel {}{\Longrightarrow }_{0}\gamma \cdot \delta \end{aligned}$$
(19)
for some process
\(\hat{\beta}\). Let nf(
γ⋅
X
k
)=
γ⋅
α⋅
β. As the first step we prove the following:
Recall that nf(
γ⋅
X
k
)=
γ⋅
α⋅
β and consider Bisimulation Game from the pair of processes
$$\gamma \cdot X_k \simeq \gamma \cdot \alpha \cdot \beta. $$
Suppose the first Spoiler’s move is
\(\gamma \cdot X_{k}\stackrel {}{\longrightarrow }_{0} \gamma \cdot \omega\), answered by a matching Duplicator’s move:
$$\begin{aligned} \gamma \cdot \alpha \cdot \beta \stackrel {}{\Longrightarrow }_0 \tau' \stackrel {}{\longrightarrow }_0 \tau. \end{aligned}$$
The sequence of transitions satisfies assumptions of Lemma 29:
γ⋅
α is unambiguous and
$$\tau \simeq \gamma \cdot \omega \simeq \gamma \cdot \alpha \cdot \bar{\beta} $$
for some
\(\bar{\beta}\) (the latter equivalence follows by Lemma 46). We apply Lemma 29 together with Lemma 31 and deduce that Duplicator has a matching move engaging only variables generated by
X
k
, thus of the form:
$$\begin{aligned} \gamma \cdot \alpha \cdot \beta \stackrel {}{\Longrightarrow }_0 \gamma \cdot \alpha \cdot ({\beta'||Y})\stackrel {}{\longrightarrow }\gamma \cdot \alpha \cdot ({\beta'||\theta}). \end{aligned}$$
(21)
Finally we use (
21) to provide a
γ-squeeze of
X
k
of size at most
d. Recall that (
21) is a matching Duplicator’s move, i.e.
$$\begin{aligned} \gamma \cdot \alpha \cdot ({\beta'||Y}) \simeq \gamma \cdot X_k, \qquad \gamma \cdot \alpha \cdot ({\beta'||\theta}) \simeq \gamma \cdot \omega. \end{aligned}$$
(22)
Using these two equivalences we derive the following sequence of equivalences:
$$\gamma \cdot X_k \simeq \gamma \cdot X_k\cdot \theta \simeq \gamma \cdot \alpha \cdot {(\beta'||Y||\theta)} \simeq \gamma \cdot \alpha \cdot {(\beta'||\theta ||Y)} \simeq \gamma \cdot ({\omega ||Y}). $$
The first one is due to the fact that
θ is generated by
X
k
. The second one is by substitutivity, using the first equivalence in (
22). The third one is simply commutativity of composition, and the last one is by substitutivity again, this time using the second equivalence in (
22).
The process ω, being the right-hand side of a transition rule, is of size smaller than d. Hence ω||Y is a γ-squeeze of size at most d. This completes the proof of Case 2.1.
Recall that we have a fixed admissible order >, for which we should provide an estimation on the weighted size of a
γ-squeeze
δ of
X
k
. As in Case 2.1, we will use in the proof an admissible order >′ different than >, namely an arbitrary admissible order >′ fulfilling the following conditions:
1.
>′ is k-consistent with >,
2.
all variables generated by X
k
are smaller with respect to >′ than all variables not generated by X
k
, and
3.
the orders > and >′ coincide on variables not generated by X
k
.
The first two conditions are exactly as before, the last one is added. Similarly as before, the conditions are satisfiable. Moreover, the estimation on the weighted size of a
γ-squeeze with respect to >′ easily transfers to the original order >. Indeed, by Lemma 47, a ⊑-minimal squeeze contains only variables not generated by
X
k
, and these variables are placed higher in the order >′ than in the order >, thus their contribution to the weighted size with respect to the order >′ is not smaller than with respect to >.
From now on we work with the order >′ instead of >, and thus indexing of variables, squeezes, normal forms, etc. are implicitly understood to be defined with respect to that order.
Let nf(γ⋅X
k
)=γ⋅α. By Lemma 47 we know that no variable appearing in α is generated by X
k
. We are aiming at showing that the d-size(α)≤d-size(X
k
).
Case 2.2 is the only one which requires referring to the induction assumption. We will invoke the induction assumption for variables smaller than X
k
, and the same admissible order >′ on variables. To this aim, we will start by considering Bisimulation Game starting with a decreasing non-generating Spoiler’s move, as outlined below.
Let
X
m
be the smallest variable occurring in
α, i.e.
α=
α′||
X
m
(note that
X
m
may occur in
α′). Consider the Bisimulation Game for
$$\gamma \cdot X_k \simeq \gamma \cdot \alpha $$
and the first Spoiler’s move from the right process induced by some decreasing non-generating transition rule of
X
m
, say
\(X_{m} \stackrel {\zeta }{\longrightarrow } \omega\):
$$\gamma \cdot ({\alpha'||X_m}) \stackrel {\zeta }{\longrightarrow } \gamma \cdot \alpha'\cdot \omega. $$
By Lemma 32 we know that there is a matching Duplicator’s response that does not engage
γ. As no
γ-squeeze of
X
k
is reachable from
X
k
by
\(\stackrel {}{\Longrightarrow }_{0}\), the response has necessarily the following form
$$\gamma \cdot X_k \stackrel {}{\Longrightarrow }_0 \gamma \cdot X_k\cdot \eta \stackrel {\zeta }{\longrightarrow } \gamma \cdot ({\sigma ||\eta}), $$
where
η is generated by
X
k
and
X
k
disappears in the last transition:
$$X_k \stackrel {}{\Longrightarrow }_0 X_k\cdot \eta \quad \text{and}\quad X_k \stackrel {\zeta }{\longrightarrow } \sigma. $$
Indeed, otherwise the second last process in the sequence forming a matching Duplicator’s move would be a
γ-squeeze of
X
k
, forbidden by the assumption of Case 2.2. We have
γ⋅(
σ||
η)≃
γ⋅
α′⋅
ω and thus also
$$ \text {nf}\big (\gamma \cdot ({\sigma ||\eta})\big ) = \text {nf}(\gamma \cdot \alpha'\cdot \omega). $$
(28)
Now we are going to deduce from equality (
28) how the weighted sizes of nf(
γ⋅
σ) and nf(
γ⋅
α′) are related, in order to conclude that the weighted size of
α is as required.
Let’s inspect the
m-prefix of the left processes in (
28). Process
η can not contribute to the
m-prefix of the normal form. Indeed,
η contains only variables generated by
X
k
, which are necessarily smaller than
X
m
, as
X
m
is not generated by
X
k
, since it appears in nf(
γ⋅
X
k
). Thus if we restrict to the
m-prefixes we have the equality
$$ {m}\text {-}\text {prefix}\big (\text {nf}\big (\gamma \cdot ({\sigma ||\eta})\big )\big ) = {m}\text {-}\text {prefix}\big (\text {nf}(\gamma \cdot \sigma)\big ). $$
(29)
Similarly, let’s inspect the
m-prefix of the right process in (
28). Again,
ω can not contribute to the
m-prefix of the normal form, thus if we restrict to the
m-prefixes we have the equality
$${m}\text {-}\text {prefix}\big (\text {nf}\big (\gamma \cdot \alpha'\cdot \omega\big )\big ) = {m}\text {-}\text {prefix}\big (\text {nf}\big (\gamma \cdot \alpha' \big )\big ). $$
As
γ⋅
α is the normal form,
γ⋅
α′ is unambiguous and thus we have nf(
γ⋅
α′)=
γ⋅
α′. From this we derive that
$$ {m}\text {-}\text {prefix}\big (\text {nf}\big (\gamma \cdot \alpha'\cdot \omega\big )\big )= {m}\text {-}\text {prefix}\big (\text {nf}\big (\gamma \cdot \alpha' \big )\big )={m}\text {-}\text {prefix}\big (\gamma \cdot \alpha' \big )= \gamma \cdot \alpha' . $$
(30)
Combine the equalities (
29), (
30) and (
28) to obtain:
$$ \gamma \cdot \alpha' = {m}\text {-}\text {prefix}\big (\text {nf}(\gamma \cdot \sigma )\big ) $$
(31)
and to observe that
$$ {d}\text {-}\text {size}\big ( \gamma \cdot \alpha' \big ) = {d}\text {-}\text {size}\big ( {m}\text {-}\text {prefix}\big (\text {nf}(\gamma \cdot \sigma )\big ) \big ) \leq {d}\text {-}\text {size}\big (\text {nf}(\gamma \cdot \sigma )\big ). $$
(32)
Now we will use induction assumption for the variables smaller than
X
k
, to derive that every variable
X
i
smaller than
X
k
(i.e. for
i>
k) has a
γ-squeeze of weighted size smaller than
X
i
. As normal form is obtained via a sequence of squeezes, and
γ is unambiguous, the induction assumption implies that
$${d}\text {-}\text {size}\big (\text {nf}(\gamma \cdot \sigma )\big ) \leq {d}\text {-}\text {size}(\gamma \cdot \sigma ) $$
which leads to the following estimation:
$$ {d}\text {-}\text {size}\big (\text {nf}(\gamma \cdot \sigma )\big ) \leq {d}\text {-}\text {size}(\gamma)+ {d}\text {-}\text {size}(\sigma) \leq {d}\text {-}\text {size}(\gamma)+ \text {size}(\sigma) \cdot d^{n-k-1}. $$
(33)
The inequalities (
32) and (
33) jointly imply:
$${d}\text {-}\text {size}\big ( \gamma \cdot \alpha' \big ) \leq {d}\text {-}\text {size}(\gamma)+ \text {size}(\sigma) \cdot d^{n-k-1}, $$
and removing
γ from both sides of the inequality, we get:
$${d}\text {-}\text {size}\big ( \alpha'\big ) \leq\ \text {size}(\sigma) \cdot d^{n-k-1} \leq (d-1) \cdot d^{n-k-1}. $$
Recalling that
α=
α′⋅
X
m
:
$$\begin{aligned} {d}\text {-}\text {size}(\alpha) = {d}\text {-}\text {size}\big ( \alpha'\cdot X_m\big ) \leq \text {size}(\sigma) \cdot d^{n-k-1}\ +\ d^{n-m} \\ \ \leq\ (d-1)\cdot d^{n-k-1}\ +\ d^{n-k-1} = d^{n-k} = {d}\text {-}\text {size}(X_k) \end{aligned}$$
which is the required bound. As Case 2.2 is the last one, we have thus completed the proof of Lemma 43.