Solution (source code)

= Solution

Take a <rooted directed graph> $G$ with one root $r$ and one terminal vertex $a$, with its sole edge $r\to a$. Let $H$ have a root $s$ and two terminal vertices $b,c$, with edges $s\to b$ and $s\to c$. The relation
$$
Z=\{(r,s),(a,b),(a,c)\}
$$
is a <bisimulation>. Each root move can be matched by a root move ending in a related terminal vertex. At all related terminal pairs there are no further edges, so both matching conditions are vacuous. Yet the <directed graphs> have two and three vertices and cannot be isomorphic. \b[Bisimilarity need not preserve the number of successors.]

Here and in the next part, the second graph's edge relation is $F$, and its response vertices belong to $H$. These are the corrections to the printed relation and vertex slips in the bisimulation clauses.