Function:
(defun bitarr-remove-marked (n max mark mark2) (declare (xargs :stobjs (mark mark2))) (declare (xargs :guard (and (natp n) (natp max)))) (declare (xargs :guard (and (<= n max) (<= max (bits-length mark)) (<= max (bits-length mark2))))) (let ((__function__ 'bitarr-remove-marked)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (nfix max) (nfix n))) :exec (eql n max))) mark) (mark (if (eql 1 (get-bit n mark2)) (set-bit n 0 mark) mark))) (bitarr-remove-marked (1+ (lnfix n)) max mark mark2))))
Theorem:
(defthm len-of-bitarr-remove-marked (b* ((?new-mark (bitarr-remove-marked n max mark mark2))) (implies (<= (nfix max) (len mark)) (equal (len new-mark) (len mark)))))
Theorem:
(defthm nth-of-bitarr-remove-marked (b* ((?new-mark (bitarr-remove-marked n max mark mark2))) (bit-equiv (nth k new-mark) (if (and (<= (nfix n) (nfix k)) (< (nfix k) (nfix max))) (b-and (nth k mark) (b-not (nth k mark2))) (nth k mark)))))
Theorem:
(defthm bitarr-remove-marked-of-nfix-n (equal (bitarr-remove-marked (nfix n) max mark mark2) (bitarr-remove-marked n max mark mark2)))
Theorem:
(defthm bitarr-remove-marked-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (bitarr-remove-marked n max mark mark2) (bitarr-remove-marked n-equiv max mark mark2))) :rule-classes :congruence)
Theorem:
(defthm bitarr-remove-marked-of-nfix-max (equal (bitarr-remove-marked n (nfix max) mark mark2) (bitarr-remove-marked n max mark mark2)))
Theorem:
(defthm bitarr-remove-marked-nat-equiv-congruence-on-max (implies (nat-equiv max max-equiv) (equal (bitarr-remove-marked n max mark mark2) (bitarr-remove-marked n max-equiv mark mark2))) :rule-classes :congruence)