本とペンをセットで持ち運びたい
本に線を引いたり書き込んだりするようになってきたのでペンをセットで
持ち運びたいと思うようになりました
万年筆のクリップで表紙に挟んだり
マグネットで挟んで止めるタイプのペンケースをくっつけてみたりしましたが
どうも具合がよろしくない
定理証明手習い (60) align/align
進んでみたらわかることを期待して進む
J-Bob/prove
に(align x)
を種として与えてやると証明すべき式が出力されます
(if (atom x)
(equal (align (align x)) (align x))
(if (atom (car x))
(if (equal (align (align (cdr x)))
(align (cdr x)))
(equal (align (align x)) (align x))
't)
(if (equal (align (align (rotate x)))
(align (rotate x)))
(equal (align (align x)) (align x))
't)))
が
Defun帰納法にしたがって自分で作ってみます
主張はこれ
定理証明手習い (58)
休息の時間を勝ち取りました。
おやつを食べ終わったら続けます。
定理証明手習い (57) 見えない
142ページの
ここで関数
wt
を使いましょう。
から
:
ここでも、いまと同じステップが使えそうですね。
:
これで3回めになりますが、同じステップですかね?
:
次の2つのフォーカスで関数wt
を使いましょう。
:
まず、associate-+
の公理を使います。
:
を経由して
common-addends-<
を使って(wt (cdr x))
をキャンセルできますからね。
まで、何やってるのかわかんね感がぱない
言われたとおりにやればそうなるんだけど
(wt (cdr x))
をキャンセルできる形に持っていける見込みがあって変形していってるんだろうか
その見通しってやつが見えない
ここは「洞察」ないのかな