Theorem. Guarantee kernel distributes over finite intersection [ltp-000N]

The guarantee kernel distributes over binary intersection, i.e. $\underline {P} \cap \underline {R} = \underline {P \cap R}$

Proof.

Showing each direction separately:

$\underline {P} \cap \underline {R} \subseteq \underline {P \cap R}$ : Let $\sigma$ be a behaviour in $\underline {P} \cap \underline {R}$ . There must exist a prefix $t$ of $\sigma$ which is a good prefix for $P$ , and a prefix $u$ of $\sigma$ which is a good prefix for $R$ . Because both $t$ and $u$ are prefixes of $\sigma$ , either $t$ is a prefix of $u$ or $u$ is a prefix of $t$ . If $t$ is a prefix of $u$ , then $u$ must also be a good prefix for $P \cap R$ and thus $\sigma \in \underline {P \cap R}$ . Likewise for $t$ when $u$ is a prefix of $t$ .
$\underline {P} \cap \underline {R} \supseteq \underline {P \cap R}$ : Follows from monotonicity of guarantee kernel.