		Search-engine friendly clone of the ACL2 documentation.

Apply-m-assumption-n-output-transform

Apply-m-assumption-n-output-transform!

Signature
(apply-m-assumption-n-output-transform! m n aignet transform state) → (mv new-aignet new-state)
Arguments: m — Guard (natp m).; n — Guard (natp n).

Definitions and Theorems

Function: apply-m-assumption-n-output-transform!

(defun
    apply-m-assumption-n-output-transform!
    (m n aignet transform state)
    (declare (xargs :stobjs (aignet state)))
    (declare (xargs :guard (and (natp m) (natp n))))
    (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 state))
              :exec (b* (((local-stobjs aignet2)
                          (mv aignet aignet2 state))
                         ((mv aignet2 state)
                          (apply-m-assumption-n-output-transform
                               m n aignet aignet2 transform state))
                         ((mv aignet aignet2)
                          (swap-stobjs aignet aignet2)))
                        (mv aignet aignet2 state)))))