Function check_termination_mutual 

pub fn check_termination_mutual(
    ctx: &Context,
    defs: &[(String, Term)],
) -> KernelResult<()>

Check that a MUTUAL block of fixpoints terminates — the mutual Giménez guard.

Every member’s structural (decreasing) argument position is computed first; then each body is checked so that a call to ANY member — itself OR a sibling — passes, at that member’s structural position, an argument structurally SMALLER than the CURRENT body’s structural parameter. Any infinite call chain would then demand an infinite strictly-descending sequence of subterms, which cannot exist — so the whole block terminates. Even.rec’s fixpoint calling Odd.rec on the sub-proof, and vice versa, is exactly what this guards. It is the single-fix guard with the recursive name generalized from one to a set of positions.