In addition, this rule is sufficiently simple that it can be proved without assistance. The heuristics used by the critic to perform this lemma speculation are described in more detail in the next two sections. The divergence analysis performed by the critic is summarised in Figure 1. In analysing the divergence, we consider all the equations which the prover attempts to prove by induction. This includes those equation where the induction proof succeeds as these can often suggest useful patterns.
H is thus the accumulating and nested term structure that appears to be causing divergence.
Although G and H are second order variables, the second order nature of the divergence analysis is limited. Indeed, the implementation of the critic merely requires first order difference matching which is polynomial. For simplicity, the preconditions ignore the orientation of equations. In addition, the preconditions can be easily generalised to include multiple and nested annotations. This allows the critic to recognise multiple sources of divergence in the same equation.