(vl-oddinfolist-details n x &key (ps 'ps)) → ps
Function:
(defun vl-oddinfolist-details-fn (n x ps) (declare (xargs :stobjs (ps))) (declare (xargs :guard (and (natp n) (vl-oddinfolist-p x)))) (let ((__function__ 'vl-oddinfolist-details)) (declare (ignorable __function__)) (b* ((n (lnfix n)) (x (vl-oddinfolist-fix x)) ((when (atom x)) ps)) (vl-ps-seq (vl-oddinfo-details n (car x)) (vl-oddinfolist-details (+ 1 n) (cdr x))))))
Theorem:
(defthm vl-oddinfolist-details-fn-of-nfix-n (equal (vl-oddinfolist-details-fn (nfix n) x ps) (vl-oddinfolist-details-fn n x ps)))
Theorem:
(defthm vl-oddinfolist-details-fn-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-oddinfolist-details-fn n x ps) (vl-oddinfolist-details-fn n-equiv x ps))) :rule-classes :congruence)
Theorem:
(defthm vl-oddinfolist-details-fn-of-vl-oddinfolist-fix-x (equal (vl-oddinfolist-details-fn n (vl-oddinfolist-fix x) ps) (vl-oddinfolist-details-fn n x ps)))
Theorem:
(defthm vl-oddinfolist-details-fn-vl-oddinfolist-equiv-congruence-on-x (implies (vl-oddinfolist-equiv x x-equiv) (equal (vl-oddinfolist-details-fn n x ps) (vl-oddinfolist-details-fn n x-equiv ps))) :rule-classes :congruence)