		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-to-faig

Faig-const-<=

Lattice ordering for FAIG constants.

Signature
(faig-const-<= x y) → *

This is just the FAIG equivalent of 4v-<=.

Definitions and Theorems

Function: faig-const-<=

(defun faig-const-<= (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'faig-const-<=))
    (declare (ignorable __function__))
    (let ((x (faig-const-fix x))
          (y (faig-const-fix y)))
      (or (equal x y) (equal x (faig-x))))))

Theorem: faig-const-equiv-implies-equal-faig-const-<=-1

(defthm faig-const-equiv-implies-equal-faig-const-<=-1
  (implies (faig-const-equiv x x-equiv)
           (equal (faig-const-<= x y)
                  (faig-const-<= x-equiv y)))
  :rule-classes (:congruence))

Theorem: faig-const-equiv-implies-equal-faig-const-<=-2

(defthm faig-const-equiv-implies-equal-faig-const-<=-2
  (implies (faig-const-equiv y y-equiv)
           (equal (faig-const-<= x y)
                  (faig-const-<= x y-equiv)))
  :rule-classes (:congruence))