(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))))))