kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い (55) common-addendsのキャンセル

common-addends-<の公理を使うことで、<の引数にある2つの(wt (cdr x))をキャンセルできると思います。

     (if (atom x)
         't
         (if (atom (car x))
             (< (wt (cdr x))
                (+ (+ (wt (car x)) (wt (car x)))
                   (wt (cdr x))))
             (< (wt (rotate x)) (wt x))))

これを

    (dethm common-addends-< (x y z)
      (equal (< (+ x z) (+ y z)) (< x y)))

と見比べて0を足すことを思いつけばいいわけだな!
ちょっと自信なし

足し算するためには(wt (cdr x))自然数であると言わなければいけないけれども
if-trueで都合のいい前提を導入する技はマスター済み
そして目的を果たすや否や導入したばかりの前提を消去するという極悪非道ぶりも発揮