		Search-engine friendly clone of the ACL2 documentation.

Untranslate-for-execution

Ute-term-p

Recognize the kinds of terms that can be processed by untranslate-for-execution.

Signature
(ute-term-p x) → *

These are similar to pseudo-termps, but we also explicitly support mv-let and mv forms.

Theorem: ute-termlist-p-when-atom

(defthm ute-termlist-p-when-atom
        (implies (atom x)
                 (equal (ute-termlist-p x) (not x))))

Theorem: ute-termlist-p-of-cons

(defthm ute-termlist-p-of-cons
        (equal (ute-termlist-p (cons a x))
               (and (ute-term-p a)
                    (ute-termlist-p x))))

Theorem: true-listp-when-ute-termlist-p

(defthm true-listp-when-ute-termlist-p
        (implies (ute-termlist-p x)
                 (true-listp x))
        :rule-classes :compound-recognizer)

Theorem: ute-term-p-of-car-when-ute-termlist-p

(defthm ute-term-p-of-car-when-ute-termlist-p
        (implies (ute-termlist-p x)
                 (ute-term-p (car x))))

Theorem: ute-termlist-p-of-cdr-when-ute-termlist-p

(defthm ute-termlist-p-of-cdr-when-ute-termlist-p
        (implies (ute-termlist-p x)
                 (ute-termlist-p (cdr x))))

Theorem: ute-termlist-p-of-append

(defthm ute-termlist-p-of-append
        (equal (ute-termlist-p (append x y))
               (and (ute-termlist-p (list-fix x))
                    (ute-termlist-p y))))

Theorem: ute-termlist-p-of-rev

(defthm ute-termlist-p-of-rev
        (equal (ute-termlist-p (rev x))
               (ute-termlist-p (list-fix x))))

Subtopics

Ute-termlist-p