		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Pseudo-term-fix

Signature
(pseudo-term-fix x) → xx
Arguments: x — Guard (pseudo-termp x).
Returns: xx — Type (pseudo-termp xx).

Definitions and Theorems

Function: pseudo-term-fix

(defun pseudo-term-fix (x)
  (declare (xargs :guard (pseudo-termp x)))
  (let ((__function__ 'pseudo-term-fix))
    (declare (ignorable __function__))
    (mbe :logic (and (pseudo-termp x) x)
         :exec x)))

Theorem: pseudo-termp-of-pseudo-term-fix

(defthm pseudo-termp-of-pseudo-term-fix
  (b* ((xx (pseudo-term-fix x)))
    (pseudo-termp xx))
  :rule-classes :rewrite)

Theorem: pseudo-term-fix-when-pseudo-termp

(defthm pseudo-term-fix-when-pseudo-termp
  (implies (pseudo-termp x)
           (equal (pseudo-term-fix x) x)))

Function: pseudo-term-equiv$inline

(defun pseudo-term-equiv$inline (x y)
  (declare (xargs :guard (and (pseudo-termp x)
                              (pseudo-termp y))))
  (equal (pseudo-term-fix x)
         (pseudo-term-fix y)))

Theorem: pseudo-term-equiv-is-an-equivalence

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

Theorem: pseudo-term-equiv-implies-equal-pseudo-term-fix-1

(defthm pseudo-term-equiv-implies-equal-pseudo-term-fix-1
  (implies (pseudo-term-equiv x x-equiv)
           (equal (pseudo-term-fix x)
                  (pseudo-term-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: pseudo-term-fix-under-pseudo-term-equiv

(defthm pseudo-term-fix-under-pseudo-term-equiv
  (pseudo-term-equiv (pseudo-term-fix x)
                     x)
  :rule-classes (:rewrite :rewrite-quoted-constant))