recognizer for the quotation of a term

Example: (termp '(CAR (CONS X Y)) (w state)) General Form: (termp x w)

where

Each metafunction (see `meta`) is supposed to take (the quotation of)
a translated term as input and yield (the quotation of) a translated term as
output. When a metafunction is run by the simplifier its input is guaranteed
to be well-formed by invariants maintained by ACL2. But its output is checked
by an explicit call of `set-skip-meta-termp-checks`.

`Termp` is mutually recursive with `term-listp`.

**Function: **

(defun termp (x w) (declare (xargs :guard (plist-worldp-with-formals w))) (cond ((atom x) (legal-variablep x)) ((eq (car x) 'quote) (and (consp (cdr x)) (null (cddr x)))) ((symbolp (car x)) (let ((arity (arity (car x) w))) (and arity (term-listp (cdr x) w) (eql (length (cdr x)) arity)))) ((and (consp (car x)) (true-listp (car x)) (eq (car (car x)) 'lambda) (eql 3 (length (car x))) (arglistp (cadr (car x))) (termp (caddr (car x)) w) (null (set-difference-eq (all-vars (caddr (car x))) (cadr (car x)))) (term-listp (cdr x) w) (eql (length (cadr (car x))) (length (cdr x)))) t) (t nil)))

**Function: **

(defun term-listp (x w) (declare (xargs :guard (plist-worldp-with-formals w))) (cond ((atom x) (equal x nil)) ((termp (car x) w) (term-listp (cdr x) w)) (t nil)))

- Logic-fns-list-listp
- Recognizer for when a given list of lists of terms calls only
: `logic`-mode function symbols - Logic-fnsp
- Recognizer for when a given term calls only
: `logic`-mode function symbols - Logic-fns-listp
- Recognizer for when a given list of terms calls only
: `logic`-mode function symbols - Logic-termp
- Recognizer for terms that call only
: `logic`-mode function symbols - Logic-term-list-listp
- Recognizer for lists of lists of terms that call only
: `logic`-mode function symbols - Logic-term-listp
- Recognizer for lists of terms that call only
: `logic`-mode function symbols