定理証明手習い(96) しゅくだい(4)

reverse/reverseの証明に戻ってここからです

(if (atom x)
    't
    (equal
     (if (atom (reverse2 x '()))
         (reverse2 x '())
         (reverse2 (reverse2 x '()) '()))
     x))

(atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、が証明されたので

     ((E 1 Q) (atom/reverse2 x '()))
     ((E 1) (if-false (reverse2 x '())
                      (reverse2 (reverse2 x '()) '())))

して
こうなりました

(if (atom x) 't (equal (reverse2 (reverse2 x '()) '()) x))

すっきりしたところでいよいよ本丸

帰納法のための前提としてうまく使えるようにするには、関数add-atomsの
引数が変数になっている必要が

ありますが、

(if (atom x) 't (equal (reverse2 (reverse2 x res) res) x))

の形にすると前提が必要になります
ということを忘れててだいぶ時間を潰しました！
こういうふうにしないといけませんね

(dethm reverse2/reverse2 (x res)
  (if (equal res '())
      (if (atom x)
          't
          (equal (reverse2 (reverse2 x res) res) x))
      't))

証明を始める前に確かめておくべきでした

> (reverse2/reverse2 '(a b) '())
t
> (reverse2/reverse2 '(a b) 'c)
t
> (reverse2/reverse2 '(a b) '(c))
t
> (reverse2/reverse2 '() '())
t
> (reverse2/reverse2 '() 'a)
t
> (reverse2/reverse2 '() '(a))
t

だからきっとこれでいけるんじゃないかな？

(J-Bob/prove (dethm.atom/reverse2)
  '(((dethm reverse2/reverse2 (x res)
       (if (equal res '())
           (if (atom x)
               't
               (equal (reverse2 (reverse2 x res) res) x))
           't))
     (reverse2 x res)

これくらいで時間切れ