		Search-engine friendly clone of the ACL2 documentation.

4v-operations

4v-pullup

Four-valued semantics for a pullup resistor.

(4v-pullup a) acts just like a buffer except that, if its input is floating, it instead produces true. That is, it returns the value specified by the following truth table:

  a  |  out
-----+-------
  F  |   F
  T  |   T
  X  |   X
  Z  |   T

Definitions and Theorems

Function: 4v-pullup

(defun 4v-pullup (a)
       (declare (xargs :guard t))
       (4vcases a (t (4vt))
                (z (4vt))
                (f (4vf))
                (& (4vx))))

Theorem: 4v-equiv-implies-equal-4v-pullup-1

(defthm 4v-equiv-implies-equal-4v-pullup-1
        (implies (4v-equiv a a-equiv)
                 (equal (4v-pullup a)
                        (4v-pullup a-equiv)))
        :rule-classes (:congruence))