⁴In general, a set of initial states may not be describable by a single pattern $t$, but may have a description as a finite collection of patterns $t_1,\dots ,t_n$. There is no problem in handling this more general case: the narrowing-based symbolic model checking can just take a tuple $⟨t_1,\dots ,t_n⟩$.