		Search-engine friendly clone of the ACL2 documentation.

Vcd.lisp

Vcd-print-4vec-aux

Signature
(vcd-print-4vec-aux upper lower firstbit p) → p1
Arguments: upper — Guard (integerp upper).; lower — Guard (integerp lower).; firstbit — Guard (natp firstbit).; p — Guard (vl-printedlist-p p).
Returns: p1 — Type (vl-printedlist-p p1).

Definitions and Theorems

Function: vcd-print-4vec-aux

(defun vcd-print-4vec-aux (upper lower firstbit p)
  (declare (xargs :guard (and (integerp upper)
                              (integerp lower)
                              (natp firstbit)
                              (vl-printedlist-p p))))
  (let ((__function__ 'vcd-print-4vec-aux))
    (declare (ignorable __function__))
    (b* (((when (zp firstbit))
          (vl::vl-printedlist-fix p))
         (firstbit (1- firstbit))
         (ubit (logbitp firstbit upper))
         (lbit (logbitp firstbit lower))
         (char (if ubit (if lbit #\1 #\x)
                 (if lbit #\z #\0))))
      (vcd-print-4vec-aux upper lower firstbit (cons char p)))))

Theorem: vl-printedlist-p-of-vcd-print-4vec-aux

(defthm vl-printedlist-p-of-vcd-print-4vec-aux
  (b* ((p1 (vcd-print-4vec-aux upper lower firstbit p)))
    (vl-printedlist-p p1))
  :rule-classes :rewrite)

Theorem: vcd-print-4vec-aux-of-ifix-upper

(defthm vcd-print-4vec-aux-of-ifix-upper
  (equal (vcd-print-4vec-aux (ifix upper)
                             lower firstbit p)
         (vcd-print-4vec-aux upper lower firstbit p)))

Theorem: vcd-print-4vec-aux-int-equiv-congruence-on-upper

(defthm vcd-print-4vec-aux-int-equiv-congruence-on-upper
 (implies (int-equiv upper upper-equiv)
          (equal (vcd-print-4vec-aux upper lower firstbit p)
                 (vcd-print-4vec-aux upper-equiv lower firstbit p)))
 :rule-classes :congruence)

Theorem: vcd-print-4vec-aux-of-ifix-lower

(defthm vcd-print-4vec-aux-of-ifix-lower
  (equal (vcd-print-4vec-aux upper (ifix lower)
                             firstbit p)
         (vcd-print-4vec-aux upper lower firstbit p)))

Theorem: vcd-print-4vec-aux-int-equiv-congruence-on-lower

(defthm vcd-print-4vec-aux-int-equiv-congruence-on-lower
 (implies (int-equiv lower lower-equiv)
          (equal (vcd-print-4vec-aux upper lower firstbit p)
                 (vcd-print-4vec-aux upper lower-equiv firstbit p)))
 :rule-classes :congruence)

Theorem: vcd-print-4vec-aux-of-nfix-firstbit

(defthm vcd-print-4vec-aux-of-nfix-firstbit
  (equal (vcd-print-4vec-aux upper lower (nfix firstbit)
                             p)
         (vcd-print-4vec-aux upper lower firstbit p)))

Theorem: vcd-print-4vec-aux-nat-equiv-congruence-on-firstbit

(defthm vcd-print-4vec-aux-nat-equiv-congruence-on-firstbit
 (implies (nat-equiv firstbit firstbit-equiv)
          (equal (vcd-print-4vec-aux upper lower firstbit p)
                 (vcd-print-4vec-aux upper lower firstbit-equiv p)))
 :rule-classes :congruence)