		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4veclist-p-to-stringp

Converts 4veclist-p into list of strings of 0,1,x,z's msb-first

Signature
(4veclist-p-to-stringp x) → x-string-list
Arguments: x — Guard (4veclist-p x).
Returns: x-string-list — Type (string-listp x-string-list).

Definitions and Theorems

Function: 4veclist-p-to-stringp

(defun 4veclist-p-to-stringp (x)
  (declare (xargs :guard (4veclist-p x)))
  (let ((__function__ '4veclist-p-to-stringp))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (4vec-p-to-stringp (car x))
            (4veclist-p-to-stringp (cdr x))))))

Theorem: string-listp-of-4veclist-p-to-stringp

(defthm string-listp-of-4veclist-p-to-stringp
  (b* ((x-string-list (4veclist-p-to-stringp x)))
    (string-listp x-string-list))
  :rule-classes :rewrite)