(ADE::QUEUE10$DATA-INS-LEN
 (1 1 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$INS-LEN)
(ADE::QUEUE10*
 (28 28 (:TYPE-PRESCRIPTION POSP))
 )
(ADE::QUEUE10*$DESTRUCTURE
 (180 18 (:DEFINITION BINARY-APPEND))
 (153 36 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (105 105 (:TYPE-PRESCRIPTION POSP))
 (28 28 (:REWRITE DEFAULT-CDR))
 (23 23 (:REWRITE DEFAULT-CAR))
 )
(ADE::NOT-PRIMP-QUEUE10)
(ADE::QUEUE10$NETLIST)
(ADE::QUEUE10&)
(ADE::CHECK-QUEUE10$NETLIST-64)
(ADE::QUEUE10$ST-FORMAT)
(ADE::QUEUE10$ST-FORMAT=>CONSTRAINT
 (5 1 (:DEFINITION LEN))
 (4 4 (:REWRITE NTH-WHEN-PREFIXP))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::QUEUE10$VALID-ST)
(ADE::QUEUE10$VALID-ST=>CONSTRAINT
 (6 6 (:REWRITE NTH-WHEN-PREFIXP))
 (5 1 (:DEFINITION LEN))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::QUEUE10$VALID-ST=>ST-FORMAT
 (11 11 (:REWRITE NTH-WHEN-PREFIXP))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::QUEUE10$DATA-IN
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (1 1 (:REWRITE NATP-RW))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::LEN-QUEUE10$DATA-IN)
(ADE::QUEUE10$Q4-INPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::QUEUE10$Q5-INPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::QUEUE10$IN-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE4$IN-ACT))
 (5 5 (:TYPE-PRESCRIPTION ADE::QUEUE4$INPUT-FORMAT))
 )
(ADE::QUEUE10$IN-ACT-INACTIVE
 (54 2 (:REWRITE TAKE-OF-TOO-MANY))
 (43 1 (:DEFINITION TAKE))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (23 3 (:DEFINITION LEN))
 (17 17 (:TYPE-PRESCRIPTION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (12 6 (:REWRITE DEFAULT-CDR))
 (12 1 (:REWRITE ADE::LEN-NTHCDR))
 (10 7 (:REWRITE DEFAULT-+-2))
 (10 1 (:DEFINITION NTHCDR))
 (9 3 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE NTH-WHEN-PREFIXP))
 (6 4 (:REWRITE DEFAULT-<-2))
 (6 1 (:REWRITE COMMUTATIVITY-OF-+))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION ADE::QUEUE10$DATA-IN))
 (5 4 (:REWRITE DEFAULT-<-1))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 1 (:REWRITE ADE::NFIX-OF-NAT))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$OUT-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE5$OUT-ACT))
 (5 5 (:TYPE-PRESCRIPTION ADE::QUEUE5$INPUT-FORMAT))
 )
(ADE::QUEUE10$OUT-ACT-INACTIVE
 (54 2 (:REWRITE TAKE-OF-TOO-MANY))
 (43 1 (:DEFINITION TAKE))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (23 3 (:DEFINITION LEN))
 (20 2 (:DEFINITION NTHCDR))
 (17 17 (:TYPE-PRESCRIPTION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 12 (:REWRITE DEFAULT-+-2))
 (15 9 (:REWRITE DEFAULT-CDR))
 (15 6 (:REWRITE DEFAULT-CAR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 2 (:REWRITE COMMUTATIVITY-OF-+))
 (12 1 (:REWRITE ADE::LEN-NTHCDR))
 (12 1 (:DEFINITION BINARY-APPEND))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 4 (:REWRITE DEFAULT-<-2))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 4 (:REWRITE DEFAULT-<-1))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$DATA-OUT)
