		Search-engine friendly clone of the ACL2 documentation.

Vcd.lisp

Vcd-wire->width

Signature
(vcd-wire->width x) → width
Arguments: x — Guard (vcd-wire-p x).
Returns: width — Type (natp width).

Definitions and Theorems

Function: vcd-wire->width

(defun vcd-wire->width (x)
  (declare (xargs :guard (vcd-wire-p x)))
  (let ((__function__ 'vcd-wire->width))
    (declare (ignorable __function__))
    (b* (((vcd-wire x) x))
      (+ 1 (abs (- x.msb x.lsb))))))

Theorem: natp-of-vcd-wire->width

(defthm natp-of-vcd-wire->width
  (b* ((width (vcd-wire->width x)))
    (natp width))
  :rule-classes :type-prescription)

Theorem: vcd-wire->width-of-vcd-wire-fix-x

(defthm vcd-wire->width-of-vcd-wire-fix-x
  (equal (vcd-wire->width (vcd-wire-fix x))
         (vcd-wire->width x)))

Theorem: vcd-wire->width-vcd-wire-equiv-congruence-on-x

(defthm vcd-wire->width-vcd-wire-equiv-congruence-on-x
  (implies (vcd-wire-equiv x x-equiv)
           (equal (vcd-wire->width x)
                  (vcd-wire->width x-equiv)))
  :rule-classes :congruence)