There are several basic properties of communication primitives that currently lack proofs, because these proofs have to be conducted by directly referring to the transition system and conducting such proofs was hard in the ♮-calculus era, without support for “up to” methods.

We shall conduct all the missing proofs of properties of communication primitives. For this, we shall follow the approach outlined in the respective comment in the high-assurance-legacy repository as much as feasible.