  Maintaining data consistency among multiple parties requires nodes to
repeatedly send data to all other nodes. For example, the nodes of a blockchain
network have to disseminate the blocks they create across the whole network.
The scientific literature typically takes the ideal perspective that such data
distribution is performed by broadcasting to all nodes directly, while in
practice data is distributed by repeated multicast. Since correctness and
security of consistency maintenance protocols usually have been established for
the ideal setting only, it is vital to show that these properties carry over to
real-world implementations. Therefore, it is desirable to prove that the ideal
and the real behavior are equivalent.
  In the work described in this paper, we take an important step towards such a
proof by proving a simpler variant of this equivalence statement. The
simplification is that we consider only a concrete pair of network topologies,
which nevertheless illustrates important phenomena encountered with arbitrary
topologies. For describing systems that distribute data, we use a
domain-specific language of processes that corresponds to a class of Petri nets
and is embedded in a general-purpose process calculus. This way, we can outline
our proof using an intuitive graphical notation and leverage the rich theory of
process calculi in the actual proof, which is machine-checked using the
Isabelle proof assistant.
