手帳をちゃんと使わないと、と思っている人へ

手帳にメモってそれを見ることができるようになった、というあたりが いいサイクルの回り始めだったと思います

『ちょっとしたことでうまくいく 発達障害の人が上手に働くための本』 - kb84tkhrのブログ

せっかくなんでこのへんのことも書いておこうかと
特に目新しい技があるわけではなくて、まあ体験談みたいなものです

だれか似た状況のひとがいるかもしれないな、と思いまして
自分が改善できたのはかなりおっさんになってからでしたが
早いうちに改善できればずっと楽になれるので

定理証明手習い (56) positive/wt

(+ (wt (car x)) (wt (car x)))は正の数ですか？
(wt (car x))が正なら、正ですね。

そういう当たり前のことがね

次のような主張positive/wtを作れば、そのフォーカスをうまい前提に書き換えられますね。

(dethm positive/wt (x)
  (equal (< '0 (wt x)) 't))

そうですね

もちろん、positive/wtは証明が必要です。

はいそうですね

定理証明手習い (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で都合のいい前提を導入する技はマスター済み
そして目的を果たすや否や導入したばかりの前提を消去するという極悪非道ぶりも発揮

定理証明手習い (54) 常に自然数でした

ひとつめは
公理の形に合わせるためには(equal (natp (wt (car x))) 't)じゃなくて
(natp (wt (car x))でないとだめ
ってこと

これには9章の後半で出てきた、if-trueを使って都合のいい前提を作る作戦が使える

定理証明手習い (53) (wt x)は常に自然数でしょうか

(wt x)は常に自然数でしょうか？
わかりませんが、できると思います。

（証明が）できる、ってことかな？
could beみたいに書いてあったのかもしれないな
それはともかくとして

(natp (wt x))を'tに書き換えて、外側のifをif-trueで取り除けば

いやーん

関数wtとnatpについての主張はあとで証明しないとですね。

気持ち悪いので先に証明してしまおう

定理証明手習い (52) 公理と定理と実際の用途

+と<についての公理
言ってることはわかります

定理証明手習い (51) wt

というわけで新しい尺度

(defun wt (x)
       (if (atom x)
           '1
           (+ (+ (wt (car x)) (wt (car x)))
              (wt (cdr x)))))

Scheme手習いでやったやつと同じです
そのときはこうでした