@cmplstofB それであってます。なお ACL ではなくて ACL2 です(A Computational Logic for Applicative Common Lisp の略なので)。証明支援系の一つですね。