		Search-engine friendly clone of the ACL2 documentation.

Fn-desc-p

Signature
(fn-desc-p x) → *

Definitions and Theorems

Function: fn-desc-p

(defun fn-desc-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'fn-desc-p))
    (declare (ignorable __function__))
    (or (null x)
        (and (true-listp x)
             (symbolp (car x))
             (eqlable-alistp (cdr x))))))

Function: fn-desc-fix

(defun fn-desc-fix (x)
  (declare (xargs :guard (fn-desc-p x)))
  (let ((__function__ 'fn-desc-fix))
    (declare (ignorable __function__))
    (mbe :logic (if (fn-desc-p x) x 'nil)
         :exec x)))

Function: fn-desc-equiv$inline

(defun fn-desc-equiv$inline (x y)
  (declare (xargs :guard (and (fn-desc-p x) (fn-desc-p y))))
  (equal (fn-desc-fix x) (fn-desc-fix y)))

Theorem: fn-desc-equiv-is-an-equivalence

(defthm fn-desc-equiv-is-an-equivalence
  (and (booleanp (fn-desc-equiv x y))
       (fn-desc-equiv x x)
       (implies (fn-desc-equiv x y)
                (fn-desc-equiv y x))
       (implies (and (fn-desc-equiv x y)
                     (fn-desc-equiv y z))
                (fn-desc-equiv x z)))
  :rule-classes (:equivalence))

Theorem: fn-desc-equiv-implies-equal-fn-desc-fix-1

(defthm fn-desc-equiv-implies-equal-fn-desc-fix-1
  (implies (fn-desc-equiv x x-equiv)
           (equal (fn-desc-fix x)
                  (fn-desc-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: fn-desc-fix-under-fn-desc-equiv

(defthm fn-desc-fix-under-fn-desc-equiv
  (fn-desc-equiv (fn-desc-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))