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.