自動定理証明器 ACL2 の入門向けに L-99 の1問目を解きました

[2023-02-05 日] この記事はいま思うとあまりよく分かっていなかったときに書いたものなので参考にしない方がいいです。 Lisp の説明のあたりは別に問題ないと思っていますが、実際に ACL2 に渡す補題を考えるときの心構え的な部分が微妙です。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張ります。 今回は L-99: Ninety-Nine Lisp Problems の問題の一問目を ACL2 でやっていきます。 L-99 は P-99: Ninety-Nine Prolog Problems という Prolog の 99 問の問題が Lisp に翻訳されたものです。Lisp の入門に広く使われている問題集になっています(要出典)。 L-99 の1問目を ACL2 で解いてさらにその関数の性質を ACL2 で証明することによって、 簡単に AC