Recognizer for terms that call only :logic-mode function symbols
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.
Function: logic-termp
(defun logic-termp (x wrld) (declare (xargs :guard (plist-worldp-with-formals wrld))) (and (termp x wrld) (logic-fnsp x wrld)))
