Now, suppose we have a counter that ranges from zero to infinity.
We can still prove by induction that any value `i` is
eventually reached. To do this, we declare `TYPE` to
be an `ordset` without an upper bound:

ordset TYPE 0..;

With this change, run the example.
Now choose `Verify All` to verify that in fact
the induction works, and that `p[i]` holds for all `i`.
We've just proved a property of an infinite-state system
by model checking.

2003-01-07