theory Semantics imports Broadcast_Chain Broadcast_Frame begin text ‹This file is a (heavily modified) variant of the theory {\it Psi\_Calculi.Semantics} from~\cite{DBLP:journals/afp/Bengtson12}. The nominal datatypes {\it ('a,'b,'c) residual} and {\it 'a action} have been extended with constructors for broadcast input and output. This leads to a different semantics.›