1: \begin{proof}

2: Since bisimulation is both an equivalence and a congruence, we only need to check that the first clause in the definition of the relation $=$ is sound.

3: That is, if $s=t$ is an axiom in GameBPA and $\sigma$ is a closed substitution that maps the variables in $s$ and $t$ to process terms, then we need to check that $\sigma(s)\underline{\leftrightarrow}\sigma(t)$.

4: 

5: We only provide some intuition for soundness of the axioms in Table \ref{AxiomOfPO}.

6: 

7: \begin{enumerate}

8:   \item The axiom DL1 says that $\delta$ displays no behavior, so the process term $t + \delta$ is equal to the process term $t$.

9:   \item The axioms DL2, PO3 and PO4 say that $\delta$ blocks the behavior of the process term $\delta \cdot t$, $\delta \sqcap t$ and $t \sqcap \delta$.

10:   \item The axioms PO1 and PO2 say that the co-action of two same actions will lead to the only action, otherwise, it will cause a deadlock.

11:   \item The axioms PO5-PO10 say that $s\sqcap t$ makes as initial transition a playing of initial transitions from $s$ and $t$. If the execution sequence of $s$ is not matched with that of $t$, a deadlock will be caused.

12:   \item The axioms PO11-PO12 say that the function of playing operator makes two non-deterministic GameBPA processes deterministic.

13:   \item The axioms PO13-PO14 say that the playing operator satisfies right and left distributivity to the operator $+$.

14: \end{enumerate}

15: 

16: These intuitions can be made rigorous by means of explicit bisimulation relations between the left- and right-hand sides of closed instantiations of the axioms in Table \ref{AxiomOfPO}. Hence, all such instantiations are sound modulo bisimulation equivalence.

17: \end{proof}

18: