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