(vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr) → aliases
Function:
(defun vl-instarray-replicated-port-aliases (port-lhs instname conn-lhs instindex instoffset inst-incr) (declare (xargs :guard (and (sv::lhs-p port-lhs) (stringp instname) (sv::lhs-p conn-lhs) (integerp instindex) (natp instoffset) (integerp inst-incr)))) (declare (xargs :guard (and (sv::svarlist-addr-p (sv::lhs-vars port-lhs)) (sv::svarlist-addr-p (sv::lhs-vars conn-lhs))))) (let ((__function__ 'vl-instarray-replicated-port-aliases)) (declare (ignorable __function__)) (b* (((when (zp instoffset)) nil) (instindex (lifix instindex)) (lhs1 (sv::lhs-add-namespace (string-fix instname) (sv::lhs-add-namespace instindex port-lhs)))) (cons (cons (sv::lhs-fix conn-lhs) lhs1) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs (+ instindex (lifix inst-incr)) (1- instoffset) inst-incr)))))
Theorem:
(defthm lhspairs-p-of-vl-instarray-replicated-port-aliases (b* ((aliases (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-instarray-replicated-port-aliases (b* ((?aliases (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr))) (implies (sv::svarlist-addr-p (sv::lhs-vars conn-lhs)) (sv::svarlist-addr-p (sv::lhspairs-vars aliases)))))
Theorem:
(defthm vl-instarray-replicated-port-aliases-of-lhs-fix-port-lhs (equal (vl-instarray-replicated-port-aliases (sv::lhs-fix port-lhs) instname conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-aliases-lhs-equiv-congruence-on-port-lhs (implies (sv::lhs-equiv port-lhs port-lhs-equiv) (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs-equiv instname conn-lhs instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-aliases-of-str-fix-instname (equal (vl-instarray-replicated-port-aliases port-lhs (str-fix instname) conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-aliases-streqv-congruence-on-instname (implies (streqv instname instname-equiv) (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname-equiv conn-lhs instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-aliases-of-lhs-fix-conn-lhs (equal (vl-instarray-replicated-port-aliases port-lhs instname (sv::lhs-fix conn-lhs) instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-aliases-lhs-equiv-congruence-on-conn-lhs (implies (sv::lhs-equiv conn-lhs conn-lhs-equiv) (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs-equiv instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-aliases-of-ifix-instindex (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs (ifix instindex) instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-aliases-int-equiv-congruence-on-instindex (implies (acl2::int-equiv instindex instindex-equiv) (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex-equiv instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-aliases-of-nfix-instoffset (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex (nfix instoffset) inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-aliases-nat-equiv-congruence-on-instoffset (implies (acl2::nat-equiv instoffset instoffset-equiv) (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset-equiv inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-aliases-of-ifix-inst-incr (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset (ifix inst-incr)) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-aliases-int-equiv-congruence-on-inst-incr (implies (acl2::int-equiv inst-incr inst-incr-equiv) (equal (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr) (vl-instarray-replicated-port-aliases port-lhs instname conn-lhs instindex instoffset inst-incr-equiv))) :rule-classes :congruence)