Termination checking for complete induction

[MartyO256]

Twelf has a reduction declaration that can be used to label the outputs of lemmas as non-inflationary, which allows for recursive calls on these outputs.

Totality checking for such programs would require the use of complete induction.
This may be implemented following the same ideas as in Termination and Reduction Checking for Higher-Order Logic Programs.

[tsani]

This would be really great to have. Brigitte pointed out that the main challenge will be integrating it with our existing approach for totality checking. It isn't clear how this can be made compatible with the notion of generating at the moment that splitting occurs a list of possible induction hypotheses, since suddenly terms such as lemma [|- D] is still considered structurally smaller.

I think that a bigger investigation into how we do totality checking will be necessary.