		Search-engine friendly clone of the ACL2 documentation.

Expand.lisp

Svtv-wire->lhs

Signature
(svtv-wire->lhs x modidx moddb aliases) → (mv errs lhs)
Arguments: modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).
Returns: lhs — Type (lhs-p lhs).

Definitions and Theorems

Function: svtv-wire->lhs

(defun svtv-wire->lhs (x modidx moddb aliases)
 (declare (xargs :stobjs (moddb aliases)))
 (declare (xargs :guard (and (natp modidx) (moddb-ok moddb))))
 (declare
      (xargs :guard (svtv-mod-alias-guard modidx moddb aliases)))
 (let ((__function__ 'svtv-wire->lhs))
   (declare (ignorable __function__))
   (b* (((unless (stringp x))
         (mv (list (msg "SVTV wirenames must be strings; ~x0 is not"
                        x))
             nil)))
     (svtv-wire->lhs! x modidx moddb aliases))))

Theorem: lhs-p-of-svtv-wire->lhs.lhs

(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: svtv-wire->lhs-of-nfix-modidx

(defthm svtv-wire->lhs-of-nfix-modidx
  (equal (svtv-wire->lhs x (nfix modidx)
                         moddb aliases)
         (svtv-wire->lhs x modidx moddb aliases)))

Theorem: svtv-wire->lhs-nat-equiv-congruence-on-modidx

(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: svtv-wire->lhs-of-moddb-fix-moddb

(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: svtv-wire->lhs-moddb-equiv-congruence-on-moddb

(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: svtv-wire->lhs-of-lhslist-fix-aliases

(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: svtv-wire->lhs-lhslist-equiv-congruence-on-aliases

(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)