		Search-engine friendly clone of the ACL2 documentation.

Faig

Faig-onoff-equiv

We say the objects X and Y are equivalent if they are (1) faig-equiv, and (2) both atoms or both conses.

This might seem kind of strange at first, but it has some nice congruence properties that aren't true of ordinary faig-equiv.

In particular, FAIG operations like faig-eval and faig-restrict generally treat any malformed FAIGs (i.e., atoms) as "X", that is, (t . t). This is nice because in some sense it is conservative with respect to our ordinary interpretation of FAIGs.

Unfortunately, this means that faig-equiv is not sufficient to imply that the car/cdr are aig-equiv. For instance, let x be 5 and let y be (t . t). Then, x and y are faig-equiv, but their cars are not aig-equiv because the car of x is nil, constant false, whereas the car of y is t, constant true.

So, (faig-onoff-equiv x y) corrects for this by insisting that x and y are either both atoms or both conses. This way, the car/cdr of faig-onoff-equiv objects are always aig-equiv.

Function: faig-onoff-equiv

(defun faig-onoff-equiv (x y)
  (and (iff (consp x) (consp y))
       (faig-equiv x y)))

Definitions and Theorems

Function: faig-onoff-equiv

(defun faig-onoff-equiv (x y)
  (and (iff (consp x) (consp y))
       (faig-equiv x y)))

Theorem: faig-onoff-equiv-is-an-equivalence

(defthm faig-onoff-equiv-is-an-equivalence
  (and (booleanp (faig-onoff-equiv x y))
       (faig-onoff-equiv x x)
       (implies (faig-onoff-equiv x y)
                (faig-onoff-equiv y x))
       (implies (and (faig-onoff-equiv x y)
                     (faig-onoff-equiv y z))
                (faig-onoff-equiv x z)))
  :rule-classes (:equivalence))

Theorem: faig-onoff-equiv-refines-faig-equiv

(defthm faig-onoff-equiv-refines-faig-equiv
  (implies (faig-onoff-equiv x y)
           (faig-equiv x y))
  :rule-classes (:refinement))

Theorem: faig-equiv-implies-faig-onoff-equiv-faig-fix-1

(defthm faig-equiv-implies-faig-onoff-equiv-faig-fix-1
  (implies (faig-equiv x x-equiv)
           (faig-onoff-equiv (faig-fix x)
                             (faig-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: faig-onoff-equiv-implies-aig-equiv-car-1

(defthm faig-onoff-equiv-implies-aig-equiv-car-1
  (implies (faig-onoff-equiv x x-equiv)
           (aig-equiv (car x) (car x-equiv)))
  :rule-classes (:congruence))

Theorem: faig-onoff-equiv-implies-aig-equiv-cdr-1

(defthm faig-onoff-equiv-implies-aig-equiv-cdr-1
  (implies (faig-onoff-equiv x x-equiv)
           (aig-equiv (cdr x) (cdr x-equiv)))
  :rule-classes (:congruence))