一句话：从余代数对偶视角关联 apartness 与互模拟，并为弱/分支互模拟建立 apartness 证明系统。
论文研究互模拟（bisimulation）的余代数表述与其对偶概念 apartness 的关系。互模拟是余归纳等价，apartness 表示两元素可被正向区分，即不互模拟；它由最小不动点归纳描述，可用推导规则构成证明系统。作者在关系范畴中用提升函子刻画互模拟，并从初始代数/终结余代数的对偶说明 apartness 是互模拟性的精确对偶。对含 silent τ 步的标号迁移系统，论文定义对应弱互模拟与分支互模拟的 apartness，给出有限推导规则，并把分支互模拟的若干已知性质改写为分支 apartness 加以证明。最后在一般范畴情形展示 apartness 为初始代数、导出归纳原理，并纳入幂集函子以语义化非确定性选择。
A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives rise to the coinduction principle, which states that two bisimilar elements are equal. For polynomial functors, this leads to well-known descriptions. In the present paper we look at the dual notion of "apartness". Intuitively, two elements are apart if there is a positive way to distinguish them. Phrased differently: two elements are apart if and only if they are not bisimilar. Since apartness is an inductive notion, described by a least fixed point, we can give a proof system, to derive that two elements are apart. This proof system has derivation rules and two elements are apart if and only if there is a finite derivation (using the rules) of this fact. We study apartness versus bisimulation in two separate ways. First, for weak forms of bisimulation on labelled transition systems, where silent (tau) steps are included, we define an apartness notion that corresponds to weak bisimulation and another apartness that corresponds to branching bisimulation. The rules for apartness can be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them. Next, we also study the more general categorical situation and show that indeed, apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In this analogy, we include the powerset functor, which gives a semantics to non-deterministic choice in process-theory.