Recognizer for terms that call only :logic-mode
This predicate strengthens (termp x wrld), as it also requires
(logic-fnsp x wrld), i.e., that every function symbol called in x is
in :logic mode in the world, wrld.
(defun logic-termp (x wrld)
(declare (xargs :guard (plist-worldp-with-formals wrld)))
(and (termp x wrld)
(logic-fnsp x wrld)))