Function:
(defun svtv-fsm-mod-alias-guard (top moddb aliases) (declare (xargs :stobjs (moddb aliases))) (declare (xargs :guard (and (modname-p top) (moddb-ok moddb)))) (let ((__function__ 'svtv-fsm-mod-alias-guard)) (declare (ignorable __function__)) (b* ((modidx (moddb-modname-get-index top moddb))) (and modidx (svtv-mod-alias-guard modidx moddb aliases)))))
Theorem:
(defthm svtv-fsm-mod-alias-guard-of-modname-fix-top (equal (svtv-fsm-mod-alias-guard (modname-fix top) moddb aliases) (svtv-fsm-mod-alias-guard top moddb aliases)))
Theorem:
(defthm svtv-fsm-mod-alias-guard-modname-equiv-congruence-on-top (implies (modname-equiv top top-equiv) (equal (svtv-fsm-mod-alias-guard top moddb aliases) (svtv-fsm-mod-alias-guard top-equiv moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-fsm-mod-alias-guard-of-moddb-fix-moddb (equal (svtv-fsm-mod-alias-guard top (moddb-fix moddb) aliases) (svtv-fsm-mod-alias-guard top moddb aliases)))
Theorem:
(defthm svtv-fsm-mod-alias-guard-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (svtv-fsm-mod-alias-guard top moddb aliases) (svtv-fsm-mod-alias-guard top moddb-equiv aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-fsm-mod-alias-guard-of-lhslist-fix-aliases (equal (svtv-fsm-mod-alias-guard top moddb (lhslist-fix aliases)) (svtv-fsm-mod-alias-guard top moddb aliases)))
Theorem:
(defthm svtv-fsm-mod-alias-guard-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-fsm-mod-alias-guard top moddb aliases) (svtv-fsm-mod-alias-guard top moddb aliases-equiv))) :rule-classes :congruence)