定理証明手習い (83) Dethmの法則？

具体的な形になった定理をつかう前に、follow-premsで延滞をチェックする必要があります。このチェックにより、等しいことが証明可能な2つの式を表す具体的な帰結が、等式として得られます。

わかったようなわからないような
(equal (car (cons 'a 'b)) 'a)みたいな式が得られる、ってことですかね

follow-premsから見てみます

(defun follow-prems (path e thm)
  (if (if? thm)
      (if (prem-A? (if.Q thm) path e)
          (follow-prems path e (if.A thm))
          (if (prem-E? (if.Q thm) path e)
              (follow-prems path e (if.E thm))
              thm))
      thm))

thmは定理でしょうね
pathはeにおけるフォーカスを表してるんでしょうがeはなんでしょうか
thmとeの関係は？
eがthmの証明？

thmがifじゃなければなにもしないでthmをそのまま返す
ifだったら
Q部がprem-AならA部のfollow-premsを返す
Q部がprem-EならE部のfollow-premsを返す
どちらでもなければthmをそのまま返す

A部やE部をたどって何かしている、くらいしかわかりません

prem-A?とprem-E?を見てみます
ほとんど同じなのでprem-A?の方を

(defun prem-A? (prem path e)
  (if (atom path)
      'nil
      (if (equal (car path) 'A)
          (if (equal (if.Q e) prem)
              't
              (prem-A? prem (cdr path)
                       (find-focus-at-direction (car path) e)))
          (prem-A? prem (cdr path)
                   (find-focus-at-direction (car path) e)))))

premにはthmのQ部が入ってきます
premというからにはきっと前提となるもの

pathの先頭が'Aで、eのQ部がpremと等しいなら't

例で考えてみる
premが(equal x 'b)
pathが(A 2 A ...)
eが(if (equal x 'a) (equal 't (if (equal x 'b) (equal y 'b) (equal y 'c))) (equal y 'd))なら
まずはpremと(equal x 'a)を比較
一致しないからA部 (equal 't (if (equal x 'b) (equal y 'b)))を見る
pathの先頭が'Aではないので
'2が示す(if (equal x 'b) (equal y 'b))を見る
premと(equal x 'b)が一致しているので't

これは何をやってることになるのかな
あるパスのA部に、指定された前提と同じQ部があるかどうかを確認している

Dethmの法則のことかな？

3. その帰結がifのAnswer部（あるいはElse部）に含まれているなら、書き換え対象のフォーカスも同じQuestion部を持つifのAnswer部（あるいはElse部）に含まれていなければならない。

premise（前提）らしき言葉は出てこないけど
〜なければならない、の部分には一致してそう

pathの示す部分式が、premの示す条件に合った場所にあるかどうかってことだな

てところでfollow-premsに戻ると

pathの示す部分式が、thmのQ部の示す条件に合った場所にあるかどうか

ってことか
follow-premsの再帰はifの入れ子に対応しているんだな

まだちょっと完全には理解してないけどこれくらいで先に進もう