		Search-engine friendly clone of the ACL2 documentation.

Built-in-theorems

Built-in-theorems-about-system-utilities

Built-in theorems about system utilities.

Theorem: pseudo-term-listp-forward-to-true-listp

(defthm pseudo-term-listp-forward-to-true-listp
        (implies (pseudo-term-listp x)
                 (true-listp x))
        :rule-classes :forward-chaining)

Theorem: legal-variable-or-constant-namep-implies-symbolp

(defthm legal-variable-or-constant-namep-implies-symbolp
        (implies (not (symbolp x))
                 (not (legal-variable-or-constant-namep x))))

Theorem: termp-implies-pseudo-termp

(defthm termp-implies-pseudo-termp
        (implies (termp x w) (pseudo-termp x))
        :rule-classes (:rewrite :forward-chaining))

Theorem: term-listp-implies-pseudo-term-listp

(defthm term-listp-implies-pseudo-term-listp
        (implies (term-listp x w)
                 (pseudo-term-listp x))
        :rule-classes (:rewrite :forward-chaining))

Theorem: arities-okp-implies-arity

(defthm arities-okp-implies-arity
        (implies (and (arities-okp user-table w)
                      (assoc fn user-table))
                 (equal (arity fn w)
                        (cdr (assoc fn user-table)))))

Theorem: arities-okp-implies-logicp

(defthm arities-okp-implies-logicp
        (implies (and (arities-okp user-table w)
                      (assoc fn user-table))
                 (logicp fn w)))