(aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) → (mv new-mark new-copy new-mark2 new-copy2 new-strash new-aignet2)
Function:
(defun aignet-parametrize-output-ranges (start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (declare (xargs :stobjs (aignet mark copy mark2 copy2 strash aignet2))) (declare (xargs :guard (and (natp start) (aignet-output-range-map-p output-ranges) (parametrize-output-type-map-p outtypes) (gatesimp-p gatesimp)))) (declare (xargs :guard (and (<= (num-fanins aignet) (bits-length mark)) (<= (num-fanins aignet) (bits-length mark2)) (<= (num-fanins aignet) (lits-length copy)) (<= (num-fanins aignet) (lits-length copy2)) (aignet-copies-in-bounds copy aignet2) (aignet-copies-in-bounds copy2 aignet2)))) (let ((__function__ 'aignet-parametrize-output-ranges)) (declare (ignorable __function__)) (b* (((when (<= (num-outs aignet) (lnfix start))) (b* ((aignet2 (mbe :logic (non-exec (node-list-fix aignet2)) :exec aignet2))) (mv mark copy mark2 copy2 strash aignet2))) ((when (atom output-ranges)) (b* (((mv mark2 copy2 strash aignet2) (aignet-copy-dfs-output-range start (- (num-outs aignet) (lnfix start)) aignet mark2 copy2 strash gatesimp aignet2))) (mv mark copy mark2 copy2 strash aignet2))) ((unless (mbt (consp (car output-ranges)))) (aignet-parametrize-output-ranges start (cdr output-ranges) outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2)) (name (mbe :logic (acl2::symbol-fix (caar output-ranges)) :exec (caar output-ranges))) (count (min (lnfix (cdar output-ranges)) (- (num-outs aignet) (lnfix start)))) (type (or (cdr (hons-assoc-equal name (parametrize-output-type-map-fix outtypes))) (parametrize-output-type-param))) ((mv mark copy mark2 copy2 strash aignet2) (if (parametrize-output-type-case type :param) (b* (((mv mark2 copy2 strash aignet2) (aignet-copy-dfs-output-range start count aignet mark2 copy2 strash gatesimp aignet2))) (mv mark copy mark2 copy2 strash aignet2)) (b* (((mv mark copy strash aignet2) (aignet-copy-dfs-output-range start count aignet mark copy strash gatesimp aignet2))) (mv mark copy mark2 copy2 strash aignet2))))) (aignet-parametrize-output-ranges (+ (lnfix start) count) (cdr output-ranges) outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2))))
Theorem:
(defthm aignet-extension-p-of-aignet-parametrize-output-ranges (b* (((mv ?new-mark ?new-copy ?new-mark2 ?new-copy2 ?new-strash ?new-aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm stype-count-of-aignet-parametrize-output-ranges (b* (((mv ?new-mark ?new-copy ?new-mark2 ?new-copy2 ?new-strash ?new-aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2))) (implies (and (not (equal (stype-fix stype) (and-stype))) (not (equal (stype-fix stype) (xor-stype)))) (equal (stype-count stype new-aignet2) (case (stype-fix stype) (:po (+ (nfix (- (stype-count :po aignet) (nfix start))) (stype-count stype aignet2))) (t (stype-count stype aignet2)))))))
Theorem:
(defthm output-eval-of-aignet-parametrize-output-ranges (b* (((mv ?new-mark ?new-copy ?new-mark2 ?new-copy2 ?new-strash ?new-aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2))) (implies (and (dfs-copy-onto-invar aignet mark copy aignet2) (dfs-copy-onto-invar aignet mark2 copy2 aignet2) (aignet-copies-in-bounds copy aignet2) (aignet-copies-in-bounds copy2 aignet2) (bits-equiv (input-copy-values 0 invals regvals aignet copy aignet2) (input-copy-values 0 invals regvals aignet copy2 aignet2)) (bits-equiv (reg-copy-values 0 invals regvals aignet copy aignet2) (reg-copy-values 0 invals regvals aignet copy2 aignet2))) (equal (output-eval n invals regvals new-aignet2) (if (and (<= (num-outs aignet2) (nfix n)) (< (nfix n) (+ (num-outs aignet2) (nfix (- (stype-count :po aignet) (nfix start)))))) (output-eval (+ (nfix start) (- (nfix n) (num-outs aignet2))) (input-copy-values 0 invals regvals aignet copy aignet2) (reg-copy-values 0 invals regvals aignet copy aignet2) aignet) (output-eval n invals regvals aignet2))))))
Theorem:
(defthm aignet-parametrize-output-ranges-of-nfix-start (equal (aignet-parametrize-output-ranges (nfix start) output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-output-ranges-nat-equiv-congruence-on-start (implies (nat-equiv start start-equiv) (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start-equiv output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-output-ranges-of-aignet-output-range-map-fix-output-ranges (equal (aignet-parametrize-output-ranges start (aignet-output-range-map-fix output-ranges) outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-output-ranges-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges-equiv outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-output-ranges-of-parametrize-output-type-map-fix-outtypes (equal (aignet-parametrize-output-ranges start output-ranges (parametrize-output-type-map-fix outtypes) aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-output-ranges-parametrize-output-type-map-equiv-congruence-on-outtypes (implies (parametrize-output-type-map-equiv outtypes outtypes-equiv) (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes-equiv aignet mark copy mark2 copy2 strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-output-ranges-of-node-list-fix-aignet (equal (aignet-parametrize-output-ranges start output-ranges outtypes (node-list-fix aignet) mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-output-ranges-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet-equiv mark copy mark2 copy2 strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-output-ranges-of-gatesimp-fix-gatesimp (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash (gatesimp-fix gatesimp) aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-output-ranges-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp-equiv aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-output-ranges-of-node-list-fix-aignet2 (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp (node-list-fix aignet2)) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-output-ranges-node-list-equiv-congruence-on-aignet2 (implies (node-list-equiv aignet2 aignet2-equiv) (equal (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2) (aignet-parametrize-output-ranges start output-ranges outtypes aignet mark copy mark2 copy2 strash gatesimp aignet2-equiv))) :rule-classes :congruence)