(apply-comb-transform! aignet transform output-ranges state) → (mv new-aignet new-output-ranges new-state)
Function:
(defun apply-comb-transform! (aignet transform output-ranges state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (aignet-output-range-map-p output-ranges))) (declare (xargs :guard t)) (let ((__function__ 'apply-comb-transform!)) (declare (ignorable __function__)) (mbe :logic (non-exec (apply-comb-transform aignet nil transform output-ranges state)) :exec (b* (((local-stobjs aignet2) (mv aignet aignet2 output-ranges state)) ((mv aignet2 output-ranges state) (apply-comb-transform 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-comb-transform!.new-output-ranges (b* (((mv ?new-aignet ?new-output-ranges ?new-state) (apply-comb-transform! aignet transform output-ranges state))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)