(vcd-wirelist-add-to-wiremap x idx vcd-wiremap) → vcd-wiremap1
Function:
(defun vcd-wirelist-add-to-wiremap (x idx vcd-wiremap) (declare (xargs :stobjs (vcd-wiremap))) (declare (xargs :guard (and (vcd-wirelist-p x) (natp idx)))) (declare (xargs :guard (<= (+ (len x) idx) (vcdwires-length vcd-wiremap)))) (let ((__function__ 'vcd-wirelist-add-to-wiremap)) (declare (ignorable __function__)) (b* (((when (atom x)) vcd-wiremap) (vcd-wiremap (set-vcdwire idx (car x) vcd-wiremap))) (vcd-wirelist-add-to-wiremap (cdr x) (1+ (lnfix idx)) vcd-wiremap))))
Theorem:
(defthm len-of-vcd-wirelist-add-to-wiremap-linear (<= (len vcd-wiremap) (len (vcd-wirelist-add-to-wiremap x idx vcd-wiremap))) :rule-classes :linear)
Theorem:
(defthm vcd-wirelist-add-to-wiremap-of-vcd-wirelist-fix-x (equal (vcd-wirelist-add-to-wiremap (vcd-wirelist-fix x) idx vcd-wiremap) (vcd-wirelist-add-to-wiremap x idx vcd-wiremap)))
Theorem:
(defthm vcd-wirelist-add-to-wiremap-vcd-wirelist-equiv-congruence-on-x (implies (vcd-wirelist-equiv x x-equiv) (equal (vcd-wirelist-add-to-wiremap x idx vcd-wiremap) (vcd-wirelist-add-to-wiremap x-equiv idx vcd-wiremap))) :rule-classes :congruence)
Theorem:
(defthm vcd-wirelist-add-to-wiremap-of-nfix-idx (equal (vcd-wirelist-add-to-wiremap x (nfix idx) vcd-wiremap) (vcd-wirelist-add-to-wiremap x idx vcd-wiremap)))
Theorem:
(defthm vcd-wirelist-add-to-wiremap-nat-equiv-congruence-on-idx (implies (nat-equiv idx idx-equiv) (equal (vcd-wirelist-add-to-wiremap x idx vcd-wiremap) (vcd-wirelist-add-to-wiremap x idx-equiv vcd-wiremap))) :rule-classes :congruence)