1: \begin{proof}

2: Because rooted branching bisimulation is both an equivalence and a congruence, we only need to check that if $t=u$ is an axiom and a closed substitution $\sigma$ replacing the variables in $t$ and $u$ to get $\sigma(t)$ and $\sigma(u)$, then $\sigma(t)\underline{\leftrightarrow}_{rb}\sigma(u)$.

3: 

4: We only provide some intuition for soundness of the axioms AO1, PO1-PO14.

5: 

6: \begin{enumerate}

7:   \item The axiom OA1 says a GameBPA process term $t \ddagger s$ is the same as the process term $t + s$ in the view of O.

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

9:   \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.

10:   \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.

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

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

13: \end{enumerate}

14: 

15: These intuitions can be made rigorous by means of explicit rooted branching 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 rooted branching bisimulation equivalence.

16: \end{proof}

17: