(svtv-concat->lhs x modidx moddb aliases) → (mv errs lhs)
Function:
(defun svtv-concat->lhs (x modidx moddb aliases) (declare (xargs :stobjs (moddb aliases))) (declare (xargs :guard (and (string-listp x) (natp modidx) (moddb-ok moddb)))) (declare (xargs :guard (svtv-mod-alias-guard modidx moddb aliases))) (let ((__function__ 'svtv-concat->lhs)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv err1 first) (svtv-1wire->lhs (car x) modidx moddb aliases)) ((mv errs rest) (svtv-concat->lhs (cdr x) modidx moddb aliases))) (if err1 (mv (cons err1 errs) nil) (mv errs (append first rest))))))
Theorem:
(defthm lhs-p-of-svtv-concat->lhs.lhs (b* (((mv ?errs ?lhs) (svtv-concat->lhs x modidx moddb aliases))) (lhs-p lhs)) :rule-classes :rewrite)
Theorem:
(defthm svtv-concat->lhs-of-string-list-fix-x (equal (svtv-concat->lhs (str::string-list-fix x) modidx moddb aliases) (svtv-concat->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-concat->lhs-string-list-equiv-congruence-on-x (implies (str::string-list-equiv x x-equiv) (equal (svtv-concat->lhs x modidx moddb aliases) (svtv-concat->lhs x-equiv modidx moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-concat->lhs-of-nfix-modidx (equal (svtv-concat->lhs x (nfix modidx) moddb aliases) (svtv-concat->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-concat->lhs-nat-equiv-congruence-on-modidx (implies (nat-equiv modidx modidx-equiv) (equal (svtv-concat->lhs x modidx moddb aliases) (svtv-concat->lhs x modidx-equiv moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-concat->lhs-of-moddb-fix-moddb (equal (svtv-concat->lhs x modidx (moddb-fix moddb) aliases) (svtv-concat->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-concat->lhs-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (svtv-concat->lhs x modidx moddb aliases) (svtv-concat->lhs x modidx moddb-equiv aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-concat->lhs-of-lhslist-fix-aliases (equal (svtv-concat->lhs x modidx moddb (lhslist-fix aliases)) (svtv-concat->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-concat->lhs-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-concat->lhs x modidx moddb aliases) (svtv-concat->lhs x modidx moddb aliases-equiv))) :rule-classes :congruence)