(IN-PACKAGE "*")

(INCLUDE-BOOK "exec")

(INCLUDE-BOOK "declarations")

(DEFUN LONGOP_FLOPPED
       NIL (+::LONGOP_FLOPPED (LONGOP)))

(DEFUN S01 NIL (+::S01 (IN)))

(DEFUN S01_MUXED
       NIL (+::S01_MUXED (LONGOP) (S01)))

(DEFUN S01_MUXED_FLOPPED
       NIL (+::S01_MUXED_FLOPPED (S01_MUXED)))

(DEFUN S23 NIL (+::S23 (IN)))

(DEFUN S23_FLOPPED NIL (+::S23_FLOPPED (S23)))

(DEFUN S0123 NIL
       (+::S0123 (S01_MUXED_FLOPPED)
                 (S23_FLOPPED)))

(DEFUN OUT NIL
       (+::OUT (LONGOP_FLOPPED)
               (S01_MUXED_FLOPPED)
               (S0123)))

(IN-THEORY (DISABLE (:EXECUTABLE-COUNTERPART LONGOP_FLOPPED)
                    (:EXECUTABLE-COUNTERPART S01)
                    (:EXECUTABLE-COUNTERPART S01_MUXED)
                    (:EXECUTABLE-COUNTERPART S01_MUXED_FLOPPED)
                    (:EXECUTABLE-COUNTERPART S23)
                    (:EXECUTABLE-COUNTERPART S23_FLOPPED)
                    (:EXECUTABLE-COUNTERPART S0123)
                    (:EXECUTABLE-COUNTERPART OUT)))

(IN-THEORY (DISABLE LONGOP_FLOPPED
                    S01 S01_MUXED S01_MUXED_FLOPPED
                    S23 S23_FLOPPED S0123 OUT))