定理証明手習い (31) 証明の順番

次のフォーカスでctx?/tを使えるでしょうか？
はい、オレンジ色で示したぜんていがあるので使えます。あとでctx?/tの証明はしないといけませんけどね。

あとでいいんだっけ？

(J-Bob/prove (defun.ctx?)
  '(((dethm ctx?/t (x)
         (if (ctx? x)
             (equal (ctx? x) 't)
             't))
     nil)
    ((dethm ctx?/sub (x y)
     :

これでもちゃんとctx?/subの証明が進められるんだ
そういえば下の方から証明していくって話だったかそうかそういう意味になるのか
じゃあ上に無茶な定理とか書いても使えちゃうんだ

> (J-Bob/prove (my/prelude)
    '(((dethm mucha (a b)
         (equal a b))
       nil)
      ((dethm kucha ()
         (equal 't 'nil))
       nil
       ((1) (mucha 't 'nil)))))
(equal 'nil 'nil)

ほんとだ
でもやっぱり定理って証明してから使うものじゃないのかなあ
どうしてこういう仕様になってるんだろう？

まあもう証明したし

あとは長いけどctx?/tの証明でだいたい感じはつかめてるので
流れに沿って進む
ctx?/tの証明もどうやら思った通りの流れだった模様
(細部まで細かく答え合わせする気力なし)

どこで関数を展開するかはちょっと悩む
行き詰ったくらいでやるのがいい気はする