 In order to warrant that there are such minimal states, \(\prec\) is considered to be smooth (also sometimes called stuttered), i.e., for each \(M\) either \(M\) is \(\prec\)-minimal or there is a \(\prec\)-minimal \(M'\) such that \(M' \prec M\). 