(apply-m-assumption-n-output-transform! m n aignet transform output-ranges state) → (mv new-aignet new-output-ranges new-state)
Function:
(defun apply-m-assumption-n-output-transform! (m n aignet transform output-ranges state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (and (natp m) (natp n) (aignet-output-range-map-p output-ranges)))) (declare (xargs :guard (<= (+ m n) (num-outs aignet)))) (let ((__function__ 'apply-m-assumption-n-output-transform!)) (declare (ignorable __function__)) (mbe :logic (non-exec (apply-m-assumption-n-output-transform m n aignet nil transform output-ranges state)) :exec (b* (((local-stobjs aignet2) (mv aignet aignet2 output-ranges state)) ((mv aignet2 output-ranges state) (apply-m-assumption-n-output-transform m n aignet aignet2 transform output-ranges state)) ((mv aignet aignet2) (swap-stobjs aignet aignet2))) (mv aignet aignet2 output-ranges state)))))
Theorem:
(defthm aignet-output-range-map-p-of-apply-m-assumption-n-output-transform!.new-output-ranges (b* (((mv ?new-aignet ?new-output-ranges ?new-state) (apply-m-assumption-n-output-transform! m n aignet transform output-ranges state))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)