(RTL::LNOT_ALT-IS-LNOT
     (16 2 (:REWRITE RTL::BITS-TAIL))
     (14 8 (:REWRITE DEFAULT-+-2))
     (12 4 (:REWRITE RTL::A4))
     (10 8 (:REWRITE DEFAULT-+-1))
     (6 6
        (:TYPE-PRESCRIPTION RTL::BITS-NONNEGATIVE-INTEGERP-TYPE))
     (6 6 (:REWRITE DEFAULT-<-2))
     (6 6 (:REWRITE DEFAULT-<-1))
     (6 2
        (:REWRITE RTL::BITS-WITH-INDICES-IN-THE-WRONG-ORDER))
     (6 2 (:REWRITE RTL::BITS-NEG))
     (4 4
        (:TYPE-PRESCRIPTION RTL::EXPT-2-POSITIVE-INTEGER-TYPE))
     (4 4 (:TYPE-PRESCRIPTION RTL::BVECP))
     (4 2 (:REWRITE UNICITY-OF-0))
     (4 2 (:REWRITE DEFAULT-*-2))
     (2 2 (:REWRITE FOLD-CONSTS-IN-+))
     (2 2 (:REWRITE DEFAULT-*-1))
     (2 2 (:DEFINITION FIX)))
(RTL::EQUAL-LNOT_ALT-0 (1 1 (:REWRITE RTL::BVECP-MONOTONE)))
(RTL::EQUAL-LNOT_ALT-1 (1 1 (:REWRITE RTL::BVECP-MONOTONE)))
(RTL::BITS_ALT-IF)
(RTL::BITN_ALT-IF)
(RTL::BITS_ALT-IF1 (8 4
                      (:REWRITE RTL::BITS-WITH-INDICES-IN-THE-WRONG-ORDER))
                   (6 4 (:REWRITE RTL::BITS-NEG))
                   (3 3 (:REWRITE RTL::IF1-NON-0))
                   (3 2 (:REWRITE DEFAULT-<-2))
                   (3 2 (:REWRITE DEFAULT-<-1))
                   (2 2
                      (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP)))
(RTL::BITN_ALT-IF1 (10 4 (:REWRITE RTL::BVECP-BITN-0))
                   (7 4 (:REWRITE RTL::BITN-NEG))
                   (3 3 (:REWRITE RTL::IF1-NON-0))
                   (2 2 (:REWRITE RTL::BVECP-MONOTONE))
                   (2 1 (:REWRITE DEFAULT-<-1))
                   (1 1
                      (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
                   (1 1 (:REWRITE DEFAULT-<-2)))
(RTL::LOG=-0-REWRITE_ALT (1 1 (:REWRITE RTL::BVECP-MONOTONE)))
(RTL::LOG<>-IS-LNOT_ALT-LOG=)
(RTL::CAT_ALT-COMBINE-CONSTANTS (4 4 (:REWRITE DEFAULT-+-2))
                                (4 4 (:REWRITE DEFAULT-+-1))
                                (3 3 (:REWRITE DEFAULT-<-2))
                                (3 3 (:REWRITE DEFAULT-<-1))
                                (2 2
                                   (:REWRITE RTL::CAT-COMBINE-CONSTANTS)))
