		Search-engine friendly clone of the ACL2 documentation.

A4vec-parity

Aig-parity-s

Signature
(aig-parity-s x) → *
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: aig-parity-s

(defun aig-parity-s (x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'aig-parity-s))
    (declare (ignorable __function__))
    (b* (((mv xf xr xe) (gl::first/rest/end x)))
      (if xe nil
        (aig-xor xf (aig-parity-s xr))))))

Theorem: aig-parity-s-correct

(defthm aig-parity-s-correct
  (let ((xv (aig-list->s x env)))
    (implies (<= 0 xv)
             (equal (aig-eval (aig-parity-s x) env)
                    (bit->bool (parity (+ 1 (integer-length xv))
                                       xv))))))

Theorem: aig-parity-s-of-list-fix-x

(defthm aig-parity-s-of-list-fix-x
  (equal (aig-parity-s (list-fix x))
         (aig-parity-s x)))

Theorem: aig-parity-s-list-equiv-congruence-on-x

(defthm aig-parity-s-list-equiv-congruence-on-x
  (implies (list-equiv x x-equiv)
           (equal (aig-parity-s x)
                  (aig-parity-s x-equiv)))
  :rule-classes :congruence)