定理証明手習い(98) しゅくだい(6)

(if (equal res '()) ...を使おう
前提がついてないとこれができなくて詰む

     ((E A A 1 1 2) (equal-if res '()))
     ((E A A 1 2) (equal-if res '()))
     ((E E A A 1 1 2) (equal-if res '()))
     ((E E A A 1 2) (equal-if res '()))

↓

(if (atom x)
  't
  (if (atom (cdr x))
    (if (equal res '()) (equal (reverse2 (reverse2 x '()) '()) x) 't)
    (if (if (equal (cons (car x) res) '())
          (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x))
          't)
      (if (equal res '()) (equal (reverse2 (reverse2 x '()) '()) x) 't)
      't)))

(E A)をやっつけていきます

ここは、意味的にはxが長さ1のリストならreverse2/reverse2が成り立つということ
reverse2を展開しては整理

     ((E A A 1 1) (reverse2 x '()))
     ((E A A 1 1) (if-nest-E (atom x) '() (reverse2 (cdr x) (cons (car x) '()))))
     ((E A A 1 1) (reverse2 (cdr x) (cons (car x) '())))
     ((E A A 1 1) (if-nest-A
                   (atom (cdr x))
                   (cons (car x) '())
                   (reverse2 (cdr (cdr x)) (cons (car (cdr x)) (cons (car x) '())))))
     ((E A A 1) (reverse2 (cons (car x) '()) '()))

このへんでこうなってます
大丈夫かな

(if (atom x)
  't
  (if (atom (cdr x))
    (if (equal res '())
      (equal
       (if (atom (cons (car x) '()))
         '()
         (reverse2 (cdr (cons (car x) '())) (cons (car (cons (car x) '())) '())))
       x)
      't)
    (if (if (equal (cons (car x) res) '())
          (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x))
          't)
      (if (equal res '()) (equal (reverse2 (reverse2 x '()) '()) x) 't)
      't)))

atom/cons、car/cons、cdr/consを使って・・・

     ((E A A 1 Q) (atom/cons (car x) '()))
     ((E A A 1) (if-false
                 '()
                 (reverse2 (cdr (cons (car x) '()))
                           (cons (car (cons (car x) '())) '()))))
     ((E A A 1 1) (cdr/cons (car x) '()))
     ((E A A 1 2 1) (car/cons (car x) '()))

↓

(if (atom x)
  't
  (if (atom (cdr x))
    (if (equal res '()) (equal (reverse2 '() (cons (car x) '())) x) 't)
    (if (if (equal (cons (car x) res) '())
          (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x))
          't)
      (if (equal res '()) (equal (reverse2 (reverse2 x '()) '()) x) 't)
      't)))

xが長さ1のリストなら(reverse2 '() (cons (car x) '()))がxに等しい、になりました

     ((E A A 1) (reverse2 '() (cons (car x) '())))
     ((E A A 1 Q) (atom '()))
     ((E A A 1) (if-true
                 (cons (car x) '())
                 (reverse2 (cdr '()) (cons (car '()) (cons (car x) '())))))

↓

(if (atom x)
  't
  (if (atom (cdr x))
    (if (equal res '()) (equal (cons (car x) '()) x) 't)
    (if (if (equal (cons (car x) res) '())
          (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x))
          't)
      (if (equal res '()) (equal (reverse2 (reverse2 x '()) '()) x) 't)
      't)))

よしあとちょっと
(equal (cons (car x) '()) x)が言えれば
言えれば・・・
言え・・・
言えないなあ・・・

最大限がんばっても？cons/car+cdrで
(equal (cons (car x) '()) (cons (car x) (cdr x)))にするくらいか・・・
(cdr x)が'()に等しい、って長さ1のリストなんだからそうなるはずなんだけど

あ
(atom x)でなくて(atom (cdr x))でも長さ1のリストとは限らないのか
ドット対のことまったく考えてなかった
あちゃー

> (reverse (reverse '(a . b)))
(a)

成り立たねーじゃん
どーすんだよこれ

ドット対が出てきてもreverse/reverseが成り立つようにreverseの定義を変える？
ドット対が出てきたときはreverseはどう動くのが妥当？
わかんね

reverse/reverseにドット対が出てこないという前提を置く？
それはどう書けばいいのか
もうひとつ関数が必要か
そういう前提を置いたとして、うまく使えるかどうかもけっこう心配

それとも

「(reverse (reverse x))がどんなリストについても常にxになるか」

なりません、が答えとか？
いやそれは・・・