		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-bitmux

Signature
(4vec-bitmux test then else) → mux
Arguments: test — Guard (integerp test).; then — Guard (4vec-p then).; else — Guard (4vec-p else).
Returns: mux — Type (4vec-p mux).

Definitions and Theorems

Function: 4vec-bitmux

(defun 4vec-bitmux (test then else)
  (declare (xargs :guard (and (integerp test)
                              (4vec-p then)
                              (4vec-p else))))
  (let ((__function__ '4vec-bitmux))
    (declare (ignorable __function__))
    (b* (((4vec then)) ((4vec else)))
      (mbe :logic
           (4vec (logite test then.upper else.upper)
                 (logite test then.lower else.lower))
           :exec
           (b* (((when (eql test -1)) then)
                ((when (eql test 0)) else))
             (4vec (logite test then.upper else.upper)
                   (logite test then.lower else.lower)))))))

Theorem: 4vec-p-of-4vec-bitmux

(defthm 4vec-p-of-4vec-bitmux
  (b* ((mux (4vec-bitmux test then else)))
    (4vec-p mux))
  :rule-classes :rewrite)

Theorem: 4vec-bitmux-of-ifix-test

(defthm 4vec-bitmux-of-ifix-test
  (equal (4vec-bitmux (ifix test) then else)
         (4vec-bitmux test then else)))

Theorem: 4vec-bitmux-int-equiv-congruence-on-test

(defthm 4vec-bitmux-int-equiv-congruence-on-test
  (implies (int-equiv test test-equiv)
           (equal (4vec-bitmux test then else)
                  (4vec-bitmux test-equiv then else)))
  :rule-classes :congruence)

Theorem: 4vec-bitmux-of-4vec-fix-then

(defthm 4vec-bitmux-of-4vec-fix-then
  (equal (4vec-bitmux test (4vec-fix then) else)
         (4vec-bitmux test then else)))

Theorem: 4vec-bitmux-4vec-equiv-congruence-on-then

(defthm 4vec-bitmux-4vec-equiv-congruence-on-then
  (implies (4vec-equiv then then-equiv)
           (equal (4vec-bitmux test then else)
                  (4vec-bitmux test then-equiv else)))
  :rule-classes :congruence)

Theorem: 4vec-bitmux-of-4vec-fix-else

(defthm 4vec-bitmux-of-4vec-fix-else
  (equal (4vec-bitmux test then (4vec-fix else))
         (4vec-bitmux test then else)))

Theorem: 4vec-bitmux-4vec-equiv-congruence-on-else

(defthm 4vec-bitmux-4vec-equiv-congruence-on-else
  (implies (4vec-equiv else else-equiv)
           (equal (4vec-bitmux test then else)
                  (4vec-bitmux test then else-equiv)))
  :rule-classes :congruence)