One way of removing the accumulating and nested term structure
is to propose a wave rule
which moves this difference to the top of the term
leaving the skeleton unchanged.
We hope either that it will then cancel
against wave-fronts on the other side of the equality
or that it will disappear in the process of being
moved. For the theorem,
after generalization (which is discussed in the next
section) the divergence pattern suggests
a rule of the form,
where is a second order variable which
we need to instantiate.
Instantiating is ultimately
a difficult synthesis problem so we can only hope
to have heuristics that will work some of the time.
Two of the heuristics used by the divergence critic
to instantiate are *cancellation* and *petering out*.

The cancellation heuristic uses difference matching to identify term structure accumulating on the opposite side of the sequence which would allow cancellation to occur. Failing that, the cancellation heuristic looks for suitable term structure to cancel against in a new sequence (the original sequence is usually a divergence pattern of a step case, whilst the new sequence is usually a divergence pattern of a base case). In the example, successor functions accumulate at the top of the left hand side of the diverging equations,

This divergence pattern suggests that should be instantiated to to enable immediate cancellation. Thus, as required, the cancellation heuristic suggests the rule,

The other heuristic used to instantiate
the right hand side of speculated lemmas
is petering out. In moving the differences
up to the top of the term, they may disappear altogether.
Consider, for example, the theorem,
where *isort* is insertion sort
and is true iff a list is sorted into
order. These are defined by the conditional rewrite rules,

where , which inserts the element into the list in order, and are defined by the rewrite rules,

Divergence analysis of SPIKE's attempt to prove this theorem suggests the need for a rule of the form, The petering out heuristic instantiates to the identity function . This gives the rule, This rule allows the proof to go through without divergence.

As a more complex example, consider the theorem, where is defined by the rewrite rules,

SPIKE's diverging attempt to prove this theorem generates the equations,

Divergence analysis identifies term structure accumulating in two different places,

This is the unique maximal difference match. This divergence pattern suggests the need for a rewrite rule of the form, The petering out heuristic instantiates to the identity function giving the rule, This rule allows the proof to go through without divergence.

Since the erasure of the wave rule must be properly typed, sort information can be used to prune inappropriate instantiations for . All speculated lemmas are therefore filtered through a type checker. Speculated lemmas are also filtered through a conjecture disprover. When a confluent set of rewrite rules exists for ground terms, exhaustive normalization of some representative set of ground instances of the equations is used to filter out non-theorems. Alternatively, the prover itself could be used to filter out non-theorems. Unlike many other induction theorem provers, SPIKE can refute conjectures since its inference rules are refutationally complete for conditional theories in which the axioms are ground convergent and defined functions are completely defined over free constructors [6]. Other techniques for disproving conjectures are described by Protzen (1992).

The critic's lemma speculation is summarized in Figure 2 (using the same variable names as the preconditions).

This specification
again uses second order variables in a limited
manner. First order difference matching is merely
required to construct lemmas. As with the preconditions,
the specification of the postconditions can be easily extended to deal
with multiple and nested wave-fronts (as in the
example).
Since the rules proposed by the critic move
the wave-fronts to top of the term, they
usually only introduce fresh divergence in the rare cases
that cancellation or fertilization fails. This is
unlikely since the cancellation and petering out
heuristics attempt to ensure *precisely*
that cancellation or fertilization
can take place.

Fri Apr 12 12:14:22 BST 1996