Inductive Invariants for Nested Recursion

We show that certain input-output relations, termed inductive invariants are of central importance for termination proofs of algorithms de ned by nested recursion. Inductive invariants can be used to enhance recursive function de nition packages in higher-order logic mechanizations. We demonstrate the usefulness of inductive invariants on a large example of the BDD algorithm Apply. Finally, we introduce a related concept of inductive xpoints with the property that for every functional in higher-order logic there exists a largest partial function that is such a xpoint