		Search-engine friendly clone of the ACL2 documentation.

Pseudo-lambda

Pseudo-lambda->body

Signature
(pseudo-lambda->body x) → body
Arguments: x — Guard (pseudo-lambda-p x).
Returns: body — Type (pseudo-termp body).

Definitions and Theorems

Function: pseudo-lambda->body

(defun pseudo-lambda->body (x)
  (declare (xargs :guard (pseudo-lambda-p x)))
  (let ((__function__ 'pseudo-lambda->body))
    (declare (ignorable __function__))
    (mbe :logic (pseudo-term-fix (caddr x))
         :exec (caddr x))))

Theorem: pseudo-termp-of-pseudo-lambda->body

(defthm pseudo-termp-of-pseudo-lambda->body
  (b* ((body (pseudo-lambda->body x)))
    (pseudo-termp body))
  :rule-classes :rewrite)

Theorem: pseudo-lambda->body-of-pseudo-lambda-fix-x

(defthm pseudo-lambda->body-of-pseudo-lambda-fix-x
  (equal (pseudo-lambda->body (pseudo-lambda-fix x))
         (pseudo-lambda->body x)))

Theorem: pseudo-lambda->body-pseudo-lambda-equiv-congruence-on-x

(defthm pseudo-lambda->body-pseudo-lambda-equiv-congruence-on-x
  (implies (pseudo-lambda-equiv x x-equiv)
           (equal (pseudo-lambda->body x)
                  (pseudo-lambda->body x-equiv)))
  :rule-classes :congruence)