定理証明手習い(97) しゅくだい(5)

最初の主張

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

(if (atom x) ...)を消す

     ((A A) (if-nest-A (atom x)
                       't
                       (equal (reverse2 (reverse2 x res) res) x)))
     ((A) (if-same (equal res '()) 't))
     ((E A A) (if-nest-E (atom x)
                         't
                         (equal (reverse2 (reverse2 x res) res) x)))

↓

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

(if (atom (cdr x)) ...)を外に出そう

     ((E) (if-same
           (atom (cdr x))
           (if (if (equal (cons (car x) res) '())
                   (if (atom (cdr x))
                       't
                       (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x)))
                   't)
               (if (equal res '()) (equal (reverse2 (reverse2 x res) res) x) 't)
               't)))
     ((E A Q A)
      (if-nest-A
       (atom (cdr x))
       't
       (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x))))
     ((E A Q) (if-same (equal (cons (car x) res) '()) 't))
     ((E A) (if-true
             (if (equal res '()) (equal (reverse2 (reverse2 x res) res) x) 't) 't))
     ((E E Q A)
      (if-nest-E
       (atom (cdr x))
       't
       (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x))))

↓

(if (atom x)
    't
    (if (atom (cdr x))
        (if (equal res '()) (equal (reverse2 (reverse2 x res) res) 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 res) res) x) 't)
            't)))