定理証明手習い(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)))