(defun fbf-fun (fbf) 
	(or (negazione fbf) 
            (cong fbf) 
            (disg fbf) 
            (implicazione fbf) 
            (universale fbf) 
            (existenciale fbf)
            (predicato fbf)))
 
(defun negazione (fbf) 
	(and (eq (first fbf) 'not) 
             (fbf-fun (second fbf))
             (= (length fbf) 2)))

(defun cong (fbf)
	(and (eq (first fbf) 'and )
             (reduce (lambda (x y) (and x y))
                             (mapcar #'fbf-fun (rest fbf)))))

(defun disg (fbf)
        (and (eq (first fbf) 'or) 
             (reduce (lambda (x y) (and x y))
                             (mapcar #'fbf-fun (rest fbf)))))

(defun implicazione (fbf)
	(and (eq (first fbf) '==>)
             (fbf-fun (second fbf))
             (fbf-fun (third fbf))
             (= 3 (length fbf))))

(defun universale (fbf)
	(and (eq (first fbf) 'forall) 
             (variabile (second fbf))
             (fbf-fun (third fbf))
             (= 3 (length fbf))))


(defun existenciale (fbf)
	(and (eq (first fbf) 'exist) 
             (variabile (second fbf))
             (fbf-fun (third fbf))
             (= 3 (length fbf))))

(defun costante (fbf)
	(or (numberp fbf)
            (alpha-char-p (char (string 'fbf) 0))))

(defun variabile (fbf)
        (and (symbolp fbf) 
             (char= #\? (char (symbol-name fbf) 0))))

(defun funzione (fbf)	
        (and (symbolp (first fbf)) 
                 (or (reduce (lambda (x y) (and x y))
                             (mapcar #'termine (rest fbf))) 
                     (null (rest fbf)))))

(defun termine (fbf)
	(or (costante fbf) 
            (variabile fbf) 
            (funzione fbf)))

(defun predicato (fbf)
        (or (and (symbolp fbf) 
                 (alpha-char-p (char (string 'fbf) 0)))
            (and (symbolp (first fbf)) 
                 (or (reduce (lambda (x y) (and x y))
                             (mapcar #'termine (rest fbf))) 
                     (null (rest fbf))))))