Function:
(defun aignet-copy-outs-range (start count aignet copy aignet2) (declare (xargs :stobjs (aignet copy aignet2))) (declare (xargs :guard (and (natp start) (natp count)))) (declare (xargs :guard (and (<= (num-fanins aignet) (lits-length copy)) (<= (+ start count) (num-outs aignet)) (ec-call (aignet-po-copies-in-bounds copy aignet aignet2))))) (let ((__function__ 'aignet-copy-outs-range)) (declare (ignorable __function__)) (b* (((when (zp count)) aignet2) (aignet2 (aignet-add-out (lit-copy (outnum->fanin start aignet) copy) aignet2))) (aignet-copy-outs-range (1+ (lnfix start)) (1- count) aignet copy aignet2))))
Theorem:
(defthm aignet-extension-p-of-aignet-copy-outs-range (b* ((?new-aignet2 (aignet-copy-outs-range start count aignet copy aignet2))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm fanin-count-of-aignet-copy-outs-range (b* ((?new-aignet2 (aignet-copy-outs-range start count aignet copy aignet2))) (equal (fanin-count new-aignet2) (fanin-count aignet2))))
Theorem:
(defthm stype-count-of-aignet-copy-outs-range (b* ((?new-aignet2 (aignet-copy-outs-range start count aignet copy aignet2))) (equal (stype-count stype new-aignet2) (if (eq (stype-fix stype) :po) (+ (nfix count) (stype-count :po aignet2)) (stype-count stype aignet2)))))
Theorem:
(defthm outnum->fanin-of-aignet-copy-outs-range (b* ((?new-aignet2 (aignet-copy-outs-range start count aignet copy aignet2))) (implies (< (nfix n) (+ (nfix count) (stype-count :po aignet2))) (equal (fanin 0 (lookup-stype n (po-stype) new-aignet2)) (cond ((< (nfix n) (stype-count :po aignet2)) (fanin 0 (lookup-stype n (po-stype) aignet2))) (t (b* ((outnum (+ (nfix start) (- (nfix n) (stype-count :po aignet2))))) (aignet-lit-fix (lit-copy (fanin 0 (lookup-stype outnum (po-stype) aignet)) copy) aignet2))))))))
Theorem:
(defthm aignet-copy-outs-range-of-nfix-start (equal (aignet-copy-outs-range (nfix start) count aignet copy aignet2) (aignet-copy-outs-range start count aignet copy aignet2)))
Theorem:
(defthm aignet-copy-outs-range-nat-equiv-congruence-on-start (implies (nat-equiv start start-equiv) (equal (aignet-copy-outs-range start count aignet copy aignet2) (aignet-copy-outs-range start-equiv count aignet copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-copy-outs-range-of-nfix-count (equal (aignet-copy-outs-range start (nfix count) aignet copy aignet2) (aignet-copy-outs-range start count aignet copy aignet2)))
Theorem:
(defthm aignet-copy-outs-range-nat-equiv-congruence-on-count (implies (nat-equiv count count-equiv) (equal (aignet-copy-outs-range start count aignet copy aignet2) (aignet-copy-outs-range start count-equiv aignet copy aignet2))) :rule-classes :congruence)