		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-wildeq-bit

Signature
(a4vec-wildeq-bit au al bu bl) → (mv wildeq-p-upper wildeq-p-lower)
Arguments: au — aig.
Returns: wildeq-p-upper — aig.; wildeq-p-lower — aig.

Definitions and Theorems

Function: a4vec-wildeq-bit

(defun a4vec-wildeq-bit (au al bu bl)
  (declare (xargs :guard t))
  (let ((__function__ 'a4vec-wildeq-bit))
    (declare (ignorable __function__))
    (b* ((bxz (aig-xor bl bu))
         ((when (eq bxz t)) (mv t t))
         (axz (aig-xor au al))
         ((when (eq axz t)) (mv t bxz))
         (a=b (aig-iff au bu)))
      (mv (aig-or a=b bxz axz)
          (aig-or bxz (aig-and a=b (aig-not axz)))))))

Theorem: a4vec-wildeq-bit-eval

(defthm a4vec-wildeq-bit-eval
  (b* (((mv ?upper ?lower)
        (a4vec-wildeq-bit a.upper a.lower b.upper b.lower)))
    (and (equal (aig-eval upper env)
                (or (iff (aig-eval a.upper env)
                         (aig-eval b.upper env))
                    (xor (aig-eval b.upper env)
                         (aig-eval b.lower env))
                    (xor (aig-eval a.upper env)
                         (aig-eval a.lower env))))
         (equal (aig-eval lower env)
                (or (xor (aig-eval b.upper env)
                         (aig-eval b.lower env))
                    (and (iff (aig-eval a.upper env)
                              (aig-eval b.upper env))
                         (iff (aig-eval a.lower env)
                              (aig-eval b.lower env))))))))