Now suppose that we would like to verify the correct transmission of a very large array of bytes, or even an array of unknown size. SMV provides a way to do this by reducing a type with a large or unknown number of values to an abstract type, with a small fixed number of values. This type has one additional abstract value to represent all the remaining values in the original type.
For example, when verifying the correct transmission of byte i, we might reduce the index type to just two values - i and a value representing all numbers not equal to i, (which SMV denotes NaN). This is an abstraction, since NaN, when compared for equality against itself, produces an undetermined value. In fact, here is a truth table of the equality operator for the reduced type:
| = | i | NaN |
| i | 1 | 0 |
| NaN | 0 | {0,1} |