induction.scm

(J-Bob/prove (dethm.memb?/remb0)
               '(((dethm memb?/remb (xs)
                         (if (atom xs)
                             (equal (memb? (remb xs)) 'nil)
                             (if (equal (memb? (remb (cdr xs))) 'nil)
                                 (equal (memb? (remb xs)) 'nil)
                                 't)))
                  nil
                  ; prove the base case
                  ((A 1 1) (remb xs))
                  ((A 1 1) (if-nest-A (atom xs) '() (if (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs))))))
                  ((A 1) (memb? '()))
                  ((A 1 Q) (atom '()))
                  ((A 1) (if-true 'nil (if (equal (car '()) '?) 't (memb? (cdr '())))))
                  ((A) (equal-same 'nil))
                  
                  ;prove the inductive case
                  ((E A 1 1) (remb xs))
                  ((E A 1 1) (if-nest-E (atom xs) '() (if (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs))))))
                  ((E A 1) (if-same (equal (car xs) '?) (memb? (if (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs)))))))
                  ((E A 1 A 1) (if-nest-A (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs)))))
                  ((E A 1 E 1) (if-nest-E (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs)))))
                  ((E A 1 A) (equal-if (memb? (remb (cdr xs))) 'nil))
                  ((E A 1 E) (memb? (cons (car xs) (remb (cdr xs)))))
                  ((E A 1 E Q) (atom/cons (car xs) (remb (cdr xs))))
                  ((E A 1 E) (if-false 'nil (if (equal (car (cons (car xs) (remb (cdr xs)))) '?) 't (memb? (cdr (cons (car xs) (remb (cdr xs))))))))
                  ((E A 1 E E 1) (cdr/cons (car xs) (remb (cdr xs))))
                  ((E A 1 E E) (equal-if (memb? (remb (cdr xs))) 'nil))
                  ((E A 1 E Q 1) (car/cons (car xs) (remb (cdr xs))))
                  ((E A 1 E) (if-nest-E (equal (car xs) '?) 't 'nil))
                  ((E A 1) (if-same (equal (car xs) '?) 'nil))
                  ((E A) (equal-same 'nil))
                  ((E) (if-same (equal (memb? (remb (cdr xs))) 'nil) 't))
                  (() (if-same (atom xs) 't))
                  )))