Solution of Ahmet GUL

;sequentte top level formulasi "not" olanlari bulur
(define (not-var arg)
           (filter (lambda (x) (and (list? x)
                                    (equal? (car x) 'not))) 
                                                             arg))
;sequentte top level formulasi "not" olmayanlari bulur
(define (not-yok arg)
            (filter (lambda (x) (or (not (list? x))
                                    (not (equal? (car x) 'not))))
                                                              arg))
;sequentte top level formulasi "and" olanlari bulur
(define (and-var  arg) 
           (filter (lambda (x) (and (list? x)
                                    (equal? (car x) 'and)))
                                                              arg)) 
;sequentte top level formulasi "and" olmayanlari bulur
(define (and-yok arg)
         (filter (lambda (x) (or (not (list? x))
                                  (not (equal? (car x) 'and))))
                                                               arg))
;sequentte top level formulasi "or" olanlari bulur
(define (or-var arg)
              (filter (lambda (x) (and (list? x)
                                       (equal? (car x) 'or))) 
                                                              arg))
;sequentte top level formulasi "or" olmayanlari bulur
(define (or-yok arg) 
             (filter (lambda (x) (or (not (list? x))
                                      (not (equal? (car x) 'or)))) 
                                                                 arg))
;sequentte top level formulasi ">" olanlari bulur
(define (ok-var arg)
             (filter (lambda (x) (and (list? x)
                                      (equal? (car x) '>))) arg))
;sequentte top level formulasi ">" olmayanlari bulur
(define (ok-yok arg)
             (filter (lambda (x) (or (not (list? x))
                                     (not (equal? (car x) '>))))
                                                              arg)) 
;argumanlarinin axiom olup olmadigini kontrol eder
(define (axiom? arg1 arg2)
                  (cond ((null? arg1) #f)
                        ((member (car arg1) arg2) #t)
                        (else (axiom? (cdr arg1) arg2)))) 
;r5 kuralini tek elemanli listlere uygular
(define (r5-helper arg)
              (cond ((not (list? arg)) arg)
                    ((null? arg) arg)
                    ((equal? (car arg) '>) (append (list 'or
                                                         (list 'not (cadr arg)))
                                                   (cddr arg)))
                    (else arg)))

;r5-helper yardimiyla r5 kuralini her casit liste uygular
(define (r5 arg)
             (map r5-helper arg))

;r1 kuralini uygular
(define (r1 arg1 arg2)
             (append (not-yok arg1)
                     (map (lambda (x)  (cadr x)) (not-var arg2))))
;r2 kuralinin sol taraf icin gecerli olanini uygular
(define (r2-sol arg)
            (append (and-yok arg)
                    (birlesme (map cdr (and-var arg)))))
;r2 kuralinin sag taraf icin gecerli olanini uygular
(define (r2-sag arg)
           (append (or-yok arg)
                   (birlesme (map cdr (or-var arg)))))
;listenin icindeki sublistleri birlestirir
(define (birlesme arg)
            (if (null? arg) arg
                (append (birlesme (cdr arg)) (car arg)))) 
;r3 kuralini uygular
(define (r3 arg)
            (map (lambda (x) (cons x (append (cdr (or-var arg))
                                             (or-yok arg))))
                                                                    (cdar (or-var arg))))
;r4 kuralini uygular
(define (r4 arg)
      (map (lambda (x) (cons x (append (cdr (and-var arg))
                                         (and-yok arg)))) (cdar (and-var arg))))
;ilk argumanini parcalayarak teker teker wange ilk arguman olarak yollar 
(define (r3-gonderme arg1 arg2)
          (and (wang (car arg1) arg2)
                (if (null? (cdr  arg1)) #t
                    (r3-gonderme (cdr arg1) arg2)))) 
;ikinci argumanini parcalayarak teker teker wange ikinci arguman olarak yollar
(define (r4-gonderme arg1 arg2) 
          (and (wang arg1 (car arg2))
                (if (null? (cdr  arg2)) #t
                    (r4-gonderme arg1 (cdr arg2))))) 
;bir listin icinde sublist olup olmadigina bakar (r7 icin)
(define (list-var-mi arg )
         (cond ((null?  arg) #t)
               ((list? (car arg)) #f)
                (else (list-var-mi (cdr arg)))))

;tabiki muhtesem WANG
(define (wang arg1 arg2)
          (cond ((and (axiom? arg1 arg2)
                      (list-var-mi (append arg1 arg2))) #t)
                ((not (null? (not-var (append arg1 arg2)))) (wang (r1 arg1 arg2) (r1 arg2 arg1)))
                ((not (null? (and-var arg1))) (wang (r2-sol arg1)  arg2))
                ((not (null? (or-var arg2))) (wang arg1 (r2-sag arg2)))             
                ((not (null? (ok-var (append arg1 arg2))))  (wang (r5 arg1) (r5 arg2)))
                ((not (null? (or-var arg1)))  (r3-gonderme (r3 arg1) arg2))
                ((not (null? (and-var arg2))) (r4-gonderme arg1 (r4 arg2)))      
                (else #f)))