Function:
(defun svtv-wire->lhs! (x modidx moddb aliases) (declare (xargs :stobjs (moddb aliases))) (declare (xargs :guard (and (stringp x) (natp modidx) (moddb-ok moddb)))) (declare (xargs :guard (svtv-mod-alias-guard modidx moddb aliases))) (let ((__function__ 'svtv-wire->lhs!)) (declare (ignorable __function__)) (b* ((toks (strtok x '(#\, #\Newline #\Tab #\Space #\{ #\}))) ((mv errs lhs) (svtv-concat->lhs toks modidx moddb aliases))) (mv errs (lhs-norm lhs)))))
Theorem:
(defthm lhs-p-of-svtv-wire->lhs!.lhs (b* (((mv ?errs ?lhs) (svtv-wire->lhs! x modidx moddb aliases))) (lhs-p lhs)) :rule-classes :rewrite)
Theorem:
(defthm svtv-wire->lhs!-of-str-fix-x (equal (svtv-wire->lhs! (str-fix x) modidx moddb aliases) (svtv-wire->lhs! x modidx moddb aliases)))
Theorem:
(defthm svtv-wire->lhs!-streqv-congruence-on-x (implies (acl2::streqv x x-equiv) (equal (svtv-wire->lhs! x modidx moddb aliases) (svtv-wire->lhs! x-equiv modidx moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-wire->lhs!-of-nfix-modidx (equal (svtv-wire->lhs! x (nfix modidx) moddb aliases) (svtv-wire->lhs! x modidx moddb aliases)))
Theorem:
(defthm svtv-wire->lhs!-nat-equiv-congruence-on-modidx (implies (nat-equiv modidx modidx-equiv) (equal (svtv-wire->lhs! x modidx moddb aliases) (svtv-wire->lhs! x modidx-equiv moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-wire->lhs!-of-moddb-fix-moddb (equal (svtv-wire->lhs! x modidx (moddb-fix moddb) aliases) (svtv-wire->lhs! x modidx moddb aliases)))
Theorem:
(defthm svtv-wire->lhs!-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (svtv-wire->lhs! x modidx moddb aliases) (svtv-wire->lhs! x modidx moddb-equiv aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-wire->lhs!-of-lhslist-fix-aliases (equal (svtv-wire->lhs! x modidx moddb (lhslist-fix aliases)) (svtv-wire->lhs! x modidx moddb aliases)))
Theorem:
(defthm svtv-wire->lhs!-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-wire->lhs! x modidx moddb aliases) (svtv-wire->lhs! x modidx moddb aliases-equiv))) :rule-classes :congruence)