		Search-engine friendly clone of the ACL2 documentation.

Binary-digits

Bin-digit-value

Numeric value of a Java binary digit.

Signature
(bin-digit-value x) → val
Arguments: x — Guard (bin-digitp x).
Returns: val — Type (bitp val).

Definitions and Theorems

Function: bin-digit-value

(defun bin-digit-value (x)
  (declare (xargs :guard (bin-digitp x)))
  (let ((__function__ 'bin-digit-value))
    (declare (ignorable __function__))
    (if (eql (bin-digit-fix x) (char-code #\0))
        0
      1)))

Theorem: bitp-of-bin-digit-value

(defthm bitp-of-bin-digit-value
  (b* ((val (bin-digit-value x)))
    (bitp val))
  :rule-classes (:rewrite :type-prescription))

Theorem: bin-digit-value-of-bin-digit-fix-x

(defthm bin-digit-value-of-bin-digit-fix-x
  (equal (bin-digit-value (bin-digit-fix x))
         (bin-digit-value x)))

Theorem: bin-digit-value-bin-digit-equiv-congruence-on-x

(defthm bin-digit-value-bin-digit-equiv-congruence-on-x
  (implies (bin-digit-equiv x x-equiv)
           (equal (bin-digit-value x)
                  (bin-digit-value x-equiv)))
  :rule-classes :congruence)