Function:
(defun aignet-mark-output-node-range (start count aignet mark) (declare (xargs :stobjs (aignet mark))) (declare (xargs :guard (and (natp start) (natp count)))) (declare (xargs :guard (and (<= (+ start count) (num-outs aignet)) (<= (num-fanins aignet) (bits-length mark))))) (let ((__function__ 'aignet-mark-output-node-range)) (declare (ignorable __function__)) (b* (((when (zp count)) mark) (mark (set-bit (lit->var (outnum->fanin start aignet)) 1 mark))) (aignet-mark-output-node-range (+ (lnfix start) 1) (1- count) aignet mark))))
Theorem:
(defthm len-of-aignet-mark-output-node-range (b* ((?new-mark (aignet-mark-output-node-range start count aignet mark))) (implies (<= (num-fanins aignet) (len mark)) (equal (len new-mark) (len mark)))))
Theorem:
(defthm aignet-mark-output-node-range-of-nfix-start (equal (aignet-mark-output-node-range (nfix start) count aignet mark) (aignet-mark-output-node-range start count aignet mark)))
Theorem:
(defthm aignet-mark-output-node-range-nat-equiv-congruence-on-start (implies (nat-equiv start start-equiv) (equal (aignet-mark-output-node-range start count aignet mark) (aignet-mark-output-node-range start-equiv count aignet mark))) :rule-classes :congruence)
Theorem:
(defthm aignet-mark-output-node-range-of-nfix-count (equal (aignet-mark-output-node-range start (nfix count) aignet mark) (aignet-mark-output-node-range start count aignet mark)))
Theorem:
(defthm aignet-mark-output-node-range-nat-equiv-congruence-on-count (implies (nat-equiv count count-equiv) (equal (aignet-mark-output-node-range start count aignet mark) (aignet-mark-output-node-range start count-equiv aignet mark))) :rule-classes :congruence)