⁴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₁,…,t_n. There is no problem in handling this more general case: the narrowing-based symbolic model checking can just take a tuple ⟨t₁,…,t_n⟩.