SMV has a special construct to support this kind of case analysis. It is especially useful for compositional verification, since for each case we can use a different abstraction of the system, including different components in the verification. This allows us to break large verification problems into smaller ones.
The above described case analysis is expressed in SMV in the following way:
forall (v in TYPE) subcase q[v] of p for x = v;
Now suppose that p is some temporal assertion G cond, where cond is any boolean condition. The above declaration effectively defines a collection of properties q[v], as if we had written
forall (x in TYPE) q[v] assert G (x=v -> cond);
That is, each q[v] asserts that p holds at those times when x = v. Clearly, if q[v] holds for all values of v, then p holds. Thus, SMV is relieved of the obligation of proving p, and instead separately proves all the cases of q[v]. Note that if TYPE is a scalarset type, we may in fact have to prove only one case, since all the other cases are symmetric.