p : assert G r;Suppose further that we split cases on the value of some variable

forall(i in TYPE) subcase q[i] of p for v = i;Now,

forall(i in TYPE) forall(j in TYPE) using q[j] if j < i prove q[i];The added clause

G (v < i -> r)It uses this formula to prove

As an application of course-of-values induction, consider the following example
(stolen from Zohar Manna): a finite collection of processes, where each process `i`
chooses an arbitrary number `n[i]` at the initial time. Each process also
has a flag `done[i]`. Process `i` loops through all process indices `j`
and waits for each process `j` with a number `n[j] < n[i]` to be ``done''.
When all processes with a lower number are done, it sets its own flag `done[i]`.
We would like to prove that every process eventually sets its done flag.

To begin with, here is a model of our system of processes:

#define MAXPROC 1000 ordset INDEX 1..MAXPROC; ordset NAT 0..; module main(){ n : array INDEX of NAT; done : array INDEX of boolean; count : array INDEX of INDEX; forall(i in INDEX){ next(n) := n; init(count[i]) := 1; if(n[count[i]] < n[i] -> done[count[i]]){ next(count[i]) := count[i] + 1; if(count[i] = MAXPROC) next(done[i]) := 1; } }Note we have made the type

The specification for our processes is that every process eventually sets its done flag. We write this as follows:

forall(i in INDEX) p[i] : assert G F done[i];Note, we have actually written something stronger, just because SMV is particularly fond of proving

forall(i in INDEX) forall(j in INDEX) forall (k in NAT){ subcase q[i][k] of p[i] for n[i] = k; subcase r[i][k][j] of q[i][k] for count[i] = j; forall(l in NAT) forall(m in INDEX){ using q[j][l] if l < k, r[i][k][m] if m > j prove r[i][k][j]; }The property

This example demonstrates two fairly general techniques. One is that
to prove that a loop terminates, we split cases on the index variable
of the loop and we assume termination for all values greater than the
current value (or lesser if the index is decreasing). Of course, we
could have used simple induction to prove termination of the loop,
but this technique saves us a step, and also eliminate the value `i-1`,
which would have contributed to case explosion and state explosion.

The other general point is that when we compare two numbers (such as
`n[i]` and `n[j]`) it isn't always necessary to split cases on
both values. In this case, we just split cases on `n[i]`, and then
used course-of-values induction to assume our property held for ` all` values less than `n[i]`. Thus, we didn't have to know the
`particular` value of `n[j]`. This technique is also quite
useful in avoiding case explosion, since it saves us one parameter.