(IN-PACKAGE "+")

(DEFUN LONGOP_FLOPPED (LONGOP) LONGOP)

(DEFUN S01 (IN)
       (LOGAND (BITN IN 0) (BITN IN 1)))

(DEFUN S01_MUXED (LONGOP S01)
       (IF (EQL LONGOP 0) (COMP1 S01 1) S01))

(DEFUN S01_MUXED_FLOPPED (S01_MUXED)
       S01_MUXED)

(DEFUN S23 (IN)
       (LOGAND (BITN IN 2) (BITN IN 3)))

(DEFUN S23_FLOPPED (S23) S23)

(DEFUN S0123 (S01_MUXED_FLOPPED S23_FLOPPED)
       (LOGAND S01_MUXED_FLOPPED S23_FLOPPED))

(DEFUN OUT
       (LONGOP_FLOPPED S01_MUXED_FLOPPED S0123)
       (IF (EQL LONGOP_FLOPPED 0)
           S01_MUXED_FLOPPED S0123))

(SET-IRRELEVANT-FORMALS-OK T)

(SET-IGNORE-OK T)

(DEFUN ACL2::TOY (VAR LONGOP IN)
       (LET* ((LONGOP_FLOPPED (LONGOP_FLOPPED LONGOP))
              (S01 (S01 IN))
              (S01_MUXED (S01_MUXED LONGOP S01))
              (S01_MUXED_FLOPPED (S01_MUXED_FLOPPED S01_MUXED))
              (S23 (S23 IN))
              (S23_FLOPPED (S23_FLOPPED S23))
              (S0123 (S0123 S01_MUXED_FLOPPED S23_FLOPPED))
              (OUT (OUT LONGOP_FLOPPED
                        S01_MUXED_FLOPPED S0123)))
             (CASE VAR (ACL2::OUT OUT)
                   (T (STRING-APPEND (SYMBOL-NAME VAR)
                                     " is not a valid output")))))