		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-bitmux

Signature
(s4vec-bitmux test then else) → mux
Arguments: test — Guard (sparseint-p test).; then — Guard (s4vec-p then).; else — Guard (s4vec-p else).
Returns: mux — Type (s4vec-p mux).

Definitions and Theorems

Function: s4vec-bitmux

(defun s4vec-bitmux (test then else)
 (declare (xargs :guard (and (sparseint-p test)
                             (s4vec-p then)
                             (s4vec-p else))))
 (let ((__function__ 's4vec-bitmux))
  (declare (ignorable __function__))
  (b* (((s4vec then))
       ((s4vec else))
       ((when (sparseint-equal test -1))
        (s4vec-fix then))
       ((when (sparseint-equal test 0))
        (s4vec-fix else)))
    (s4vec (bitops::sparseint-bitite test then.upper else.upper)
           (bitops::sparseint-bitite test then.lower else.lower)))))

Theorem: s4vec-p-of-s4vec-bitmux

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

Theorem: s4vec-bitmux-correct

(defthm s4vec-bitmux-correct
  (b* ((?mux (s4vec-bitmux test then else)))
    (equal (s4vec->4vec mux)
           (4vec-bitmux (sparseint-val test)
                        (s4vec->4vec then)
                        (s4vec->4vec else)))))

Theorem: s4vec-bitmux-of-sparseint-fix-test

(defthm s4vec-bitmux-of-sparseint-fix-test
  (equal (s4vec-bitmux (sparseint-fix test)
                       then else)
         (s4vec-bitmux test then else)))

Theorem: s4vec-bitmux-sparseint-equiv-congruence-on-test

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

Theorem: s4vec-bitmux-of-s4vec-fix-then

(defthm s4vec-bitmux-of-s4vec-fix-then
  (equal (s4vec-bitmux test (s4vec-fix then)
                       else)
         (s4vec-bitmux test then else)))

Theorem: s4vec-bitmux-s4vec-equiv-congruence-on-then

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

Theorem: s4vec-bitmux-of-s4vec-fix-else

(defthm s4vec-bitmux-of-s4vec-fix-else
  (equal (s4vec-bitmux test then (s4vec-fix else))
         (s4vec-bitmux test then else)))

Theorem: s4vec-bitmux-s4vec-equiv-congruence-on-else

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