(svtv-fsm-add-names names x &key (top 'nil) (moddb 'moddb) (aliases 'aliases)) → (mv err new-fsm)
Function:
(defun svtv-fsm-add-names-fn (names x top moddb aliases) (declare (xargs :stobjs (moddb aliases))) (declare (xargs :guard (and (svtv-namemap-p names) (svtv-fsm-p x) (modname-p top) (moddb-ok moddb)))) (declare (xargs :guard (svtv-fsm-mod-alias-guard top moddb aliases))) (let ((__function__ 'svtv-fsm-add-names)) (declare (ignorable __function__)) (b* (((svtv-fsm x)) ((mv errs lhsmap) (svtv-namemap->lhsmap names (moddb-modname-get-index top moddb) moddb aliases)) ((when errs) (mv (msg-list errs) nil))) (mv nil (change-svtv-fsm x :namemap (append lhsmap x.namemap))))))
Theorem:
(defthm return-type-of-svtv-fsm-add-names.new-fsm (b* (((mv ?err ?new-fsm) (svtv-fsm-add-names-fn names x top moddb aliases))) (implies (not err) (svtv-fsm-p new-fsm))) :rule-classes :rewrite)
Theorem:
(defthm svtv-fsm-add-names-fn-of-svtv-namemap-fix-names (equal (svtv-fsm-add-names-fn (svtv-namemap-fix names) x top moddb aliases) (svtv-fsm-add-names-fn names x top moddb aliases)))
Theorem:
(defthm svtv-fsm-add-names-fn-svtv-namemap-equiv-congruence-on-names (implies (svtv-namemap-equiv names names-equiv) (equal (svtv-fsm-add-names-fn names x top moddb aliases) (svtv-fsm-add-names-fn names-equiv x top moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-fsm-add-names-fn-of-svtv-fsm-fix-x (equal (svtv-fsm-add-names-fn names (svtv-fsm-fix x) top moddb aliases) (svtv-fsm-add-names-fn names x top moddb aliases)))
Theorem:
(defthm svtv-fsm-add-names-fn-svtv-fsm-equiv-congruence-on-x (implies (svtv-fsm-equiv x x-equiv) (equal (svtv-fsm-add-names-fn names x top moddb aliases) (svtv-fsm-add-names-fn names x-equiv top moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-fsm-add-names-fn-of-modname-fix-top (equal (svtv-fsm-add-names-fn names x (modname-fix top) moddb aliases) (svtv-fsm-add-names-fn names x top moddb aliases)))
Theorem:
(defthm svtv-fsm-add-names-fn-modname-equiv-congruence-on-top (implies (modname-equiv top top-equiv) (equal (svtv-fsm-add-names-fn names x top moddb aliases) (svtv-fsm-add-names-fn names x top-equiv moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-fsm-add-names-fn-of-moddb-fix-moddb (equal (svtv-fsm-add-names-fn names x top (moddb-fix moddb) aliases) (svtv-fsm-add-names-fn names x top moddb aliases)))
Theorem:
(defthm svtv-fsm-add-names-fn-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (svtv-fsm-add-names-fn names x top moddb aliases) (svtv-fsm-add-names-fn names x top moddb-equiv aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-fsm-add-names-fn-of-lhslist-fix-aliases (equal (svtv-fsm-add-names-fn names x top moddb (lhslist-fix aliases)) (svtv-fsm-add-names-fn names x top moddb aliases)))
Theorem:
(defthm svtv-fsm-add-names-fn-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-fsm-add-names-fn names x top moddb aliases) (svtv-fsm-add-names-fn names x top moddb aliases-equiv))) :rule-classes :congruence)