(vl-portdecllist-names-by-direction x in out inout) → (mv in out inout)
Function:
(defun vl-portdecllist-names-by-direction (x in out inout) (declare (xargs :guard (and (vl-portdecllist-p x) (string-listp in) (string-listp out) (string-listp inout)))) (let ((__function__ 'vl-portdecllist-names-by-direction)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (string-list-fix in) (string-list-fix out) (string-list-fix inout))) (decl (car x)) (name (vl-portdecl->name decl)) (dir (vl-portdecl->dir decl))) (case dir (:vl-input (vl-portdecllist-names-by-direction (cdr x) (cons name in) out inout)) (:vl-output (vl-portdecllist-names-by-direction (cdr x) in (cons name out) inout)) (:vl-inout (vl-portdecllist-names-by-direction (cdr x) in out (cons name inout))) (otherwise (progn$ (raise "Impossible") (mv nil nil nil)))))))
Theorem:
(defthm string-listp-of-vl-portdecllist-names-by-direction.in (b* (((mv set::?in ?out ?inout) (vl-portdecllist-names-by-direction x in out inout))) (string-listp in)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-portdecllist-names-by-direction.out (b* (((mv set::?in ?out ?inout) (vl-portdecllist-names-by-direction x in out inout))) (string-listp out)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-portdecllist-names-by-direction.inout (b* (((mv set::?in ?out ?inout) (vl-portdecllist-names-by-direction x in out inout))) (string-listp inout)) :rule-classes :rewrite)
Theorem:
(defthm vl-portdecllist-names-by-direction-of-vl-portdecllist-fix-x (equal (vl-portdecllist-names-by-direction (vl-portdecllist-fix x) in out inout) (vl-portdecllist-names-by-direction x in out inout)))
Theorem:
(defthm vl-portdecllist-names-by-direction-vl-portdecllist-equiv-congruence-on-x (implies (vl-portdecllist-equiv x x-equiv) (equal (vl-portdecllist-names-by-direction x in out inout) (vl-portdecllist-names-by-direction x-equiv in out inout))) :rule-classes :congruence)
Theorem:
(defthm vl-portdecllist-names-by-direction-of-string-list-fix-in (equal (vl-portdecllist-names-by-direction x (string-list-fix in) out inout) (vl-portdecllist-names-by-direction x in out inout)))
Theorem:
(defthm vl-portdecllist-names-by-direction-string-list-equiv-congruence-on-in (implies (str::string-list-equiv in in-equiv) (equal (vl-portdecllist-names-by-direction x in out inout) (vl-portdecllist-names-by-direction x in-equiv out inout))) :rule-classes :congruence)
Theorem:
(defthm vl-portdecllist-names-by-direction-of-string-list-fix-out (equal (vl-portdecllist-names-by-direction x in (string-list-fix out) inout) (vl-portdecllist-names-by-direction x in out inout)))
Theorem:
(defthm vl-portdecllist-names-by-direction-string-list-equiv-congruence-on-out (implies (str::string-list-equiv out out-equiv) (equal (vl-portdecllist-names-by-direction x in out inout) (vl-portdecllist-names-by-direction x in out-equiv inout))) :rule-classes :congruence)
Theorem:
(defthm vl-portdecllist-names-by-direction-of-string-list-fix-inout (equal (vl-portdecllist-names-by-direction x in out (string-list-fix inout)) (vl-portdecllist-names-by-direction x in out inout)))
Theorem:
(defthm vl-portdecllist-names-by-direction-string-list-equiv-congruence-on-inout (implies (str::string-list-equiv inout inout-equiv) (equal (vl-portdecllist-names-by-direction x in out inout) (vl-portdecllist-names-by-direction x in out inout-equiv))) :rule-classes :congruence)