(vl-seltrace-usertypes-ok x) → *
Function:
(defun vl-seltrace-usertypes-ok (x) (declare (xargs :guard (vl-seltrace-p x))) (let ((__function__ 'vl-seltrace-usertypes-ok)) (declare (ignorable __function__)) (if (atom x) t (and (vl-selstep-usertypes-ok (car x)) (vl-seltrace-usertypes-ok (cdr x))))))
Theorem:
(defthm vl-seltrace-usertypes-ok-of-append (implies (and (vl-seltrace-usertypes-ok x) (vl-seltrace-usertypes-ok y)) (vl-seltrace-usertypes-ok (append x y))))
Theorem:
(defthm vl-seltrace-usertypes-ok-of-rev (implies (vl-seltrace-usertypes-ok x) (vl-seltrace-usertypes-ok (rev x))))
Theorem:
(defthm vl-datatype-resolved-p-of-first-seltrace (implies (and (vl-seltrace-usertypes-ok x) (consp x)) (vl-datatype-resolved-p (vl-selstep->type (car x)))))
Theorem:
(defthm vl-seltrace-usertypes-ok-of-vl-seltrace-fix-x (equal (vl-seltrace-usertypes-ok (vl-seltrace-fix x)) (vl-seltrace-usertypes-ok x)))
Theorem:
(defthm vl-seltrace-usertypes-ok-vl-seltrace-equiv-congruence-on-x (implies (vl-seltrace-equiv x x-equiv) (equal (vl-seltrace-usertypes-ok x) (vl-seltrace-usertypes-ok x-equiv))) :rule-classes :congruence)