		Search-engine friendly clone of the ACL2 documentation.

Primitive-functions

Eval-bad-atom<=

Evaluation semantics of bad-atom<=.

Signature
(eval-bad-atom<= x y) → result
Arguments: x — Guard (valuep x).; y — Guard (valuep y).
Returns: result — Type (valuep result).

The guard of this function requires bad atoms, which we do not model in our formalization. It looks like the raw Lisp code of this function returns nil. So we do the same here.

Definitions and Theorems

Function: eval-bad-atom<=

(defun eval-bad-atom<= (x y)
       (declare (xargs :guard (and (valuep x) (valuep y))))
       (declare (ignore x y))
       (let ((__function__ 'eval-bad-atom<=))
            (declare (ignorable __function__))
            (value-nil)))

Theorem: valuep-of-eval-bad-atom<=

(defthm valuep-of-eval-bad-atom<=
        (b* ((result (eval-bad-atom<= x y)))
            (valuep result))
        :rule-classes :rewrite)

Theorem: eval-bad-atom<=-of-value-fix-x

(defthm eval-bad-atom<=-of-value-fix-x
        (equal (eval-bad-atom<= (value-fix x) y)
               (eval-bad-atom<= x y)))

Theorem: eval-bad-atom<=-value-equiv-congruence-on-x

(defthm eval-bad-atom<=-value-equiv-congruence-on-x
        (implies (value-equiv x x-equiv)
                 (equal (eval-bad-atom<= x y)
                        (eval-bad-atom<= x-equiv y)))
        :rule-classes :congruence)

Theorem: eval-bad-atom<=-of-value-fix-y

(defthm eval-bad-atom<=-of-value-fix-y
        (equal (eval-bad-atom<= x (value-fix y))
               (eval-bad-atom<= x y)))

Theorem: eval-bad-atom<=-value-equiv-congruence-on-y

(defthm eval-bad-atom<=-value-equiv-congruence-on-y
        (implies (value-equiv y y-equiv)
                 (equal (eval-bad-atom<= x y)
                        (eval-bad-atom<= x y-equiv)))
        :rule-classes :congruence)