other
(in-package "ACL2")
negative-syntaxpfunction
(defun negative-syntaxp (term) (if (not (consp term)) nil (case (car term) '(and (rationalp (cadr term)) (< (cadr term) 0)) (unary-- (not (negative-syntaxp (cadr term)))) (binary-+ (and (negative-syntaxp (cadr term)) (negative-syntaxp (caddr term)))) (binary-* (and (or (and (negative-syntaxp (cadr term)) (not (negative-syntaxp (caddr term)))) (and (not (negative-syntaxp (cadr term))) (negative-syntaxp (caddr term)))))) (otherwise nil))))