 This supremum \(t_1 \sqcup t_2\) (its uniqueness follows from \(\sqsubseteq\)’s antisymmetry) can be understood as the ‘sum’, ‘merge’ or ‘fusion’ of states \(t_1\) and \(t_2\), and it provides the crucial tool for deciding whether a ‘conjunction’ is the case, as shown below.