		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))