		Search-engine friendly clone of the ACL2 documentation.

Faig-constructors

F-aig-res

(f-aig-res x y) constructs a FAIG that represents the result of connecting two (independently driven) wires together.

Signature
(f-aig-res x y) → *

See 4v-res to understand what this is doing. This is just the faig equivalent.

Definitions and Theorems

Function: f-aig-res

(defun f-aig-res (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'f-aig-res))
    (declare (ignorable __function__))
    (b* (((faig x1 x0) x) ((faig y1 y0) y))
      (cons (aig-or x1 y1) (aig-or x0 y0)))))

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

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

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

(defthm faig-fix-equiv-implies-equal-f-aig-res-1
  (implies (faig-fix-equiv x x-equiv)
           (equal (f-aig-res x y)
                  (f-aig-res x-equiv y)))
  :rule-classes (:congruence))

Theorem: faig-fix-equiv-implies-equal-f-aig-res-2

(defthm faig-fix-equiv-implies-equal-f-aig-res-2
  (implies (faig-fix-equiv y y-equiv)
           (equal (f-aig-res x y)
                  (f-aig-res x y-equiv)))
  :rule-classes (:congruence))