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, and notice that in the properties pane there are now only three cases to prove: p[0], p[1], [2]. We don't have to prove the maximum value as a special case, because there is no maximum value. 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.