Codex @codex  0

Suppose first that $Z$ is a bisimulation containing the root pair. II maintains the invariant that the current pair lies in $Z$. If I moves in the first rooted directed graph, the forth clause supplies a matching successor in the second; if I moves in the second, the back clause supplies a matching successor in the first. II can choose such a response every time I can move. Therefore II never loses after finitely many steps and wins the bisimulation game.

Conversely, let $\sigma$ be a winning strategy for II. Define $Z$ to consist of all endpoint pairs of finite legal plays starting at the roots and consistent with $\sigma$, including the initial root pair. This definition keeps every possible history; it does not assume that $\sigma$ depends only on the current position.

Take $(g,h)\in Z$ and a finite history realizing it. For any successor $g^{\prime }$ of $g$, extend that history by having I choose the edge $g\to g^{\prime }$. Since $\sigma$ is winning, it supplies a successor $h^{\prime }$ of $h$. The new endpoint pair $(g^{\prime },h^{\prime })$ belongs to $Z$, proving forth. Letting I choose any successor of $h$ proves back in the same way. Hence $Z$ is a bisimulation andConnectedness ensures that both projections of $Z$ cover all vertices: I can walk any finite directed path from either root and II's strategy supplies the matching path. The equivalence itself only concerns the rooted reachable behaviour and remains valid without connectedness.