(vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr) → scoped-lhs
Function:
(defun vl-instarray-nonreplicated-port-lhs (port-lhs instname instindex instoffset inst-incr) (declare (xargs :guard (and (sv::lhs-p port-lhs) (stringp instname) (integerp instindex) (natp instoffset) (integerp inst-incr)))) (declare (xargs :guard (sv::svarlist-addr-p (sv::lhs-vars port-lhs)))) (let ((__function__ 'vl-instarray-nonreplicated-port-lhs)) (declare (ignorable __function__)) (sv::lhs-add-namespace (string-fix instname) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr))))
Theorem:
(defthm lhs-p-of-vl-instarray-nonreplicated-port-lhs (b* ((scoped-lhs (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr))) (sv::lhs-p scoped-lhs)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-instarray-nonreplicated-port-lhs (b* ((?scoped-lhs (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr))) (sv::svarlist-addr-p (sv::lhs-vars scoped-lhs))))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-of-lhs-fix-port-lhs (equal (vl-instarray-nonreplicated-port-lhs (sv::lhs-fix port-lhs) instname instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-lhs-equiv-congruence-on-port-lhs (implies (sv::lhs-equiv port-lhs port-lhs-equiv) (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs-equiv instname instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-of-str-fix-instname (equal (vl-instarray-nonreplicated-port-lhs port-lhs (str-fix instname) instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-streqv-congruence-on-instname (implies (streqv instname instname-equiv) (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname-equiv instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-of-ifix-instindex (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname (ifix instindex) instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-int-equiv-congruence-on-instindex (implies (acl2::int-equiv instindex instindex-equiv) (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex-equiv instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-of-nfix-instoffset (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex (nfix instoffset) inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-nat-equiv-congruence-on-instoffset (implies (acl2::nat-equiv instoffset instoffset-equiv) (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset-equiv inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-of-ifix-inst-incr (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset (ifix inst-incr)) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-int-equiv-congruence-on-inst-incr (implies (acl2::int-equiv inst-incr inst-incr-equiv) (equal (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs port-lhs instname instindex instoffset inst-incr-equiv))) :rule-classes :congruence)