(ADE::PISO-SREG$DATA-INS-LEN
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(ADE::PISO-SREG$INS-LEN)
(ADE::PISO-SREG*)
(ADE::PISO-SREG*$DESTRUCTURE
 (360 30 (:DEFINITION BINARY-APPEND))
 (342 60 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (135 135 (:TYPE-PRESCRIPTION POSP))
 (84 24 (:REWRITE CONSP-OF-REPEAT))
 (84 18 (:REWRITE ZP-OPEN))
 (60 60 (:TYPE-PRESCRIPTION REPEAT))
 (58 40 (:REWRITE DEFAULT-CDR))
 (53 35 (:REWRITE DEFAULT-CAR))
 (48 6 (:REWRITE REPEAT-WHEN-ZP))
 (42 30 (:DEFINITION NOT))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-<-1))
 (24 12 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 12 (:REWRITE DEFAULT-+-1))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 )
(ADE::NOT-PRIMP-PISO-SREG)
(ADE::PISO-SREG$NETLIST)
(ADE::PISO-SREG&)
(ADE::CHECK-PISO-SREG$NETLIST-64-7)
(ADE::PISO-SREG$ST-FORMAT)
(ADE::PISO-SREG$ST-FORMAT=>CONSTRAINT
 (20 4 (:DEFINITION LEN))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::PISO-SREG$VALID-ST)
(ADE::EXPT-LINEAR-LOWER-<=-INSTANCE
 (17 11 (:REWRITE DEFAULT-<-1))
 (11 11 (:REWRITE DEFAULT-<-2))
 (7 3 (:REWRITE DEFAULT-*-2))
 (6 2 (:REWRITE COMMUTATIVITY-OF-+))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-*-1))
 )