(ADE::LEN-QUEUE10$DATA-OUT-1
 (5 5 (:REWRITE NTH-WHEN-PREFIXP))
 (5 1 (:DEFINITION LEN))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE ADE::LEN-QUEUE5$DATA-OUT-2))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::LEN-QUEUE10$DATA-OUT-2
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (5 1 (:DEFINITION LEN))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::BVP-QUEUE10$DATA-OUT
 (14 14 (:REWRITE NTH-WHEN-PREFIXP))
 (5 1 (:DEFINITION LEN))
 (4 2 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (4 2 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::QUEUE10$OUTPUTS)
(ADE::QUEUE10$VALUE
 (574 40 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (322 49 (:DEFINITION BINARY-APPEND))
 (313 160 (:REWRITE DEFAULT-+-2))
 (192 12 (:REWRITE ADE::DISJOINT-ATOM))
 (169 160 (:REWRITE DEFAULT-+-1))
 (159 98 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (123 12 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (91 19 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (90 12 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (90 12 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (90 6 (:DEFINITION ATOM))
 (72 6 (:REWRITE LEN-OF-APPEND))
 (54 54 (:REWRITE NTH-WHEN-PREFIXP))
 (50 50 (:TYPE-PRESCRIPTION PAIRLIS$))
 (39 13 (:REWRITE ADE::CAR-V-THREEFIX))
 (36 12 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (35 5 (:REWRITE ADE::QUEUE4$OUT-ACT-INACTIVE))
 (33 5 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (31 20 (:REWRITE TAKE-WHEN-ATOM))
 (30 22 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (30 22 (:REWRITE ADE::F-BUF-OF-3VP))
 (29 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (28 14 (:REWRITE DEFAULT-<-2))
 (28 7 (:REWRITE COMMUTATIVITY-OF-+))
 (26 13 (:DEFINITION ADE::3V-FIX))
 (24 3 (:REWRITE ADE::QUEUE5$IN-ACT-INACTIVE))
 (21 21 (:TYPE-PRESCRIPTION ADE::3VP))
 (21 5 (:REWRITE ADE::QUEUE4$IN-ACT-INACTIVE))
 (19 13 (:REWRITE ADE::V-THREEFIX-BVP))
 (18 18 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 16 (:LINEAR LEN-WHEN-PREFIXP))
 (15 14 (:REWRITE DEFAULT-<-1))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 2 (:REWRITE EQUAL-CONSTANT-+))
 (11 11 (:DEFINITION STRIP-CARS))
 (10 4 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (10 4 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 8 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (8 2 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (8 2 (:DEFINITION TRUE-LISTP))
 (8 1 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (7 7 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (7 7 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (5 1 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 1 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (2 2 (:REWRITE ADE::LEN-QUEUE5$DATA-OUT-2))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 )
(ADE::QUEUE10$STEP
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE5$IN-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE4$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE5$INPUT-FORMAT))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE4$INPUT-FORMAT))
 )
(ADE::QUEUE10$STATE
 (619 99 (:DEFINITION BINARY-APPEND))
 (541 277 (:REWRITE DEFAULT-+-2))
 (320 20 (:REWRITE ADE::DISJOINT-ATOM))
 (292 277 (:REWRITE DEFAULT-+-1))
 (277 198 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (211 15 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (205 20 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (175 47 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (150 20 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (150 20 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (150 10 (:DEFINITION ATOM))
 (144 12 (:REWRITE LEN-OF-APPEND))
 (126 26 (:DEFINITION ALISTP))
 (90 30 (:REWRITE ADE::CAR-V-THREEFIX))
 (86 86 (:TYPE-PRESCRIPTION PAIRLIS$))
 (86 6 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (72 24 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (70 70 (:TYPE-PRESCRIPTION ALISTP))
 (70 70 (:REWRITE NTH-WHEN-PREFIXP))
 (68 51 (:REWRITE TAKE-WHEN-ATOM))
 (67 53 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (67 53 (:REWRITE ADE::F-BUF-OF-3VP))
 (65 15 (:REWRITE ADE::QUEUE4$OUT-ACT-INACTIVE))
 (60 30 (:DEFINITION ADE::3V-FIX))
 (57 11 (:REWRITE ADE::QUEUE5$IN-ACT-INACTIVE))
 (52 13 (:REWRITE COMMUTATIVITY-OF-+))
 (44 44 (:TYPE-PRESCRIPTION ADE::3VP))
 (44 22 (:REWRITE DEFAULT-<-2))
 (39 29 (:REWRITE ADE::V-THREEFIX-BVP))
 (35 7 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (33 33 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (30 30 (:DEFINITION STRIP-CARS))
 (29 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (26 26 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (24 24 (:LINEAR LEN-WHEN-PREFIXP))
 (23 22 (:REWRITE DEFAULT-<-1))
 (23 7 (:REWRITE ADE::QUEUE4$IN-ACT-INACTIVE))
 (20 20 (:TYPE-PRESCRIPTION ADE::BVP))
 (20 20 (:TYPE-PRESCRIPTION BOOLEANP))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (12 12 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (12 12 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (12 12 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (12 12 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (12 12 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 2 (:REWRITE EQUAL-CONSTANT-+))
 (10 10 (:TYPE-PRESCRIPTION ADE::FV-IF))
 (9 3 (:REWRITE ADE::BOOLEANP-QUEUE4$OUT-ACT))
 (8 2 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (8 2 (:DEFINITION TRUE-LISTP))
 (5 5 (:REWRITE ADE::LEN-QUEUE4$DATA-OUT-2))
 (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 )
(ADE::QUEUE10$INPUT-FORMAT)
(ADE::QUEUE10$INPUT-FORMAT=>Q4$INPUT-FORMAT
 (109 17 (:DEFINITION LEN))
 (88 6 (:REWRITE ADE::LEN-NTHCDR))
 (86 2 (:DEFINITION TAKE))
 (85 41 (:REWRITE DEFAULT-CDR))
 (72 8 (:REWRITE TAKE-WHEN-ATOM))
 (66 49 (:REWRITE DEFAULT-+-2))
 (64 20 (:REWRITE DEFAULT-CAR))
 (49 49 (:REWRITE DEFAULT-+-1))
 (48 8 (:DEFINITION BINARY-APPEND))
 (40 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (32 32 (:REWRITE NTH-WHEN-PREFIXP))
 (30 3 (:DEFINITION NTHCDR))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (25 19 (:REWRITE DEFAULT-<-2))
 (25 19 (:REWRITE DEFAULT-<-1))
 (24 5 (:REWRITE COMMUTATIVITY-OF-+))
 (20 20 (:LINEAR LEN-WHEN-PREFIXP))
 (18 2 (:REWRITE LEN-OF-APPEND))
 (18 2 (:DEFINITION TRUE-LISTP))
 (12 2 (:REWRITE CONSP-OF-APPEND))
 (10 10 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE CONSP-OF-TAKE))
 (1 1 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$INPUT-FORMAT=>Q5$INPUT-FORMAT
 (108 75 (:REWRITE DEFAULT-+-2))
 (88 6 (:REWRITE ADE::LEN-NTHCDR))
 (86 2 (:DEFINITION TAKE))
 (75 75 (:REWRITE DEFAULT-+-1))
 (72 8 (:REWRITE TAKE-WHEN-ATOM))
 (67 55 (:REWRITE DEFAULT-CDR))
 (50 5 (:DEFINITION NTHCDR))
 (48 6 (:DEFINITION BINARY-APPEND))
 (37 19 (:REWRITE DEFAULT-CAR))
 (36 7 (:REWRITE COMMUTATIVITY-OF-+))
 (34 34 (:REWRITE NTH-WHEN-PREFIXP))
 (30 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (30 3 (:DEFINITION ADE::V-THREEFIX))
 (27 2 (:REWRITE LEN-OF-APPEND))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (25 19 (:REWRITE DEFAULT-<-2))
 (25 19 (:REWRITE DEFAULT-<-1))
 (20 20 (:LINEAR LEN-WHEN-PREFIXP))
 (18 2 (:DEFINITION TRUE-LISTP))
 (16 4 (:DEFINITION STRIP-CARS))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (12 2 (:REWRITE CONSP-OF-APPEND))
 (10 10 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (10 5 (:DEFINITION ADE::3V-FIX))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (5 5 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE CONSP-OF-TAKE))
 (1 1 (:REWRITE NATP-RW))
 )
(ADE::BOOLEANP-QUEUE10$IN-ACT
 (24 24 (:REWRITE NTH-WHEN-PREFIXP))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 3 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE ADE::QUEUE4$IN-ACT-INACTIVE))
 (4 2 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(ADE::BOOLEANP-QUEUE10$OUT-ACT
 (24 24 (:REWRITE NTH-WHEN-PREFIXP))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 3 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (4 2 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(ADE::QUEUE10$ST-FORMAT-PRESERVED
 (42 2 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (27 27 (:REWRITE NTH-WHEN-PREFIXP))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE4$OUT-ACT))
 (12 2 (:REWRITE ADE::BOOLEANP-QUEUE4$OUT-ACT))
 (10 10 (:TYPE-PRESCRIPTION ADE::QUEUE4$INPUT-FORMAT))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE4$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE10$Q4-INPUTS))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::QUEUE10$INPUT-FORMAT=>Q4$INPUT-FORMAT))
 (5 1 (:DEFINITION PAIRLIS$))
 (5 1 (:DEFINITION LEN))
 (4 4 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 2 (:REWRITE ADE::QUEUE4$OUT-ACT-INACTIVE))
 (3 3 (:REWRITE ADE::LEN-QUEUE4$DATA-OUT-2))
 (3 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 1 (:REWRITE ADE::QUEUE5$IN-ACT-INACTIVE))
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(ADE::QUEUE10$VALUE-ALT
 (320 32 (:DEFINITION NTHCDR))
 (192 174 (:REWRITE DEFAULT-+-2))
 (192 32 (:REWRITE COMMUTATIVITY-OF-+))
 (174 174 (:REWRITE DEFAULT-+-1))
 (150 21 (:DEFINITION BINARY-APPEND))
 (144 9 (:REWRITE ADE::LEN-NTHCDR))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (90 42 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (90 18 (:DEFINITION LEN))
 (81 9 (:DEFINITION TRUE-LISTP))
 (80 80 (:REWRITE DEFAULT-CDR))
 (65 65 (:REWRITE NTH-WHEN-PREFIXP))
 (48 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (45 11 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (36 18 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (21 21 (:REWRITE DEFAULT-CAR))
 (18 9 (:REWRITE DEFAULT-<-1))
 (16 16 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (9 9 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(ADE::QUEUE10$STATE-ALT
 (310 31 (:DEFINITION NTHCDR))
 (188 170 (:REWRITE DEFAULT-+-2))
 (186 31 (:REWRITE COMMUTATIVITY-OF-+))
 (170 170 (:REWRITE DEFAULT-+-1))
 (144 20 (:DEFINITION BINARY-APPEND))
 (144 9 (:REWRITE ADE::LEN-NTHCDR))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (90 18 (:DEFINITION LEN))
 (88 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (81 9 (:DEFINITION TRUE-LISTP))
 (78 78 (:REWRITE DEFAULT-CDR))
 (48 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (36 18 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (35 35 (:REWRITE NTH-WHEN-PREFIXP))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (20 20 (:REWRITE DEFAULT-CAR))
 (18 9 (:REWRITE DEFAULT-<-1))
 (16 16 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (9 9 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(ADE::QUEUE10$RUN
 (4 4 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 )
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-QUEUE10$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-QUEUE10$RUN)
(ADE::QUEUE10$RUN-PLUS
 (115 25 (:REWRITE ZP-OPEN))
 (61 61 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (42 14 (:REWRITE <-0-+-NEGATIVE-1))
 (38 15 (:REWRITE DEFAULT-CDR))
 (36 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (33 10 (:REWRITE DEFAULT-CAR))
 (26 22 (:REWRITE DEFAULT-+-2))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-<-1))
 (24 22 (:REWRITE DEFAULT-+-1))
 (16 8 (:REWRITE FOLD-CONSTS-IN-+))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2 2 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$INPUT-FORMAT-N
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE NATP-RW))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-QUEUE10$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-QUEUE10$INPUT-FORMAT-N)
(ADE::QUEUE10$INPUT-FORMAT-PLUS
 (36 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (33 15 (:REWRITE DEFAULT-CDR))
 (33 15 (:REWRITE DEFAULT-CAR))
 (32 27 (:REWRITE DEFAULT-+-2))
 (31 31 (:REWRITE DEFAULT-<-2))
 (31 31 (:REWRITE DEFAULT-<-1))
 (29 27 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (4 4 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$DE-N
 (114 30 (:REWRITE ZP-OPEN))
 (36 36 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (36 12 (:REWRITE <-0-+-NEGATIVE-1))
 (36 2 (:DEFINITION ADE::QUEUE10$RUN))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE ADE::QUEUE10$INPUT-FORMAT-PLUS))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::QUEUE10$EXTRACT)
(ADE::QUEUE10$EXTRACT-NOT-EMPTY
 (44 22 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (43 7 (:DEFINITION LEN))
 (28 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (24 2 (:DEFINITION BINARY-APPEND))
 (23 23 (:REWRITE NTH-WHEN-PREFIXP))
 (21 10 (:REWRITE DEFAULT-+-2))
 (20 20 (:TYPE-PRESCRIPTION ADE::QUEUE5$EXTRACT))
 (13 13 (:REWRITE DEFAULT-CDR))
 (13 10 (:REWRITE DEFAULT-+-1))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 4 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 7 (:TYPE-PRESCRIPTION ADE::QUEUE4$EXTRACT))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (6 2 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (4 2 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (2 2 (:LINEAR ADE::QUEUE4$EXTRACT-NOT-EMPTY))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE EQUAL-CONSTANT-+))
 )
(ADE::QUEUE10$EXTRACTED-STEP
 (24 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$IN-ACT))
 (18 18 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$OUT-ACT))
 )
(ADE::QUEUE10$Q4-OUT-ACT-INACTIVE
 (54 2 (:REWRITE TAKE-OF-TOO-MANY))
 (43 1 (:DEFINITION TAKE))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (23 3 (:DEFINITION LEN))
 (17 17 (:TYPE-PRESCRIPTION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (12 6 (:REWRITE DEFAULT-CDR))
 (12 1 (:REWRITE ADE::LEN-NTHCDR))
 (10 7 (:REWRITE DEFAULT-+-2))
 (10 1 (:DEFINITION NTHCDR))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 2 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 4 (:REWRITE DEFAULT-<-2))
 (6 1 (:REWRITE COMMUTATIVITY-OF-+))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION ADE::QUEUE10$DATA-IN))
 (5 4 (:REWRITE DEFAULT-<-1))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 1 (:REWRITE ADE::NFIX-OF-NAT))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$Q5-IN-ACT-INACTIVE
 (54 2 (:REWRITE TAKE-OF-TOO-MANY))
 (43 1 (:DEFINITION TAKE))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (23 3 (:DEFINITION LEN))
 (20 2 (:DEFINITION NTHCDR))
 (17 17 (:TYPE-PRESCRIPTION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 12 (:REWRITE DEFAULT-+-2))
 (15 9 (:REWRITE DEFAULT-CDR))
 (14 5 (:REWRITE DEFAULT-CAR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 2 (:REWRITE COMMUTATIVITY-OF-+))
 (12 1 (:REWRITE ADE::LEN-NTHCDR))
 (12 1 (:DEFINITION BINARY-APPEND))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 4 (:REWRITE DEFAULT-<-2))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 4 (:REWRITE DEFAULT-<-1))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE NATP-RW))
 )
(ADE::QUEUE10$Q4-DATA-IN-REWRITE
 (43 1 (:DEFINITION TAKE))
 (42 21 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (37 5 (:DEFINITION LEN))
 (36 4 (:REWRITE TAKE-WHEN-ATOM))
 (24 2 (:REWRITE ADE::LEN-NTHCDR))
 (21 21 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (19 16 (:REWRITE DEFAULT-<-2))
 (18 16 (:REWRITE DEFAULT-<-1))
 (18 13 (:REWRITE DEFAULT-+-2))
 (14 8 (:REWRITE DEFAULT-CDR))
 (13 13 (:REWRITE DEFAULT-+-1))
 (12 1 (:REWRITE LEN-OF-APPEND))
 (10 1 (:DEFINITION NTHCDR))
 (9 3 (:REWRITE DEFAULT-CAR))
 (9 2 (:REWRITE COMMUTATIVITY-OF-+))
 (9 1 (:REWRITE ADE::NTHCDR-APPEND))
 (7 1 (:DEFINITION BINARY-APPEND))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (6 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 1 (:REWRITE CONSP-OF-APPEND))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NATP-RW))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:REWRITE LEN-OF-TAKE))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE CONSP-OF-TAKE))
 )
(ADE::QUEUE10$Q5-DATA-IN-REWRITE
 (484 1 (:REWRITE TAKE-WHEN-PREFIXP))
 (275 9 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (255 1 (:REWRITE PREFIXP-OF-APPEND-ARG2))
 (234 7 (:REWRITE TAKE-OF-TOO-MANY))
 (209 38 (:DEFINITION LEN))
 (187 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (120 6 (:REWRITE ADE::LEN-NTHCDR))
 (116 64 (:REWRITE DEFAULT-+-2))
 (93 33 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (73 64 (:REWRITE DEFAULT-+-1))
 (59 50 (:REWRITE DEFAULT-CDR))
 (54 1 (:DEFINITION TAKE))
 (53 4 (:DEFINITION NTHCDR))
 (45 4 (:REWRITE TAKE-WHEN-ATOM))
 (43 43 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (34 7 (:REWRITE COMMUTATIVITY-OF-+))
 (32 2 (:REWRITE LEN-OF-APPEND))
 (23 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (22 11 (:REWRITE DEFAULT-<-2))
 (21 9 (:REWRITE DEFAULT-CAR))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (18 1 (:REWRITE ADE::NTHCDR-APPEND))
 (17 11 (:REWRITE DEFAULT-<-1))
 (17 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 2 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (16 2 (:DEFINITION TRUE-LISTP))
 (14 14 (:LINEAR LEN-WHEN-PREFIXP))
 (14 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (13 1 (:DEFINITION BINARY-APPEND))
 (12 4 (:REWRITE ADE::V-THREEFIX-BVP))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 2 (:REWRITE LEN-OF-LIST-FIX))
 (11 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 10 (:REWRITE NTH-WHEN-PREFIXP))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (8 8 (:REWRITE LEN-OF-TAKE))
 (8 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (8 2 (:DEFINITION STRIP-CARS))
 (8 1 (:REWRITE ZP-OPEN))
 (7 7 (:TYPE-PRESCRIPTION STRIP-CARS))
 (7 7 (:TYPE-PRESCRIPTION NFIX))
 (7 7 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 6 (:REWRITE CONSP-OF-TAKE))
 (6 3 (:DEFINITION ADE::3V-FIX))
 (6 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 1 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:TYPE-PRESCRIPTION ADE::3VP))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (2 2 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 )
(ADE::QUEUE10$EXTRACTED-STEP-CORRECT
 (1356 23 (:DEFINITION TAKE))
 (1153 593 (:REWRITE DEFAULT-+-2))
 (1062 1062 (:REWRITE NTH-WHEN-PREFIXP))
 (715 562 (:REWRITE DEFAULT-CDR))
 (640 593 (:REWRITE DEFAULT-+-1))
 (460 37 (:DEFINITION BINARY-APPEND))
 (432 2 (:REWRITE TAKE-WHEN-PREFIXP))
 (346 14 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (254 2 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (248 173 (:REWRITE DEFAULT-CAR))
 (222 52 (:REWRITE TAKE-WHEN-ATOM))
 (218 14 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (214 115 (:REWRITE DEFAULT-<-2))
 (208 115 (:REWRITE DEFAULT-<-1))
 (192 48 (:DEFINITION STRIP-CARS))
 (140 4 (:REWRITE CONSP-OF-TAKE))
 (128 4 (:REWRITE REPEAT-WHEN-ZP))
 (122 33 (:REWRITE <-0-+-NEGATIVE-1))
 (116 4 (:DEFINITION NTHCDR))
 (105 5 (:REWRITE CONSP-OF-APPEND))
 (102 102 (:LINEAR LEN-WHEN-PREFIXP))
 (98 18 (:LINEAR ADE::QUEUE4$EXTRACT-NOT-EMPTY))
 (74 4 (:REWRITE LEN-WHEN-PREFIXP))
 (62 32 (:REWRITE ADE::QUEUE4$IN-ACT-INACTIVE))
 (51 51 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (51 26 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (46 23 (:REWRITE POSP-NATP))
 (34 17 (:REWRITE ADE::QUEUE5$IN-ACT-INACTIVE))
 (31 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (30 6 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (29 1 (:REWRITE CAR-OF-APPEND))
 (28 28 (:TYPE-PRESCRIPTION PREFIXP))
 (25 14 (:REWRITE ADE::QUEUE4$OUT-ACT-INACTIVE))
 (16 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (14 14 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (14 14 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (14 14 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (14 14 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (14 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (10 10 (:TYPE-PRESCRIPTION STRIP-CARS))
 (10 10 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (10 10 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (8 4 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (8 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (5 1 (:DEFINITION PAIRLIS$))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 2 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (4 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (2 1 (:DEFINITION ADE::3V-FIX))
 (1 1 (:TYPE-PRESCRIPTION ADE::3VP))
 )
(ADE::QUEUE10$VALID-ST-PRESERVED
 (355 355 (:REWRITE NTH-WHEN-PREFIXP))
 (138 70 (:REWRITE DEFAULT-+-2))
 (91 91 (:REWRITE DEFAULT-CDR))
 (76 19 (:DEFINITION STRIP-CARS))
 (70 70 (:REWRITE DEFAULT-+-1))
 (42 42 (:REWRITE DEFAULT-CAR))
 (21 4 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (11 7 (:REWRITE ADE::QUEUE4$OUT-ACT-INACTIVE))
 (6 3 (:REWRITE ADE::QUEUE5$IN-ACT-INACTIVE))
 (5 1 (:DEFINITION PAIRLIS$))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(ADE::QUEUE10$EXTRACT-LEMMA
 (116 4 (:DEFINITION NTHCDR))
 (90 45 (:REWRITE DEFAULT-+-2))
 (62 45 (:REWRITE DEFAULT-+-1))
 (42 29 (:REWRITE DEFAULT-CDR))
 (40 4 (:REWRITE ZP-OPEN))
 (34 17 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (33 33 (:REWRITE NTH-WHEN-PREFIXP))
 (32 32 (:TYPE-PRESCRIPTION ADE::QUEUE4$EXTRACT))
 (30 4 (:DEFINITION BINARY-APPEND))
 (16 4 (:REWRITE <-0-+-NEGATIVE-1))
 (14 14 (:REWRITE DEFAULT-CAR))
 (12 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (12 3 (:DEFINITION STRIP-CARS))
 (8 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 2 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (4 2 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(ADE::QUEUE10$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (3 3 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 )
(ADE::QUEUE10$IN-SEQ-NETLIST
 (3 3 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 )
(ADE::QUEUE10$IN-SEQ-LEMMA
 (313 65 (:REWRITE ZP-OPEN))
 (213 35 (:DEFINITION BINARY-APPEND))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (156 156 (:REWRITE NTH-WHEN-PREFIXP))
 (120 120 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (120 120 (:REWRITE DEFAULT-CAR))
 (120 40 (:REWRITE <-0-+-NEGATIVE-1))
 (91 91 (:REWRITE DEFAULT-CDR))
 (88 72 (:REWRITE DEFAULT-+-2))
 (80 40 (:REWRITE ADE::QUEUE4$IN-ACT-INACTIVE))
 (72 72 (:REWRITE DEFAULT-+-1))
 (72 36 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (48 16 (:REWRITE FOLD-CONSTS-IN-+))
 (28 14 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (12 12 (:REWRITE ADE::QUEUE10$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::QUEUE10$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (3 3 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 )
(ADE::QUEUE10$OUT-SEQ-NETLIST
 (3 3 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 )
(ADE::QUEUE10$OUT-SEQ-LEMMA
 (313 65 (:REWRITE ZP-OPEN))
 (213 35 (:DEFINITION BINARY-APPEND))
 (170 170 (:REWRITE NTH-WHEN-PREFIXP))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 120 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (120 40 (:REWRITE <-0-+-NEGATIVE-1))
 (117 117 (:REWRITE DEFAULT-CAR))
 (115 97 (:REWRITE DEFAULT-CDR))
 (88 72 (:REWRITE DEFAULT-+-2))
 (80 40 (:REWRITE ADE::QUEUE5$OUT-ACT-INACTIVE))
 (72 72 (:REWRITE DEFAULT-+-1))
 (72 36 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (48 16 (:REWRITE FOLD-CONSTS-IN-+))
 (30 6 (:DEFINITION NTHCDR))
 (29 29 (:REWRITE ADE::QUEUE10$EXTRACT-LEMMA))
 (28 14 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (18 18 (:TYPE-PRESCRIPTION ADE::SE))
 (12 12 (:REWRITE ADE::QUEUE10$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::QUEUE10$DATAFLOW-CORRECT-AUX
 (175 163 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (53 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (52 2 (:DEFINITION ADE::QUEUE10$IN-SEQ))
 (24 10 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$IN-ACT))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (5 5 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (4 4 (:TYPE-PRESCRIPTION ADE::QUEUE10$IN-ACT))
 (4 2 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (2 2 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::QUEUE10$DATAFLOW-CORRECT
 (619 106 (:REWRITE ZP-OPEN))
 (382 61 (:DEFINITION BINARY-APPEND))
 (319 11 (:DEFINITION NTHCDR))
 (234 73 (:REWRITE <-0-+-NEGATIVE-1))
 (212 145 (:REWRITE DEFAULT-+-2))
 (192 153 (:REWRITE DEFAULT-CDR))
 (175 25 (:DEFINITION LEN))
 (162 156 (:REWRITE DEFAULT-CAR))
 (156 145 (:REWRITE DEFAULT-+-1))
 (148 4 (:REWRITE TAKE-OF-TOO-MANY))
 (144 123 (:REWRITE DEFAULT-<-2))
 (129 123 (:REWRITE DEFAULT-<-1))
 (124 2 (:DEFINITION TAKE))
 (81 27 (:REWRITE FOLD-CONSTS-IN-+))
 (78 43 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (77 11 (:REWRITE COMMUTATIVITY-OF-+))
 (70 2 (:REWRITE CONSP-OF-TAKE))
 (58 4 (:REWRITE ADE::NFIX-OF-NAT))
 (56 56 (:REWRITE NTH-WHEN-PREFIXP))
 (48 27 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (36 4 (:LINEAR ADE::QUEUE10$EXTRACT-NOT-EMPTY))
 (34 2 (:REWRITE NATP-POSP--1))
 (32 32 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (30 2 (:REWRITE NATP-POSP))
 (28 28 (:TYPE-PRESCRIPTION ADE::QUEUE10$STEP))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (12 12 (:REWRITE ADE::QUEUE10$RUN-PLUS))
 (10 10 (:REWRITE ADE::QUEUE10$INPUT-FORMAT-PLUS))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:REWRITE POSP-NATP))
 (3 3 (:TYPE-PRESCRIPTION ADE::QUEUE10$RUN))
 )
(ADE::QUEUE10$FUNCTIONALLY-CORRECT
 (217 4 (:DEFINITION ADE::QUEUE10$OUT-SEQ))
 (121 4 (:REWRITE ADE::QUEUE10$EXTRACT-LEMMA))
 (104 4 (:DEFINITION ADE::QUEUE10$IN-SEQ))
 (87 3 (:DEFINITION NTHCDR))
 (80 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (60 33 (:REWRITE ZP-OPEN))
 (44 44 (:TYPE-PRESCRIPTION ZP))
 (39 30 (:REWRITE DEFAULT-CDR))
 (32 23 (:REWRITE DEFAULT-+-2))
 (27 27 (:TYPE-PRESCRIPTION LEN))
 (26 23 (:REWRITE DEFAULT-+-1))
 (24 24 (:REWRITE DEFAULT-CAR))
 (21 3 (:REWRITE COMMUTATIVITY-OF-+))
 (21 3 (:DEFINITION LEN))
 (20 5 (:REWRITE ADE::OPEN-QUEUE10$INPUT-FORMAT-N-ZP))
 (20 5 (:REWRITE ADE::OPEN-QUEUE10$INPUT-FORMAT-N))
 (18 12 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (16 16 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (16 8 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (16 8 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$IN-ACT))
 (12 3 (:REWRITE ADE::OPEN-QUEUE10$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-QUEUE10$RUN))
 (12 3 (:REWRITE ADE::OPEN-DE-N-ZP))
 (12 3 (:REWRITE ADE::OPEN-DE-N))
 (12 3 (:REWRITE <-0-+-NEGATIVE-1))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 (8 8 (:TYPE-PRESCRIPTION ADE::QUEUE10$OUT-ACT))
 (8 8 (:TYPE-PRESCRIPTION ADE::QUEUE10$IN-ACT))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 4 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (8 4 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (6 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:TYPE-PRESCRIPTION ADE::QUEUE10$RUN))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:REWRITE DEFAULT-<-1))
 )