(vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr) → array-lhs
Function:
(defun vl-instarray-nonreplicated-port-lhs-aux (port-lhs instindex instoffset inst-incr) (declare (xargs :guard (and (sv::lhs-p port-lhs) (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-aux)) (declare (ignorable __function__)) (b* (((when (zp instoffset)) nil) (instindex (lifix instindex)) (lhs1 (sv::lhs-add-namespace instindex port-lhs))) (append-without-guard lhs1 (vl-instarray-nonreplicated-port-lhs-aux port-lhs (+ instindex (lifix inst-incr)) (1- instoffset) inst-incr)))))
Theorem:
(defthm lhs-p-of-vl-instarray-nonreplicated-port-lhs-aux (b* ((array-lhs (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr))) (sv::lhs-p array-lhs)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-instarray-nonreplicated-port-lhs-aux (b* ((?array-lhs (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr))) (sv::svarlist-addr-p (sv::lhs-vars array-lhs))))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-of-lhs-fix-port-lhs (equal (vl-instarray-nonreplicated-port-lhs-aux (sv::lhs-fix port-lhs) instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-lhs-equiv-congruence-on-port-lhs (implies (sv::lhs-equiv port-lhs port-lhs-equiv) (equal (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs-aux port-lhs-equiv instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-of-ifix-instindex (equal (vl-instarray-nonreplicated-port-lhs-aux port-lhs (ifix instindex) instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-int-equiv-congruence-on-instindex (implies (acl2::int-equiv instindex instindex-equiv) (equal (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex-equiv instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-of-nfix-instoffset (equal (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex (nfix instoffset) inst-incr) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-nat-equiv-congruence-on-instoffset (implies (acl2::nat-equiv instoffset instoffset-equiv) (equal (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset-equiv inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-of-ifix-inst-incr (equal (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset (ifix inst-incr)) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-nonreplicated-port-lhs-aux-int-equiv-congruence-on-inst-incr (implies (acl2::int-equiv inst-incr inst-incr-equiv) (equal (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr) (vl-instarray-nonreplicated-port-lhs-aux port-lhs instindex instoffset inst-incr-equiv))) :rule-classes :congruence)