		Search-engine friendly clone of the ACL2 documentation.

Operations

Bitior-values

Apply | to values [C:6.5.12/2] [C:6.5.12/3] [C:6.5.12/4].

Signature
(bitior-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (value-resultp resval).

It is an error if the values are not integers. If they are integers, we perform the usual arithmetic conversions and then we call the operation on integer values.

Definitions and Theorems

Function: bitior-values

(defun bitior-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (let ((__function__ 'bitior-values))
    (declare (ignorable __function__))
    (if (and (value-integerp val1)
             (value-integerp val2))
        (b* (((mv val1 val2)
              (uaconvert-values val1 val2)))
          (bitior-integer-values val1 val2))
      (error (list :bitand-mistype :required :integer
                   :integer :supplied (value-fix val1)
                   (value-fix val2))))))

Theorem: value-resultp-of-bitior-values

(defthm value-resultp-of-bitior-values
  (b* ((resval (bitior-values val1 val2)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: bitior-values-of-value-fix-val1

(defthm bitior-values-of-value-fix-val1
  (equal (bitior-values (value-fix val1) val2)
         (bitior-values val1 val2)))

Theorem: bitior-values-value-equiv-congruence-on-val1

(defthm bitior-values-value-equiv-congruence-on-val1
  (implies (value-equiv val1 val1-equiv)
           (equal (bitior-values val1 val2)
                  (bitior-values val1-equiv val2)))
  :rule-classes :congruence)

Theorem: bitior-values-of-value-fix-val2

(defthm bitior-values-of-value-fix-val2
  (equal (bitior-values val1 (value-fix val2))
         (bitior-values val1 val2)))

Theorem: bitior-values-value-equiv-congruence-on-val2

(defthm bitior-values-value-equiv-congruence-on-val2
  (implies (value-equiv val2 val2-equiv)
           (equal (bitior-values val1 val2)
                  (bitior-values val1 val2-equiv)))
  :rule-classes :congruence)