(ADE::PISO-SREG$VALID-ST=>CONSTRAINT
 (128 128 (:LINEAR LEN-WHEN-PREFIXP))
 (66 59 (:REWRITE DEFAULT-+-2))
 (64 64 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (59 59 (:REWRITE DEFAULT-+-1))
 (54 18 (:REWRITE DEFAULT-*-2))
 (49 49 (:REWRITE DEFAULT-<-2))
 (49 49 (:REWRITE DEFAULT-<-1))
 (20 4 (:DEFINITION LEN))
 (18 18 (:REWRITE DEFAULT-*-1))
 (16 16 (:REWRITE NTH-WHEN-PREFIXP))
 (16 4 (:DEFINITION STRIP-CARS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:REWRITE UNICITY-OF-0))
 (2 1 (:DEFINITION FIX))
 )
(ADE::PISO-SREG$VALID-ST=>ST-FORMAT
 (4 4 (:REWRITE NTH-WHEN-PREFIXP))
 )
(ADE::PISO-SREG$DATA-IN
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(ADE::LEN-PISO-SREG$DATA-IN)
(ADE::PISO-SREG$IN-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (5 5 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::PISO-SREG$IN-ACT-INACTIVE
 (16 5 (:REWRITE ADE::F-GATES=B-GATES))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (10 1 (:DEFINITION NTHCDR))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 1 (:REWRITE COMMUTATIVITY-OF-+))
 (5 1 (:REWRITE ADE::NFIX-OF-NAT))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::PISO-SREG$OUT-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (5 5 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::PISO-SREG$OUT-ACT-INACTIVE
 (16 5 (:REWRITE ADE::F-GATES=B-GATES))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (10 1 (:DEFINITION NTHCDR))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 1 (:REWRITE COMMUTATIVITY-OF-+))
 (5 1 (:REWRITE ADE::NFIX-OF-NAT))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE
 (362 362 (:REWRITE NTH-WHEN-PREFIXP))
 (264 198 (:REWRITE DEFAULT-+-2))
 (220 22 (:DEFINITION NTHCDR))
 (198 198 (:REWRITE DEFAULT-+-1))
 (128 32 (:DEFINITION STRIP-CARS))
 (105 105 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (102 102 (:REWRITE DEFAULT-CDR))
 (64 64 (:REWRITE DEFAULT-CAR))
 (64 18 (:REWRITE DEFAULT-*-2))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (32 16 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (25 23 (:REWRITE DEFAULT-<-1))
 (23 23 (:REWRITE DEFAULT-<-2))
 (18 18 (:REWRITE DEFAULT-*-1))
 (16 16 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 6 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (2 1 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 )
(ADE::PISO-SREG$BIT-OUT
 (12 5 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::BOOLEANP-PISO-SREG$BIT-OUT
 (408 96 (:REWRITE ADE::F-GATES=B-GATES))
 (216 216 (:REWRITE NTH-WHEN-PREFIXP))
 (160 16 (:DEFINITION NTHCDR))
 (113 18 (:REWRITE COMMUTATIVITY-OF-+))
 (104 16 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (98 83 (:REWRITE DEFAULT-+-2))
 (96 48 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (96 24 (:DEFINITION STRIP-CARS))
 (83 83 (:REWRITE DEFAULT-+-1))
 (64 52 (:REWRITE DEFAULT-CAR))
 (60 12 (:DEFINITION LEN))
 (59 18 (:REWRITE FOLD-CONSTS-IN-+))
 (52 52 (:REWRITE DEFAULT-CDR))
 (48 48 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (48 8 (:REWRITE ADE::LEN-STRIP-CARS))
 (35 1 (:DEFINITION EXPT))
 (32 16 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (16 16 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 (6 2 (:REWRITE DEFAULT-*-2))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:REWRITE ZIP-OPEN))
 (3 1 (:REWRITE UNICITY-OF-0))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 1 (:DEFINITION FIX))
 )
(ADE::PISO-SREG$OUTPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$BIT-OUT))
 )
(ADE::PISO-SREG$VALUE
 (2337 345 (:DEFINITION BINARY-APPEND))
 (1199 699 (:REWRITE DEFAULT-+-2))
 (891 182 (:REWRITE ADE::CAR-V-THREEFIX))
 (699 699 (:REWRITE DEFAULT-+-1))
 (618 79 (:REWRITE CONSP-OF-REPEAT))
 (498 498 (:TYPE-PRESCRIPTION PAIRLIS$))
 (364 182 (:DEFINITION ADE::3V-FIX))
 (355 29 (:REWRITE CAR-OF-APPEND))
 (339 52 (:REWRITE ADE::DISJOINT-ATOM))
 (314 78 (:REWRITE ZP-OPEN))
 (306 34 (:REWRITE CAR-OF-TAKE))
 (293 293 (:DEFINITION STRIP-CARS))
 (204 204 (:TYPE-PRESCRIPTION ADE::3VP))
 (199 198 (:REWRITE DEFAULT-<-2))
 (198 198 (:REWRITE DEFAULT-<-1))
 (176 16 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (154 142 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (144 113 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (143 16 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (135 113 (:REWRITE ADE::F-BUF-OF-3VP))
 (108 108 (:LINEAR LEN-WHEN-PREFIXP))
 (86 86 (:REWRITE NTH-WHEN-PREFIXP))
 (84 1 (:REWRITE PREFIXP-OF-APPEND-ARG2))
 (82 78 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (81 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (76 9 (:DEFINITION ATOM))
 (70 63 (:REWRITE REPEAT-WHEN-ZP))
 (59 39 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (58 31 (:REWRITE TAKE-WHEN-ATOM))
 (56 56 (:TYPE-PRESCRIPTION POSP))
 (54 54 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (49 39 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (45 1 (:DEFINITION SUBSETP-EQUAL))
 (44 8 (:REWRITE ADE::TV-IF$VALUE))
 (34 34 (:TYPE-PRESCRIPTION NFIX))
 (28 3 (:REWRITE ADE::DISJOINT-CONS))
 (28 2 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (27 19 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (22 22 (:TYPE-PRESCRIPTION ADE::NATP-TREE-NUMBER))
 (22 18 (:REWRITE ADE::FV-NOT=V-NOT))
 (21 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (20 4 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (18 6 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (17 17 (:REWRITE ADE::T-OR-NOR$VALUE))
 (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 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (14 1 (:DEFINITION MEMBER-EQUAL))
 (13 7 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (12 4 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (10 10 (:TYPE-PRESCRIPTION TAKE))
 (9 1 (:REWRITE LEN-WHEN-PREFIXP))
 (8 4 (:REWRITE ADE::BVP-TAKE))
 (8 2 (:DEFINITION TRUE-LISTP))
 (8 1 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (5 1 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (4 4 (:TYPE-PRESCRIPTION ATOM))
 (2 2 (:TYPE-PRESCRIPTION ADE::TREE-SIZE))
 (2 2 (:REWRITE ADE::TREE-SIZE-MAKE-TREE))
 (2 2 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (2 1 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 )
(ADE::PISO-SREG$STEP
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::LEN-CDR
 (18 9 (:REWRITE DEFAULT-+-2))
 (9 9 (:REWRITE DEFAULT-+-1))
 (8 8 (:REWRITE DEFAULT-CDR))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(ADE::PISO-SREG$STATE
 (6095 928 (:DEFINITION BINARY-APPEND))
 (2899 1722 (:REWRITE DEFAULT-+-2))
 (1882 237 (:REWRITE CONSP-OF-REPEAT))
 (1722 1722 (:REWRITE DEFAULT-+-1))
 (1689 522 (:REWRITE ADE::CAR-V-THREEFIX))
 (1501 1501 (:DEFINITION STRIP-CARS))
 (1239 1239 (:TYPE-PRESCRIPTION PAIRLIS$))
 (1044 522 (:DEFINITION ADE::3V-FIX))
 (946 236 (:REWRITE ZP-OPEN))
 (843 829 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (706 87 (:REWRITE CAR-OF-APPEND))
 (667 107 (:REWRITE ADE::DISJOINT-ATOM))
 (552 552 (:TYPE-PRESCRIPTION ADE::3VP))
 (506 46 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (487 486 (:REWRITE DEFAULT-<-2))
 (486 486 (:REWRITE DEFAULT-<-1))
 (450 411 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (441 411 (:REWRITE ADE::F-BUF-OF-3VP))
 (364 240 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (269 262 (:REWRITE REPEAT-WHEN-ZP))
 (259 3 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (258 258 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (224 182 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (168 168 (:REWRITE NTH-WHEN-PREFIXP))
 (134 94 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (114 94 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (114 37 (:REWRITE TAKE-WHEN-ATOM))
 (112 100 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (107 107 (:TYPE-PRESCRIPTION POSP))
 (107 99 (:REWRITE ADE::FV-NOT=V-NOT))
 (106 12 (:DEFINITION ATOM))
 (62 24 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (56 4 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (54 54 (:LINEAR LEN-WHEN-PREFIXP))
 (46 22 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (45 1 (:DEFINITION SUBSETP-EQUAL))
 (38 38 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (38 38 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (38 38 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (38 38 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (28 12 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (28 3 (:REWRITE ADE::DISJOINT-CONS))
 (27 27 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 24 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (18 2 (:REWRITE LEN-WHEN-PREFIXP))
 (16 16 (:TYPE-PRESCRIPTION TAKE))
 (15 5 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (14 1 (:DEFINITION MEMBER-EQUAL))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (8 2 (:DEFINITION TRUE-LISTP))
 (8 1 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (6 6 (:TYPE-PRESCRIPTION ATOM))
 (5 1 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (4 2 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (3 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE ADE::T-OR-NOR$VALUE))
 (2 2 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 )
(ADE::PISO-SREG$INPUT-FORMAT)
(ADE::BOOLEANP-PISO-SREG$IN-ACT
 (429 323 (:REWRITE DEFAULT-+-2))
 (396 396 (:REWRITE NTH-WHEN-PREFIXP))
 (373 83 (:REWRITE ADE::F-GATES=B-GATES))
 (323 323 (:REWRITE DEFAULT-+-1))
 (290 29 (:DEFINITION NTHCDR))
 (141 141 (:REWRITE DEFAULT-CDR))
 (127 37 (:REWRITE DEFAULT-*-2))
 (116 29 (:DEFINITION STRIP-CARS))
 (65 10 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (63 63 (:REWRITE DEFAULT-CAR))
 (63 5 (:REWRITE ADE::LEN-NTHCDR))
 (52 45 (:REWRITE DEFAULT-<-1))
 (45 45 (:REWRITE DEFAULT-<-2))
 (45 5 (:DEFINITION TRUE-LISTP))
 (37 37 (:REWRITE DEFAULT-*-1))
 (32 16 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (30 5 (:DEFINITION BINARY-APPEND))
 (26 26 (:LINEAR LEN-WHEN-PREFIXP))
 (25 10 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (20 10 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (15 5 (:REWRITE ADE::BVP-NTHCDR))
 (13 13 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 )
(ADE::BOOLEANP-PISO-SREG$OUT-ACT
 (1194 888 (:REWRITE DEFAULT-+-2))
 (888 888 (:REWRITE DEFAULT-+-1))
 (814 814 (:REWRITE NTH-WHEN-PREFIXP))
 (570 57 (:DEFINITION NTHCDR))
 (442 126 (:REWRITE DEFAULT-*-2))
 (340 340 (:REWRITE DEFAULT-CDR))
 (232 58 (:DEFINITION STRIP-CARS))
 (156 24 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (154 12 (:REWRITE ADE::LEN-NTHCDR))
 (147 127 (:REWRITE DEFAULT-<-1))
 (128 128 (:REWRITE DEFAULT-CAR))
 (127 127 (:REWRITE DEFAULT-<-2))
 (126 126 (:REWRITE DEFAULT-*-1))
 (108 12 (:DEFINITION TRUE-LISTP))
 (84 84 (:LINEAR LEN-WHEN-PREFIXP))
 (72 72 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (72 12 (:DEFINITION BINARY-APPEND))
 (60 24 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (48 24 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (42 42 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (36 12 (:REWRITE ADE::BVP-NTHCDR))
 (32 16 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (16 16 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::PISO-SREG$ST-FORMAT-PRESERVED
 (101 101 (:REWRITE NTH-WHEN-PREFIXP))
 (94 12 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (77 65 (:REWRITE DEFAULT-CAR))
 (76 19 (:DEFINITION STRIP-CARS))
 (68 4 (:DEFINITION BINARY-APPEND))
 (57 45 (:REWRITE DEFAULT-CDR))
 (49 39 (:REWRITE DEFAULT-+-2))
 (45 9 (:REWRITE ADE::F-GATES=B-GATES))
 (42 9 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (40 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (39 39 (:REWRITE DEFAULT-+-1))
 (37 37 (:TYPE-PRESCRIPTION BOOLEANP))
 (36 8 (:REWRITE CONSP-OF-REPEAT))
 (30 3 (:DEFINITION ADE::V-THREEFIX))
 (28 6 (:REWRITE ZP-OPEN))
 (24 24 (:TYPE-PRESCRIPTION ADE::BVP))
 (20 4 (:DEFINITION PAIRLIS$))
 (18 18 (:TYPE-PRESCRIPTION ADE::F-OR))
 (18 6 (:REWRITE ADE::V-THREEFIX-BVP))
 (18 4 (:REWRITE REPEAT-WHEN-ZP))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (15 15 (:TYPE-PRESCRIPTION ADE::F-AND))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (10 10 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (10 10 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (10 5 (:DEFINITION ADE::3V-FIX))
 (9 9 (:TYPE-PRESCRIPTION ADE::JOINT-ACT))
 (7 3 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (6 2 (:REWRITE ADE::FV-NOT=V-NOT))
 (6 2 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (6 2 (:REWRITE ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (5 5 (:TYPE-PRESCRIPTION ADE::3VP))
 (5 3 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (5 3 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 )
(ADE::PISO-SREG$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::PISO-SREG$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))
 (11 11 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (9 9 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(ADE::PISO-SREG$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::PISO-SREG$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO-SREG$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO-SREG$RUN)
(ADE::PISO-SREG$RUN-PLUS
 (87 25 (:REWRITE ZP-OPEN))
 (32 15 (:REWRITE DEFAULT-CDR))
 (27 27 (:REWRITE DEFAULT-<-2))
 (27 27 (:REWRITE DEFAULT-<-1))
 (27 10 (:REWRITE DEFAULT-CAR))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (23 23 (:REWRITE DEFAULT-+-2))
 (23 23 (:REWRITE DEFAULT-+-1))
 (16 8 (:REWRITE FOLD-CONSTS-IN-+))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(ADE::PISO-SREG$INPUT-FORMAT-N
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO-SREG$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO-SREG$INPUT-FORMAT-N)
(ADE::PISO-SREG$INPUT-FORMAT-PLUS
 (38 38 (:REWRITE DEFAULT-<-2))
 (38 38 (:REWRITE DEFAULT-<-1))
 (28 28 (:REWRITE DEFAULT-+-2))
 (28 28 (:REWRITE DEFAULT-+-1))
 (27 15 (:REWRITE DEFAULT-CDR))
 (27 15 (:REWRITE DEFAULT-CAR))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(ADE::PISO-SREG$DE-N
 (90 30 (:REWRITE ZP-OPEN))
 (28 2 (:DEFINITION ADE::PISO-SREG$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::PISO-SREG$INPUT-FORMAT-PLUS))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::PISO-SREG$OP)
(ADE::APPEND-OF-PISO-SREG$OP-WITH-SINGLETON)
(ADE::PISO-SREG$OP-MAP)
(ADE::PISO-SREG$OP-MAP-OF-APPEND
 (80 80 (:TYPE-PRESCRIPTION ADE::PISO-SREG$OP))
 (66 35 (:REWRITE DEFAULT-CDR))
 (45 42 (:REWRITE DEFAULT-CAR))
 (24 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 4 (:REWRITE CAR-OF-APPEND))
 (8 8 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::PISO-SREG$EXTRACT)
(ADE::V-TO-NAT-OF-V-ZP
 (88 44 (:TYPE-PRESCRIPTION ADE::BOOLEANP-V-NZP))
 (44 44 (:TYPE-PRESCRIPTION ADE::BVP))
 (34 34 (:REWRITE ADE::V-NZP-AS-OR-CROCK))
 (22 12 (:REWRITE DEFAULT-+-2))
 (22 12 (:REWRITE DEFAULT-*-2))
 (19 19 (:REWRITE DEFAULT-CDR))
 (17 17 (:REWRITE ADE::NOT-V-NZP-TAKE-NTHCDR))
 (15 15 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 12 (:REWRITE DEFAULT-*-1))
 (5 5 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 )
(ADE::PISO-SREG$EXTRACT-NOT-EMPTY
 (142 99 (:REWRITE DEFAULT-+-2))
 (128 2 (:DEFINITION TAKE))
 (124 4 (:REWRITE TAKE-OF-TOO-MANY))
 (111 111 (:REWRITE NTH-WHEN-PREFIXP))
 (99 99 (:REWRITE DEFAULT-+-1))
 (60 15 (:DEFINITION STRIP-CARS))
 (52 16 (:REWRITE ADE::F-GATES=B-GATES))
 (51 45 (:REWRITE DEFAULT-CDR))
 (51 17 (:REWRITE DEFAULT-*-2))
 (45 39 (:REWRITE DEFAULT-CAR))
 (44 22 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$OUT-ACT))
 (34 2 (:REWRITE ADE::LEN-CDR))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (32 24 (:REWRITE DEFAULT-<-2))
 (30 3 (:DEFINITION NTHCDR))
 (28 28 (:TYPE-PRESCRIPTION STRIP-CARS))
 (26 26 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (26 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (18 6 (:REWRITE UNICITY-OF-0))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 16 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (16 2 (:REWRITE ZP-OPEN))
 (14 2 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (12 6 (:DEFINITION FIX))
 (8 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (6 2 (:DEFINITION NATP))
 (4 4 (:TYPE-PRESCRIPTION TAKE))
 (4 4 (:TYPE-PRESCRIPTION ADE::PISO-SREG$IN-ACT))
 (4 2 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::LEN-OF-PISO-SREG$EXTRACT-LEMMA
 (784 16 (:DEFINITION TAKE))
 (640 32 (:REWRITE TAKE-OF-TOO-MANY))
 (256 16 (:REWRITE ADE::LEN-CDR))
 (208 139 (:REWRITE DEFAULT-+-2))
 (200 200 (:REWRITE NTH-WHEN-PREFIXP))
 (192 192 (:TYPE-PRESCRIPTION STRIP-CARS))
 (164 116 (:REWRITE DEFAULT-CDR))
 (152 38 (:DEFINITION STRIP-CARS))
 (144 96 (:REWRITE DEFAULT-CAR))
 (139 139 (:REWRITE DEFAULT-+-1))
 (128 32 (:REWRITE TAKE-WHEN-ATOM))
 (128 16 (:REWRITE ZP-OPEN))
 (75 59 (:REWRITE DEFAULT-<-2))
 (75 59 (:REWRITE DEFAULT-<-1))
 (33 11 (:REWRITE DEFAULT-*-2))
 (32 32 (:TYPE-PRESCRIPTION NFIX))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (20 2 (:DEFINITION NTHCDR))
 (19 6 (:REWRITE ADE::F-GATES=B-GATES))
 (18 18 (:LINEAR LEN-WHEN-PREFIXP))
 (14 14 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (11 11 (:REWRITE DEFAULT-*-1))
 (9 9 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (9 3 (:REWRITE UNICITY-OF-0))
 (6 3 (:DEFINITION FIX))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 1 (:DEFINITION NATP))
 (2 1 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:LINEAR ADE::PISO-SREG$EXTRACT-NOT-EMPTY))
 )
(ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1
 (384 6 (:DEFINITION TAKE))
 (372 12 (:REWRITE TAKE-OF-TOO-MANY))
 (227 151 (:REWRITE DEFAULT-+-2))
 (159 159 (:REWRITE NTH-WHEN-PREFIXP))
 (151 151 (:REWRITE DEFAULT-+-1))
 (102 6 (:REWRITE ADE::LEN-CDR))
 (101 83 (:REWRITE DEFAULT-CDR))
 (100 25 (:DEFINITION STRIP-CARS))
 (84 84 (:TYPE-PRESCRIPTION STRIP-CARS))
 (78 60 (:REWRITE DEFAULT-CAR))
 (78 24 (:REWRITE DEFAULT-*-2))
 (75 47 (:REWRITE DEFAULT-<-2))
 (62 62 (:LINEAR LEN-WHEN-PREFIXP))
 (53 47 (:REWRITE DEFAULT-<-1))
 (48 12 (:REWRITE TAKE-WHEN-ATOM))
 (48 6 (:REWRITE ZP-OPEN))
 (31 31 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (30 3 (:DEFINITION NTHCDR))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (24 24 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (24 24 (:REWRITE DEFAULT-*-1))
 (23 7 (:REWRITE ADE::F-GATES=B-GATES))
 (14 14 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (12 12 (:TYPE-PRESCRIPTION TAKE))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 1 (:DEFINITION NATP))
 (2 1 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:LINEAR ADE::PISO-SREG$EXTRACT-NOT-EMPTY))
 )
(ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2
 (30 15 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (15 15 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:LINEAR ADE::PISO-SREG$EXTRACT-NOT-EMPTY))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::PISO-SREG$INV)
(ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1
 (10 1 (:DEFINITION NTHCDR))
 (6 1 (:REWRITE COMMUTATIVITY-OF-+))
 (5 1 (:REWRITE ADE::NFIX-OF-NAT))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:DEFINITION NATP))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2
 (10 1 (:DEFINITION NTHCDR))
 (6 1 (:REWRITE COMMUTATIVITY-OF-+))
 (5 1 (:REWRITE ADE::NFIX-OF-NAT))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::PISO-SREG$INPUT-FORMAT-LEMMA-3
 (10 1 (:DEFINITION NTHCDR))
 (6 1 (:REWRITE COMMUTATIVITY-OF-+))
 (5 1 (:REWRITE ADE::NFIX-OF-NAT))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::LEN-OF-PISO-SREG$EXTRACT-UPPER-BOUND
 (287 241 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 (226 226 (:REWRITE NTH-WHEN-PREFIXP))
 (112 98 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (110 2 (:DEFINITION TAKE))
 (98 4 (:REWRITE TAKE-OF-TOO-MANY))
 (70 10 (:DEFINITION STRIP-CARS))
 (54 6 (:REWRITE ADE::LEN-STRIP-CARS))
 (44 2 (:REWRITE ADE::LEN-CDR))
 (38 23 (:REWRITE DEFAULT-+-2))
 (35 1 (:DEFINITION EXPT))
 (30 24 (:REWRITE DEFAULT-CDR))
 (28 22 (:REWRITE DEFAULT-CAR))
 (24 24 (:TYPE-PRESCRIPTION STRIP-CARS))
 (23 23 (:REWRITE DEFAULT-+-1))
 (17 11 (:REWRITE DEFAULT-<-2))
 (17 2 (:REWRITE COMMUTATIVITY-OF-+))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (16 2 (:REWRITE ZP-OPEN))
 (13 11 (:REWRITE DEFAULT-<-1))
 (11 2 (:REWRITE FOLD-CONSTS-IN-+))
 (6 2 (:REWRITE DEFAULT-*-2))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:REWRITE ZIP-OPEN))
 (3 1 (:REWRITE UNICITY-OF-0))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (2 1 (:DEFINITION FIX))
 (1 1 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (1 1 (:LINEAR ADE::PISO-SREG$EXTRACT-NOT-EMPTY))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::V-TO-NAT-OF-REPEAT-LEMMA
 (172 14 (:DEFINITION BINARY-APPEND))
 (163 57 (:REWRITE CONSP-OF-REPEAT))
 (161 12 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (142 48 (:REWRITE ZP-OPEN))
 (121 28 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (84 27 (:REWRITE DEFAULT-CDR))
 (68 66 (:REWRITE DEFAULT-<-1))
 (66 66 (:REWRITE DEFAULT-<-2))
 (63 21 (:REWRITE DEFAULT-CAR))
 (62 6 (:REWRITE CAR-OF-APPEND))
 (56 44 (:REWRITE DEFAULT-+-2))
 (44 44 (:REWRITE DEFAULT-+-1))
 (42 20 (:REWRITE DEFAULT-*-2))
 (24 7 (:LINEAR ADE::EXPT-LINEAR-LOWER-<=-INSTANCE))
 (23 23 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:REWRITE DEFAULT-*-1))
 (15 5 (:REWRITE FOLD-CONSTS-IN-+))
 (5 5 (:REWRITE ZIP-OPEN))
 (5 1 (:REWRITE ADE::NFIX-OF-NAT))
 (3 1 (:DEFINITION NATP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ADE::PISO-SREG$INV-PRESERVED
 (5434 128 (:DEFINITION STRIP-CARS))
 (5211 354 (:REWRITE DEFAULT-CAR))
 (4717 894 (:REWRITE DEFAULT-CDR))
 (1903 1282 (:REWRITE DEFAULT-+-2))
 (1282 1282 (:REWRITE DEFAULT-+-1))
 (1132 1132 (:REWRITE NTH-WHEN-PREFIXP))
 (875 34 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (832 17 (:DEFINITION BINARY-APPEND))
 (692 461 (:REWRITE DEFAULT-<-2))
 (611 6 (:DEFINITION ADE::V-THREEFIX))
 (558 13 (:DEFINITION PAIRLIS$))
 (478 478 (:LINEAR LEN-WHEN-PREFIXP))
 (461 461 (:REWRITE DEFAULT-<-1))
 (239 239 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (216 72 (:REWRITE DEFAULT-*-2))
 (191 44 (:REWRITE CONSP-OF-REPEAT))
 (174 10 (:REWRITE ADE::LEN-V-THREEFIX))
 (146 73 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (125 5 (:REWRITE ADE::CAR-V-THREEFIX))
 (100 22 (:REWRITE REPEAT-WHEN-ZP))
 (73 73 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (72 72 (:REWRITE DEFAULT-*-1))
 (69 69 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (35 35 (:TYPE-PRESCRIPTION ADE::F-AND4))
 (34 2 (:REWRITE TAKE-WHEN-ATOM))
 (24 24 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (22 11 (:DEFINITION ADE::3V-FIX))
 (21 21 (:TYPE-PRESCRIPTION ADE::JOINT-ACT))
 (17 17 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (12 4 (:DEFINITION NFIX))
 (12 2 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (12 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (11 11 (:TYPE-PRESCRIPTION ADE::3VP))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 2 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (6 2 (:DEFINITION NATP))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 2 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (2 2 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (2 2 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (2 2 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (1 1 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 )
(ADE::PISO-SREG$EXTRACTED-STEP
 (12 12 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$OUT-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 )
(ADE::PISO-SREG$EXTRACTED-STEP-CORRECT
 (17602 1118 (:REWRITE DEFAULT-CAR))
 (17022 3203 (:REWRITE DEFAULT-CDR))
 (16380 380 (:DEFINITION STRIP-CARS))
 (6732 4144 (:REWRITE DEFAULT-+-2))
 (4520 35 (:DEFINITION ADE::V-THREEFIX))
 (4239 4144 (:REWRITE DEFAULT-+-1))
 (3859 39 (:DEFINITION BINARY-APPEND))
 (2851 45 (:DEFINITION PAIRLIS$))
 (2780 2780 (:REWRITE NTH-WHEN-PREFIXP))
 (2669 78 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (2165 1297 (:REWRITE DEFAULT-<-2))
 (1813 65 (:REWRITE TAKE-WHEN-ATOM))
 (1381 1297 (:REWRITE DEFAULT-<-1))
 (1332 1332 (:LINEAR LEN-WHEN-PREFIXP))
 (1160 5 (:REWRITE TAKE-WHEN-PREFIXP))
 (1029 61 (:REWRITE ADE::LEN-V-THREEFIX))
 (817 32 (:REWRITE ADE::CAR-V-THREEFIX))
 (765 3 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (666 666 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (652 11 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (564 160 (:REWRITE DEFAULT-*-2))
 (469 88 (:REWRITE CONSP-OF-REPEAT))
 (300 10 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (258 36 (:DEFINITION NFIX))
 (210 10 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (160 160 (:REWRITE DEFAULT-*-1))
 (134 67 (:DEFINITION ADE::3V-FIX))
 (105 105 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (101 3 (:REWRITE CAR-OF-APPEND))
 (78 78 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (75 10 (:DEFINITION NATP))
 (67 67 (:TYPE-PRESCRIPTION ADE::3VP))
 (41 36 (:REWRITE DEFAULT-UNARY-MINUS))
 (40 2 (:REWRITE CONSP-OF-TAKE))
 (24 24 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (24 24 (:TYPE-PRESCRIPTION ADE::F-AND4))
 (24 4 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (18 18 (:TYPE-PRESCRIPTION ADE::F-AND3))
 (16 4 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (11 11 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (11 11 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (11 11 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (11 11 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (8 3 (:REWRITE LEN-OF-TAKE))
 (6 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (6 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 4 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (4 4 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (1 1 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 )
(ADE::PISO-SREG$VALID-ST-PRESERVED
 (19503 3331 (:REWRITE DEFAULT-CDR))
 (19389 1177 (:REWRITE DEFAULT-CAR))
 (15495 379 (:DEFINITION STRIP-CARS))
 (6894 58 (:DEFINITION BINARY-APPEND))
 (6230 3797 (:REWRITE DEFAULT-+-2))
 (4708 116 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (3797 3797 (:REWRITE DEFAULT-+-1))
 (3563 7 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3253 46 (:DEFINITION PAIRLIS$))
 (2937 2937 (:REWRITE NTH-WHEN-PREFIXP))
 (1594 58 (:REWRITE ADE::CAR-V-THREEFIX))
 (1317 821 (:REWRITE DEFAULT-<-2))
 (1010 1010 (:LINEAR LEN-WHEN-PREFIXP))
 (830 821 (:REWRITE DEFAULT-<-1))
 (580 5 (:REWRITE ADE::CADR-V-THREEFIX))
 (505 505 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (472 7 (:REWRITE CAR-OF-APPEND))
 (414 99 (:REWRITE CONSP-OF-REPEAT))
 (360 3 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (341 341 (:TYPE-PRESCRIPTION BOOLEANP))
 (317 70 (:REWRITE ZP-OPEN))
 (193 46 (:REWRITE REPEAT-WHEN-ZP))
 (126 63 (:DEFINITION ADE::3V-FIX))
 (123 41 (:REWRITE DEFAULT-*-2))
 (97 5 (:REWRITE ADE::NTHCDR-APPEND))
 (96 96 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (96 16 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (80 80 (:REWRITE DEFAULT-UNARY-MINUS))
 (78 78 (:TYPE-PRESCRIPTION ADE::3VP))
 (64 16 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (48 48 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (41 41 (:REWRITE DEFAULT-*-1))
 (26 26 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (24 24 (:TYPE-PRESCRIPTION ADE::F-AND))
 (22 22 (:TYPE-PRESCRIPTION ZP))
 (16 16 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (16 16 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (8 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (7 7 (:TYPE-PRESCRIPTION ADE::BOOLEANP-IF*))
 )
(ADE::PISO-SREG$EXTRACT-LEMMA
 (3907 2552 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 (1374 278 (:REWRITE DEFAULT-CAR))
 (1362 101 (:DEFINITION STRIP-CARS))
 (1303 1095 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (1056 20 (:DEFINITION TAKE))
 (1048 44 (:REWRITE TAKE-OF-TOO-MANY))
 (960 378 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (718 479 (:REWRITE DEFAULT-+-2))
 (618 618 (:REWRITE NTH-WHEN-PREFIXP))
 (479 479 (:REWRITE DEFAULT-+-1))
 (448 20 (:REWRITE ADE::LEN-CDR))
 (378 378 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (344 284 (:REWRITE DEFAULT-CDR))
 (320 16 (:REWRITE CONSP-OF-TAKE))
 (270 74 (:REWRITE DEFAULT-*-2))
 (256 32 (:REWRITE ZP-OPEN))
 (209 161 (:REWRITE DEFAULT-<-2))
 (193 161 (:REWRITE DEFAULT-<-1))
 (176 44 (:REWRITE TAKE-WHEN-ATOM))
 (112 8 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (74 74 (:REWRITE DEFAULT-*-1))
 (64 64 (:LINEAR LEN-WHEN-PREFIXP))
 (50 5 (:DEFINITION NTHCDR))
 (32 32 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$OUT-ACT))
 (24 8 (:REWRITE ADE::F-BUF-OF-3VP))
 (16 16 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (16 16 (:TYPE-PRESCRIPTION ADE::3VP))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (7 1 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (6 1 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (4 4 (:REWRITE ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (4 2 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 3 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO-SREG$IN-ACT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-CAR-OF-PISO-SREG$EXTRACT
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$OUT-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 )
(ADE::PISO-SREG$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 )
(ADE::PISO-SREG$IN-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::PISO-SREG$IN-SEQ-LEMMA
 (1156 364 (:REWRITE DEFAULT-CAR))
 (636 80 (:REWRITE ADE::F-GATES=B-GATES))
 (534 534 (:REWRITE NTH-WHEN-PREFIXP))
 (416 208 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (400 40 (:DEFINITION NTHCDR))
 (382 322 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (344 40 (:DEFINITION STRIP-CARS))
 (240 40 (:REWRITE COMMUTATIVITY-OF-+))
 (233 65 (:REWRITE ZP-OPEN))
 (232 232 (:REWRITE DEFAULT-+-2))
 (232 232 (:REWRITE DEFAULT-+-1))
 (213 35 (:DEFINITION BINARY-APPEND))
 (208 208 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (171 171 (:REWRITE DEFAULT-CDR))
 (168 56 (:REWRITE FOLD-CONSTS-IN-+))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (144 36 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (120 40 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (110 110 (:TYPE-PRESCRIPTION ADE::PISO-SREG$STEP))
 (84 14 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (80 80 (:TYPE-PRESCRIPTION ADE::BVP))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (36 36 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (22 22 (:TYPE-PRESCRIPTION ADE::DE))
 (14 14 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (14 14 (:REWRITE ADE::PISO-SREG$EXTRACT-LEMMA))
 (12 12 (:REWRITE ADE::PISO-SREG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::PISO-SREG$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (6 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$BIT-OUT))
 )
(ADE::PISO-SREG$OUT-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 )
(ADE::PISO-SREG$OUT-SEQ-LEMMA
 (1840 1196 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 (1153 361 (:REWRITE DEFAULT-CAR))
 (876 120 (:REWRITE ADE::F-GATES=B-GATES))
 (580 580 (:REWRITE NTH-WHEN-PREFIXP))
 (416 208 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (400 40 (:DEFINITION NTHCDR))
 (344 40 (:DEFINITION STRIP-CARS))
 (240 40 (:REWRITE COMMUTATIVITY-OF-+))
 (233 65 (:REWRITE ZP-OPEN))
 (232 232 (:REWRITE DEFAULT-+-2))
 (232 232 (:REWRITE DEFAULT-+-1))
 (216 36 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (213 35 (:DEFINITION BINARY-APPEND))
 (208 208 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (171 171 (:REWRITE DEFAULT-CDR))
 (168 56 (:REWRITE FOLD-CONSTS-IN-+))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 120 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (120 40 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (110 110 (:TYPE-PRESCRIPTION ADE::PISO-SREG$STEP))
 (80 80 (:TYPE-PRESCRIPTION ADE::BVP))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (56 14 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (39 39 (:REWRITE ADE::PISO-SREG$EXTRACT-LEMMA))
 (36 36 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (22 22 (:TYPE-PRESCRIPTION ADE::DE))
 (14 14 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (12 12 (:REWRITE ADE::PISO-SREG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::PISO-SREG$OP-OF-LEN-0
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (7 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-CDR))
 )
(ADE::PISO-SREG$DATAFLOW-CORRECT-AUX
 (175 163 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (72 2 (:DEFINITION ADE::PISO-SREG$OP-MAP))
 (53 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (30 2 (:REWRITE ADE::PISO-SREG$OP-OF-LEN-0))
 (26 12 (:REWRITE DEFAULT-CDR))
 (20 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (14 14 (:TYPE-PRESCRIPTION LEN))
 (12 12 (:REWRITE DEFAULT-CAR))
 (10 10 (:TYPE-PRESCRIPTION ADE::PISO-SREG$OP))
 (10 2 (:DEFINITION LEN))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (5 5 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::PISO-SREG$DATAFLOW-CORRECT
 (4881 515 (:DEFINITION LEN))
 (1578 187 (:REWRITE DEFAULT-CAR))
 (1573 128 (:REWRITE ADE::LEN-CDR))
 (1420 700 (:REWRITE DEFAULT-CDR))
 (1176 615 (:REWRITE DEFAULT-+-2))
 (948 531 (:REWRITE DEFAULT-<-2))
 (914 40 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (826 826 (:LINEAR LEN-WHEN-PREFIXP))
 (615 615 (:REWRITE DEFAULT-+-1))
 (531 531 (:REWRITE DEFAULT-<-1))
 (413 413 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (353 89 (:REWRITE ZP-OPEN))
 (144 144 (:TYPE-PRESCRIPTION ADE::PISO-SREG$IN-SEQ))
 (132 36 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (102 14 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (95 20 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (55 55 (:REWRITE NTH-WHEN-PREFIXP))
 (52 52 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (45 5 (:REWRITE ADE::LEN-PISO-SREG$DATA-IN))
 (25 5 (:REWRITE ADE::NFIX-OF-NAT))
 (24 8 (:REWRITE FOLD-CONSTS-IN-+))
 (16 16 (:TYPE-PRESCRIPTION ADE::PISO-SREG$STEP))
 (15 5 (:DEFINITION NFIX))
 (15 5 (:DEFINITION NATP))
 (12 12 (:REWRITE ADE::PISO-SREG$RUN-PLUS))
 (12 12 (:REWRITE ADE::PISO-SREG$INPUT-FORMAT-PLUS))
 (6 2 (:REWRITE ADE::PISO-SREG$INV-PRESERVED))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION ADE::PISO-SREG$RUN))
 )
(ADE::PISO-SREG$FUNCTIONALLY-CORRECT
 (239 12 (:REWRITE ADE::PISO-SREG$OP-OF-LEN-0))
 (192 4 (:DEFINITION ADE::PISO-SREG$IN-SEQ))
 (152 4 (:DEFINITION ADE::PISO-SREG$OP-MAP))
 (139 21 (:DEFINITION LEN))
 (138 4 (:DEFINITION ADE::PISO-SREG$OUT-SEQ))
 (120 120 (:TYPE-PRESCRIPTION LEN))
 (100 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (88 4 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (65 11 (:LINEAR ADE::LEN-OF-PISO-SREG$EXTRACT-UPPER-BOUND))
 (53 53 (:REWRITE DEFAULT-CDR))
 (52 52 (:TYPE-PRESCRIPTION ZP))
 (50 29 (:REWRITE DEFAULT-+-2))
 (34 34 (:REWRITE ZP-OPEN))
 (32 32 (:REWRITE DEFAULT-CAR))
 (32 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (30 30 (:LINEAR LEN-WHEN-PREFIXP))
 (29 29 (:REWRITE DEFAULT-+-1))
 (28 28 (:TYPE-PRESCRIPTION ADE::PISO-SREG$IN-SEQ))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$IN-ACT))
 (24 6 (:REWRITE ADE::OPEN-PISO-SREG$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-PISO-SREG$INPUT-FORMAT-N))
 (24 4 (:REWRITE ADE::PISO-SREG$OUT-ACT-INACTIVE))
 (22 22 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT))
 (22 4 (:REWRITE ADE::PISO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (16 16 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-2))
 (16 8 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO-SREG$OUT-ACT))
 (16 4 (:REWRITE ADE::PISO-SREG$IN-ACT-INACTIVE))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (15 15 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 14 (:TYPE-PRESCRIPTION ADE::PISO-SREG$IN-ACT))
 (12 3 (:REWRITE ADE::OPEN-PISO-SREG$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-PISO-SREG$RUN))
 (11 11 (:LINEAR ADE::PISO-SREG$EXTRACT-NOT-EMPTY))
 (8 8 (:TYPE-PRESCRIPTION ADE::PISO-SREG$OUT-ACT))
 (8 8 (:TYPE-PRESCRIPTION ADE::PISO-SREG$INPUT-FORMAT-LEMMA-1))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (6 3 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE ADE::LEN-OF-PISO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (4 4 (:REWRITE ADE::PISO-SREG$EXTRACT-LEMMA))
 (3 3 (:TYPE-PRESCRIPTION ADE::PISO-SREG$RUN))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:REWRITE DEFAULT-<-1))
 )