		Search-engine friendly clone of the ACL2 documentation.

Sparseint

Sparseint-bitite

Compute the bitwise if-then-else of the three sparseint inputs.

Signature
(sparseint-bitite test then else) → ite
Arguments: test — Guard (sparseint-p test).; then — Guard (sparseint-p then).; else — Guard (sparseint-p else).
Returns: ite — Type (sparseint-p ite).

Definitions and Theorems

Function: sparseint-bitite

(defun sparseint-bitite (test then else)
  (declare (xargs :guard (and (sparseint-p test)
                              (sparseint-p then)
                              (sparseint-p else))))
  (let ((__function__ 'sparseint-bitite))
    (declare (ignorable __function__))
    (b* ((test (sparseint-fix test))
         (then (sparseint-fix then))
         (else (sparseint-fix else))
         (test.height (sparseint$-height test))
         ((mv test&then test&then.height)
          (sparseint$-binary-bitop-offset
               8 test test.height
               0 then (sparseint$-height then)))
         ((mv ~test&else ~test&else.height)
          (sparseint$-binary-bitop-offset
               4 test test.height
               0 else (sparseint$-height else)))
         ((mv if ?if.height)
          (sparseint$-binary-bitop-offset
               14 test&then test&then.height
               0 ~test&else ~test&else.height)))
      if)))

Theorem: sparseint-p-of-sparseint-bitite

(defthm sparseint-p-of-sparseint-bitite
  (b* ((ite (sparseint-bitite test then else)))
    (sparseint-p ite))
  :rule-classes :rewrite)

Theorem: sparseint-bitite-correct

(defthm sparseint-bitite-correct
  (b* ((?ite (sparseint-bitite test then else)))
    (equal (sparseint-val ite)
           (logite (sparseint-val test)
                   (sparseint-val then)
                   (sparseint-val else)))))

Theorem: sparseint-bitite-of-sparseint-fix-test

(defthm sparseint-bitite-of-sparseint-fix-test
  (equal (sparseint-bitite (sparseint-fix test)
                           then else)
         (sparseint-bitite test then else)))

Theorem: sparseint-bitite-sparseint-equiv-congruence-on-test

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

Theorem: sparseint-bitite-of-sparseint-fix-then

(defthm sparseint-bitite-of-sparseint-fix-then
  (equal (sparseint-bitite test (sparseint-fix then)
                           else)
         (sparseint-bitite test then else)))

Theorem: sparseint-bitite-sparseint-equiv-congruence-on-then

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

Theorem: sparseint-bitite-of-sparseint-fix-else

(defthm sparseint-bitite-of-sparseint-fix-else
  (equal (sparseint-bitite test then (sparseint-fix else))
         (sparseint-bitite test then else)))

Theorem: sparseint-bitite-sparseint-equiv-congruence-on-else

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