		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