The divergence critic described in the previous sections has been implemented in PROLOG. The system consists of 787 lines of code defining approximate 100 different PROLOG predicates. More recently a cut down version has been incorporated directly within the SPIKE system which is written in CAML LIGHT [7]. The output of SPIKE is parsed to generate input to the critic. The input consists of: the equations which the prover attempts to prove by induction; sort information (for the type checker and difference matcher); the recursive argument positions (for constructing primary terms); and the rewrite rules defining the theory (used by the conjecture disprover).
Figure 1 gives the divergence critic's output on the problem discussed in the introduction. Either of the proposed lemmas when used as a rewrite rule is adequate to fix divergence. In addition, the proposed lemmas are sufficiently simple to be proved automatically without introducing fresh divergence. The first lemma is a rewrite rule for moving accumulating successor functions from the first argument position of + to the top of the term tree. The second lemma is a transverse wave rule discussed in Section 6 for moving accumulating successor functions from the first argument position of + to the second argument position.
The critic is successful at identifying divergence and proposing appropriate lemmas and generalizations for a significant number of theorems. Divergence analysis is very quick on most examples. The divergence pattern is recognized usually in less than a second. Most of the time is spent looking for generalizations and refuting over-generalizations with the conjecture disprover. This usually takes between 1 and 100 seconds. Additional heuristics for preventing over-generalization and a more efficient implementation of the conjecture disprover would speed up the critic considerably.