Data type reductions provide a mechanism for inductive reasoning in
SMV. To do this, however, we need a symmetric data type that allows
adding and subtracting constants, and inequality comparisons. In SMV,
such data types are called *ordsets*. An ordset is just like a
scalarset, except the restrictions on ordsets are slightly relaxed. If
we declare a type as follows:

ordset TYPE 0..1000;then, in addition to the operations allowable on scalarset types, the following are also legal:

`x + 1`and`x - 1`,`x = 0`and`x = 1000``x < y`,`x > y`,`x <= y`and`x >= y`

Induction is done in the following way: suppose we want to
prove property `p[i]`, where i is the induction parameter,
ranging over type `TYPE`.
We use a data type reduction that maps `TYPE` onto
a set of four values: X,i-1,i,Y. Here the symbolic value
`X` abstracts all the values less that `i-1`, and
`Y` abstracts all the values greater than `i`.
Incrementing a value in this reduced type is defined as follows:

X + 1 = {X,i-1} (i-1) + 1 = i i + 1 = Y Y + 1 = YThat is, adding one to a value less than

As an example, suppose we have a counter that starts from
zero and increments once per clock cycle, up to 1000. We'd like
to show that for any value `i` from 0 to 1000, the
counter eventually reaches `i`. Here's how we might
set this up:

ordset TYPE 0..1000; module main() { x : TYPE; /* the counter */ init(x) := 0; next(x) := x + 1; /* the property */ forall(i in TYPE) p[i] : assert F (x = i); /* the proof */ forall(i in TYPE) using p[i-1] prove p[i]; }We prove each case

SMV can verify that this proof is non-circular. Further, using its
induction rule, it automatically generates a data type reduction
using the values `i` and `i-1`, and it generates two representative
cases to prove: `p[0]` and `p[2]`.^{1} To confirm this,
run the example,
and look in the properties pane. You should see the aforementioned
properties. Now choose `Verify All` to verify that in fact
the induction works, and that `p[i]` holds for all `i`.