Proving the language of this pi calculus process Can someone help me understand why $ L( P ) = a^n b^n c^n $ in the following pi - calculus process
$$ P = ( \nu k_1, k_2, k_3, u_{b} , u_c)( \overline{k_1} \mid \overline{k_2} \mid Q_a \mid Q_b \mid Q_c) $$
$$Q_a = {!}k_1.a.( \overline{k_1} \mid \overline{k_3} \mid \overline{u_b} \mid \overline{u_c})$$
$$Q_{b} = k_1.!k_3.k_2.u_b.b.\overline{k_2}$$
$$Q_{c} = k_2.(! u_c.c \mid u_b.\mathrm{DIV} )$$
where $DIV = !τ$
 A: At the beginning, there is a waiting $\overline{k_1}$. It can be consumed by reducing $Q_a$, which immediately puts one back, or it can be consumed by reducing $Q_b$, which gets rid of $\overline{k_1}$ forever (thus preventing $Q_a$ from reducing ever again). Thus, once a $b$ has been emitted, no $a$ can be emitted any longer. By the same reasoning on $\overline{k_2}$, once a $c$ has been emitted, no $b$ can be emitted any longer. Hence all traces of $P$ match $a^* b^* c^*$.
Let $a^n b^p c^q$ be a trace of $P$: Emitting a $b$ requires an input on $u_b$. There are exactly as many inputs on $u_b$ as there are reductions of the replication in $Q_a$, which is as many as $a$'s are emitted. Hence $p \leq n$. By the same reasoning on $u_c$, each emission on $c$ requires one prior emission on $a$, hence $q \leq n$.
If $p < n$ and the system isn't just about to emit a $b$ in $Q_b$, then there is at least one spare $\overline{u_b}$. We saw previously that there is at most one $\overline{k_2}$; let us refine the analysis:


*

*If there is a $\overline{k_2}$, then $Q_c$ must be intact. $Q_b$ may have become $!k_3.k_2.u_b.b.\overline{k_2}$, which can progress because there is a spare $\overline{k_3}$ produced together with the spare $\overline{u_b}$; or it may have become $(!k_3.k_2.u_b.b.\overline{k_2}) \mid k_2.u_b.b.\overline{k_2}$, which can progress since there is an outstanding output on $k_2$.

*If the last $\overline{k_2}$ was consumed within $Q_b$, then the leftover from the replication must be either $u_b.b.\overline{k_2}$, which can progress by emitting that spare $\overline{u_b}$, or $b.\overline{k_2}$ or $\overline{k_2}$ which can progress to put back an $\overline{k_2}$.

*Otherwise the last $\overline{k_2}$ must have been consuming by reducing $Q_c$. Then that spare $\overline{u_b}$ must lead to a divergence.


In any case, a complete, non-diverging trace cannot have a spare $\overline{u_b}$ and thus has $p = n$.
Now suppose $q < p = n$: As before, if the system isn't about to emit a $c$ in $Q_c$, then there is a spare $\overline{u_c}$. If $Q_b$ hasn't started reducing yet, then either there is a $\overline{k_1}$ and $Q_a$ can reduce, or $Q_a$ is in the process of reducing; either way the system can progress. Since $p = n$, there cannot be a spare $\overline{k_3}$ for the replication in $Q_b$ to progress. So either there is a spare $\overline{k_2}$ and $Q_c$ can start reducing, or there is none and $Q_c$ has already been reduced. There is no spare $\overline{u_b}$ because that would require $p < n$. But as long as there is a spare $\overline{u_c}$, the replication in $Q_c$ can progress and emit a $c$.
We've shown that any complete, terminating trace of $P$ is of the form $a^n b^n c^n$. Showing that $P$ can emit all such traces is left as an easy exercise for the reader.
