Function:
(defun aignet-unmark-higher-levels (n limit aignet-levels mark) (declare (xargs :stobjs (aignet-levels mark))) (declare (xargs :guard (and (natp n) (natp limit)))) (declare (xargs :guard (and (<= n (u32-length aignet-levels)) (<= (u32-length aignet-levels) (bits-length mark))))) (let ((__function__ 'aignet-unmark-higher-levels)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (u32-length aignet-levels) (nfix n))) :exec (eql (u32-length aignet-levels) n))) mark) (mark (if (< (lnfix limit) (get-u32 n aignet-levels)) (set-bit n 0 mark) mark))) (aignet-unmark-higher-levels (1+ (lnfix n)) limit aignet-levels mark))))
Theorem:
(defthm len-of-aignet-unmark-higher-levels (b* ((?new-mark (aignet-unmark-higher-levels n limit aignet-levels mark))) (implies (<= (len aignet-levels) (len mark)) (equal (len new-mark) (len mark)))))
Theorem:
(defthm aignet-unmark-higher-levels-of-nfix-n (equal (aignet-unmark-higher-levels (nfix n) limit aignet-levels mark) (aignet-unmark-higher-levels n limit aignet-levels mark)))
Theorem:
(defthm aignet-unmark-higher-levels-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (aignet-unmark-higher-levels n limit aignet-levels mark) (aignet-unmark-higher-levels n-equiv limit aignet-levels mark))) :rule-classes :congruence)
Theorem:
(defthm aignet-unmark-higher-levels-of-nfix-limit (equal (aignet-unmark-higher-levels n (nfix limit) aignet-levels mark) (aignet-unmark-higher-levels n limit aignet-levels mark)))
Theorem:
(defthm aignet-unmark-higher-levels-nat-equiv-congruence-on-limit (implies (nat-equiv limit limit-equiv) (equal (aignet-unmark-higher-levels n limit aignet-levels mark) (aignet-unmark-higher-levels n limit-equiv aignet-levels mark))) :rule-classes :congruence)