Function check_termination 

pub fn check_termination(
    ctx: &Context,
    fix_name: &str,
    body: &Term,
) -> KernelResult<()>

Check that a Fix term satisfies the syntactic guard condition.

This is the main entry point for termination checking.