RosettaCodeData/Task/Mutual-recursion/ACL2/mutual-recursion.acl2

(mutual-recursion
 (defun f (n)
    (declare (xargs :mode :program))
    (if (zp n)
        1
        (- n (m (f (1- n))))))

 (defun m (n)
    (declare (xargs :mode :program))
    (if (zp n)
        0
        (- n (f (m (1- n)))))))