		Search-engine friendly clone of the ACL2 documentation.

Faig-constructors

F-aig-unfloat

(f-aig-unfloat a) converts floating (Z) values to unknown (X) values.

Signature
(f-aig-unfloat a) → *

See 4v-unfloat; this is the analogous function for FAIGs.

Definitions and Theorems

Function: f-aig-unfloat

(defun f-aig-unfloat (a)
  (declare (xargs :guard t))
  (let ((__function__ 'f-aig-unfloat))
    (declare (ignorable __function__))
    (b* (((faig a1 a0) a))
      (cons (aig-not (aig-and a0 (aig-not a1)))
            (aig-not (aig-and a1 (aig-not a0)))))))

Theorem: faig-eval-of-f-aig-unfloat

(defthm faig-eval-of-f-aig-unfloat
  (equal (faig-eval (f-aig-unfloat a) env)
         (f-aig-unfloat (faig-eval a env))))

Theorem: faig-fix-equiv-implies-equal-f-aig-unfloat-1

(defthm faig-fix-equiv-implies-equal-f-aig-unfloat-1
  (implies (faig-fix-equiv a a-equiv)
           (equal (f-aig-unfloat a)
                  (f-aig-unfloat a-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-f-aig-unfloat-1

(defthm faig-equiv-implies-faig-equiv-f-aig-unfloat-1
  (implies (faig-equiv a a-equiv)
           (faig-equiv (f-aig-unfloat a)
                       (f-aig-unfloat a-equiv)))
  :rule-classes (:congruence))