acl2 - 証明書き換え時のループを修正する方法

Question

ACL2 で自然数を単項表記 ( O、(S O)、(S (S O))、...) でモデル化し、加算の可換性を証明しようとしています。これが私の試みです：

; a NATURAL is 'O or a list ('S n') where n' is a NATURAL
(defun naturalp (n)
  (cond ((equal n 'O) t)
        (t (and (true-listp n)
                (equal (length n) 2)
                (equal (first n) 'S)
                (naturalp (second n))))))

(defun pred (n)
  (cond ((equal n 'O) 'O)
        ((naturalp n) (second n))))

(defun succ (n)
  (list 'S n))

(defun plus (n m)
  (cond ((equal n 'O) m)
        ((naturalp n) (succ (plus (pred n) m)))))

; FIXME: cannot prove this because rewriting loops...
(defthm plus_comm                                 
  (implies (and (naturalp n) (naturalp m))
           (iff (equal (plus n m) (plus m n)) t)))

これはおそらくこれを行う最も LISPy な方法ではありません。私はパターン マッチングを使用する言語に慣れています。

私の問題は、コメントで示唆されているとおりです。証明者はループし、同じもののより深くネストされたバージョンを証明しようとします。どうすればこれを止めることができますか? マニュアルでは、ループ書き換えルールについて簡単に言及していますが、それらについて何をすべきかについては何も述べていません。

私の期待は、この証明は失敗し、それを完了するために必要な補助補題についてのヒントを与えてくれるというものでした。ループ証明からの出力を使用して、ループを停止する可能性のある補題を見つけ出すことはできますか?