(ADE::F-BUF
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::NTH-V-THREEFIX
 (108 108 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (60 20 (:REWRITE ADE::V-THREEFIX-BVP))
 (40 40 (:TYPE-PRESCRIPTION ADE::BVP))
 (36 34 (:REWRITE DEFAULT-CAR))
 (25 21 (:REWRITE DEFAULT-CDR))
 (20 20 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (20 5 (:REWRITE ADE::CAR-V-THREEFIX))
 (16 16 (:REWRITE ZP-OPEN))
 (16 16 (:REWRITE DEFAULT-+-2))
 (16 16 (:REWRITE DEFAULT-+-1))
 )
(ADE::BOOLEANP-OF-F-BUF
 (14 14 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-AND)
(ADE::3VP-F-AND)
(ADE::F-AND3)
(ADE::F-AND4)
(ADE::F-AND5)
(ADE::F-NOT)
(ADE::F-NAND)
(ADE::F-NAND3)
(ADE::F-NAND4)
(ADE::F-NAND5)
(ADE::F-NAND6)
(ADE::F-NAND8)
(ADE::F-OR)
(ADE::3VP-F-OR)
(ADE::F-OR3)
(ADE::F-OR4)
(ADE::F-OR5)
(ADE::F-NOR)
(ADE::F-NOR3)
(ADE::F-NOR4)
(ADE::F-NOR5)
(ADE::F-NOR6)
(ADE::F-NOR8)
(ADE::F-XOR)
(ADE::F-XOR3
 (13 13 (:TYPE-PRESCRIPTION ADE::F-XOR))
 )
(ADE::F-XNOR)
(ADE::F-EQUV)
(ADE::F-EQUV3
 (12 5 (:TYPE-PRESCRIPTION ADE::F-EQUV))
 (8 8 (:TYPE-PRESCRIPTION ADE::F-XOR))
 )
(ADE::F-IF)
(ADE::3VP-F-IF)
(ADE::FT-BUF)
(ADE::FT-WIRE)
(ADE::F-PULLUP
 (1 1 (:TYPE-PRESCRIPTION ADE::F-PULLUP))
 )
(ADE::F-BOOL)
(ADE::BOOLEANP-F-BOOL)
(ADE::F-SR)
(ADE::3VP-F-SR)
(ADE::F$AO2)
(ADE::F-BUF-OF-3VP
 (16 16 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-BUF-OF-NOT-BOOLEANP)
(ADE::F-AND-REWRITE
 (28 28 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-OR-REWRITE
 (28 28 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-NOT-REWRITE)
(ADE::F-XOR-REWRITE
 (28 28 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-XNOR-REWRITE
 (28 28 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-NAND-REWRITE)
(ADE::FT-BUF-REWRITE
 (68 53 (:TYPE-PRESCRIPTION ADE::FT-BUF))
 (42 41 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 )
(ADE::F-IF-REWRITE
 (30 30 (:TYPE-PRESCRIPTION ADE::F-IF))
 (28 28 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::FT-WIRE-REWRITE
 (60 60 (:TYPE-PRESCRIPTION ADE::FT-WIRE))
 (30 30 (:TYPE-PRESCRIPTION ADE::4V-FIX))
 )
(ADE::F-PULLUP-REWRITE)
(ADE::3V-FIX-HELP-LEMMA
 (30 30 (:TYPE-PRESCRIPTION ADE::F-XOR))
 (30 30 (:TYPE-PRESCRIPTION ADE::F-XNOR))
 (30 30 (:TYPE-PRESCRIPTION ADE::F-EQUV))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-NOT-F-NOT=F-BUF
 (14 14 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-NOT-F-BUF=F-NOT)
(ADE::F-BUF-DELETE-LEMMAS-1
 (30 30 (:TYPE-PRESCRIPTION ADE::F-XNOR))
 (30 30 (:TYPE-PRESCRIPTION ADE::F-IF))
 )
(ADE::F-BUF-DELETE-LEMMAS-2
 (328 326 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (177 147 (:TYPE-PRESCRIPTION ADE::F-IF))
 (37 36 (:TYPE-PRESCRIPTION ADE::FT-BUF))
 (6 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (5 5 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-GATE-3V-FIX-CONGRUENCE-LEMMAS$HELP
 (204 202 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (177 147 (:TYPE-PRESCRIPTION ADE::F-IF))
 (3 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-GATE-3V-FIX-CONGRUENCE-LEMMAS
 (177 147 (:TYPE-PRESCRIPTION ADE::F-IF))
 (45 15 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (45 15 (:REWRITE ADE::F-BUF-OF-3VP))
 (37 36 (:TYPE-PRESCRIPTION ADE::FT-BUF))
 (3 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::F-GATES=B-GATES)
(ADE::FV-NOT)
(ADE::LEN-FV-NOT
 (14 7 (:REWRITE DEFAULT-+-2))
 (9 8 (:REWRITE DEFAULT-CDR))
 (9 3 (:REWRITE ADE::F-GATES=B-GATES))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(ADE::FV-NOT-OF-V-THREEFIX-CANCELED
 (33 7 (:REWRITE ADE::F-GATES=B-GATES))
 (18 6 (:REWRITE ADE::V-THREEFIX-BVP))
 (15 12 (:REWRITE DEFAULT-CAR))
 (14 14 (:TYPE-PRESCRIPTION BOOLEANP))
 (13 10 (:REWRITE DEFAULT-CDR))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP))
 (12 3 (:REWRITE ADE::CAR-V-THREEFIX))
 )
(ADE::FV-NOT=V-NOT
 (12 12 (:REWRITE DEFAULT-CAR))
 (6 6 (:REWRITE DEFAULT-CDR))
 (2 2 (:DEFINITION ADE::F-NOT))
 )
(ADE::FV-AND)
(ADE::LEN-FV-AND
 (14 7 (:REWRITE DEFAULT-+-2))
 (11 10 (:REWRITE DEFAULT-CDR))
 (9 3 (:REWRITE ADE::F-GATES=B-GATES))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::FV-AND-OF-V-THREEFIX-CANCELED
 (384 105 (:REWRITE ADE::F-GATES=B-GATES))
 (272 92 (:REWRITE ADE::V-THREEFIX-BVP))
 (204 204 (:TYPE-PRESCRIPTION BOOLEANP))
 (180 180 (:TYPE-PRESCRIPTION ADE::BVP))
 (136 34 (:REWRITE ADE::CAR-V-THREEFIX))
 )
(ADE::FV-AND=V-AND
 (37 35 (:REWRITE DEFAULT-CAR))
 (23 12 (:REWRITE DEFAULT-+-2))
 (20 18 (:REWRITE DEFAULT-CDR))
 (18 6 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP-LEN))
 (12 12 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:DEFINITION ADE::F-AND))
 )
(ADE::FV-OR)
(ADE::LEN-FV-OR
 (14 7 (:REWRITE DEFAULT-+-2))
 (11 10 (:REWRITE DEFAULT-CDR))
 (9 3 (:REWRITE ADE::F-GATES=B-GATES))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::FV-OR-OF-V-THREEFIX-CANCELED
 (430 147 (:REWRITE ADE::F-GATES=B-GATES))
 (288 288 (:TYPE-PRESCRIPTION BOOLEANP))
 (272 92 (:REWRITE ADE::V-THREEFIX-BVP))
 (180 180 (:TYPE-PRESCRIPTION ADE::BVP))
 (162 40 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (136 34 (:REWRITE ADE::CAR-V-THREEFIX))
 )
(ADE::FV-OR=V-OR
 (37 35 (:REWRITE DEFAULT-CAR))
 (36 12 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (24 24 (:TYPE-PRESCRIPTION ADE::BVP-LEN))
 (23 12 (:REWRITE DEFAULT-+-2))
 (20 18 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:DEFINITION ADE::F-OR))
 )
(ADE::FV-XOR
 (1 1 (:TYPE-PRESCRIPTION ADE::F-XOR))
 )
(ADE::LEN-FV-XOR
 (18 6 (:REWRITE ADE::F-GATES=B-GATES))
 (14 7 (:REWRITE DEFAULT-+-2))
 (12 12 (:TYPE-PRESCRIPTION BOOLEANP))
 (11 10 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::FV-XOR-OF-V-THREEFIX-CANCELED
 (648 210 (:REWRITE ADE::F-GATES=B-GATES))
 (272 92 (:REWRITE ADE::V-THREEFIX-BVP))
 (180 180 (:TYPE-PRESCRIPTION ADE::BVP))
 (165 41 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (136 34 (:REWRITE ADE::CAR-V-THREEFIX))
 )
(ADE::FV-XOR=V-XOR
 (41 39 (:REWRITE DEFAULT-CAR))
 (23 12 (:REWRITE DEFAULT-+-2))
 (20 18 (:REWRITE DEFAULT-CDR))
 (14 2 (:DEFINITION ADE::F-XOR))
 (12 12 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:DEFINITION ADE::F-NOT))
 )
(ADE::FV-XNOR
 (1 1 (:TYPE-PRESCRIPTION ADE::F-XNOR))
 )
(ADE::LEN-FV-XNOR
 (18 6 (:REWRITE ADE::F-GATES=B-GATES))
 (14 7 (:REWRITE DEFAULT-+-2))
 (12 12 (:TYPE-PRESCRIPTION BOOLEANP))
 (11 10 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::FV-XNOR-OF-V-THREEFIX-CANCELED
 (791 263 (:REWRITE ADE::F-GATES=B-GATES))
 (352 120 (:REWRITE ADE::V-THREEFIX-BVP))
 (232 232 (:TYPE-PRESCRIPTION ADE::BVP))
 (184 46 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 )
(ADE::FV-XNOR=V-XNOR
 (41 39 (:REWRITE DEFAULT-CAR))
 (23 12 (:REWRITE DEFAULT-+-2))
 (20 18 (:REWRITE DEFAULT-CDR))
 (14 2 (:DEFINITION ADE::F-XNOR))
 (12 12 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:DEFINITION ADE::F-NOT))
 )
(ADE::FV-IF
 (1 1 (:TYPE-PRESCRIPTION ADE::F-IF))
 )
(ADE::LEN-FV-IF
 (14 7 (:REWRITE DEFAULT-+-2))
 (11 10 (:REWRITE DEFAULT-CDR))
 (9 3 (:REWRITE ADE::F-GATES=B-GATES))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::V-THREEFIX-FV-IF
 (24 8 (:REWRITE ADE::V-THREEFIX-BVP))
 (21 18 (:REWRITE DEFAULT-CAR))
 (18 6 (:REWRITE ADE::F-GATES=B-GATES))
 (17 14 (:REWRITE DEFAULT-CDR))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (12 12 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::FV-IF-WHEN-BOOLEANP-C
 (144 48 (:REWRITE ADE::F-GATES=B-GATES))
 (142 142 (:TYPE-PRESCRIPTION BOOLEANP))
 (120 40 (:REWRITE ADE::V-THREEFIX-BVP))
 (80 80 (:TYPE-PRESCRIPTION ADE::BVP))
 (69 23 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (69 23 (:REWRITE ADE::F-BUF-OF-3VP))
 (20 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 )
(ADE::FV-IF-WHEN-BVP
 (50 25 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-IF*))
 (50 25 (:TYPE-PRESCRIPTION ADE::BOOLEANP-IF*))
 (30 6 (:DEFINITION LEN))
 (25 25 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (25 25 (:TYPE-PRESCRIPTION IF*))
 (18 6 (:DEFINITION ADE::BVP))
 (14 14 (:REWRITE DEFAULT-CDR))
 (13 1 (:DEFINITION ADE::FV-IF))
 (12 6 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-CAR))
 (6 6 (:REWRITE DEFAULT-+-1))
 (5 1 (:DEFINITION ADE::F-IF))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 )
(ADE::FV-IF-REWRITE
 (289 29 (:REWRITE ZP-OPEN))
 (283 22 (:REWRITE REPEAT-WHEN-ZP))
 (80 49 (:REWRITE DEFAULT-<-2))
 (77 43 (:REWRITE DEFAULT-+-2))
 (49 49 (:REWRITE DEFAULT-<-1))
 (43 43 (:REWRITE DEFAULT-+-1))
 (36 32 (:REWRITE DEFAULT-CDR))
 (32 12 (:REWRITE ADE::V-THREEFIX-BVP))
 (30 26 (:REWRITE DEFAULT-CAR))
 (29 17 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (24 24 (:TYPE-PRESCRIPTION ADE::BVP))
 (20 20 (:TYPE-PRESCRIPTION ZP))
 (12 8 (:REWRITE ADE::F-GATES=B-GATES))
 )
(ADE::FV-IF-F-BUF-CANCELED
 (42 16 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (30 30 (:TYPE-PRESCRIPTION BOOLEANP))
 (21 8 (:REWRITE ADE::F-GATES=B-GATES))
 (20 18 (:REWRITE DEFAULT-CAR))
 (16 14 (:REWRITE DEFAULT-CDR))
 )
(ADE::FV-IF-V-THREEFIX-CANCELED
 (862 254 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (550 550 (:TYPE-PRESCRIPTION ADE::BVP))
 (496 160 (:REWRITE ADE::V-THREEFIX-BVP))
 (425 141 (:REWRITE ADE::F-GATES=B-GATES))
 (412 412 (:TYPE-PRESCRIPTION BOOLEANP))
 (336 24 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (264 132 (:REWRITE DEFAULT-+-2))
 (192 24 (:DEFINITION TRUE-LISTP))
 (176 44 (:REWRITE ADE::CAR-V-THREEFIX))
 (162 27 (:REWRITE ADE::LEN-V-THREEFIX))
 (144 48 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (132 132 (:REWRITE DEFAULT-+-1))
 (120 120 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (48 14 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (36 12 (:DEFINITION ADE::F-BUF))
 )
(ADE::VFT-WIRE
 (1 1 (:TYPE-PRESCRIPTION ADE::FT-WIRE))
 )
(ADE::VFT-WIRE-X-X=X
 (18 6 (:REWRITE ADE::BVP-V-FOURFIX))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP))
 (9 9 (:REWRITE DEFAULT-CAR))
 (6 6 (:REWRITE DEFAULT-CDR))
 )
(ADE::VFT-WIRE-MAKE-LIST-Z-1
 (102 9 (:REWRITE ZP-OPEN))
 (92 6 (:REWRITE REPEAT-WHEN-ZP))
 (44 4 (:DEFINITION ADE::FT-WIRE))
 (36 18 (:REWRITE DEFAULT-<-2))
 (28 16 (:REWRITE DEFAULT-CDR))
 (25 13 (:REWRITE DEFAULT-CAR))
 (24 8 (:REWRITE ADE::BVP-V-FOURFIX))
 (18 18 (:REWRITE DEFAULT-<-1))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:REWRITE DEFAULT-+-1))
 )
(ADE::VFT-WIRE-MAKE-LIST-Z-2
 (120 6 (:REWRITE CONSP-OF-REPEAT))
 (104 10 (:REWRITE ZP-OPEN))
 (79 13 (:REWRITE DEFAULT-CDR))
 (77 11 (:REWRITE DEFAULT-CAR))
 (74 5 (:REWRITE REPEAT-WHEN-ZP))
 (40 20 (:REWRITE DEFAULT-<-2))
 (33 3 (:DEFINITION ADE::FT-WIRE))
 (24 8 (:REWRITE ADE::BVP-V-FOURFIX))
 (20 20 (:REWRITE DEFAULT-<-1))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:REWRITE DEFAULT-+-1))
 )
(ADE::LEN-VFT-WIRE
 (14 7 (:REWRITE DEFAULT-+-2))
 (11 10 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::VFT-WIRE-MAKE-LIST-X
 (295 32 (:REWRITE ZP-OPEN))
 (232 22 (:REWRITE REPEAT-WHEN-ZP))
 (120 6 (:REWRITE CONSP-OF-REPEAT))
 (92 55 (:REWRITE DEFAULT-<-2))
 (81 14 (:REWRITE DEFAULT-CDR))
 (75 8 (:REWRITE DEFAULT-CAR))
 (55 55 (:REWRITE DEFAULT-<-1))
 (33 21 (:REWRITE DEFAULT-+-2))
 (33 3 (:DEFINITION ADE::FT-WIRE))
 (21 21 (:REWRITE DEFAULT-+-1))
 (18 9 (:DEFINITION ADE::4V-FIX))
 (17 17 (:TYPE-PRESCRIPTION ZP))
 (9 9 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::V-PULLUP
 (1 1 (:TYPE-PRESCRIPTION ADE::F-PULLUP))
 )
(ADE::LEN-V-PULLUP
 (14 7 (:REWRITE DEFAULT-+-2))
 (9 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(ADE::V-PULLUP-BVP
 (16 16 (:REWRITE DEFAULT-CAR))
 (13 13 (:REWRITE DEFAULT-CDR))
 )
(ADE::V-PULLUP-MAKE-LIST-Z
 (54 21 (:REWRITE ZP-OPEN))
 (45 10 (:REWRITE ADE::V-PULLUP-BVP))
 (25 12 (:REWRITE CONSP-OF-REPEAT))
 (20 20 (:TYPE-PRESCRIPTION ADE::BVP))
 (20 4 (:DEFINITION ADE::F-PULLUP))
 (18 5 (:REWRITE DEFAULT-CDR))
 (18 5 (:REWRITE DEFAULT-CAR))
 (14 14 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE DEFAULT-<-1))
 (10 10 (:TYPE-PRESCRIPTION ADE::BVP-REPEAT-OF-BOOLEAN))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (6 6 (:REWRITE DEFAULT-+-2))
 (6 6 (:REWRITE DEFAULT-+-1))
 (5 5 (:REWRITE ADE::BVP-REPEAT-OF-BOOLEAN))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 )
(ADE::FV-SHIFT-RIGHT
 (1 1 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 )
(ADE::FV-SHIFT-RIGHT=V-SHIFT-RIGHT
 (19 4 (:DEFINITION BINARY-APPEND))
 (16 16 (:REWRITE DEFAULT-CDR))
 (15 1 (:DEFINITION ADE::V-THREEFIX))
 (12 12 (:REWRITE DEFAULT-CAR))
 (4 1 (:REWRITE ADE::CAR-V-THREEFIX))
 )
(ADE::LEN-FV-SHIFT-RIGHT
 (150 115 (:REWRITE DEFAULT-CDR))
 (105 35 (:REWRITE ADE::V-THREEFIX-BVP))
 (102 51 (:REWRITE DEFAULT-+-2))
 (70 70 (:TYPE-PRESCRIPTION ADE::BVP))
 (52 13 (:REWRITE ADE::CAR-V-THREEFIX))
 (51 51 (:REWRITE DEFAULT-+-1))
 (42 40 (:REWRITE DEFAULT-CAR))
 (31 31 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (18 6 (:REWRITE ADE::FV-SHIFT-RIGHT=V-SHIFT-RIGHT))
 (12 12 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::V-THREEFIX-FV-SHIFT-RIGHT
 (32 4 (:DEFINITION BINARY-APPEND))
 (31 11 (:REWRITE ADE::V-THREEFIX-BVP))
 (20 20 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 4 (:REWRITE ADE::CAR-V-THREEFIX))
 (14 14 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE ADE::FV-SHIFT-RIGHT=V-SHIFT-RIGHT))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::FV-SHIFT-RIGHT-REMOVES-F-BUF
 (32 4 (:DEFINITION ADE::V-THREEFIX))
 (32 4 (:DEFINITION BINARY-APPEND))
 (22 8 (:REWRITE ADE::V-THREEFIX-BVP))
 (16 4 (:REWRITE ADE::CAR-V-THREEFIX))
 (14 14 (:TYPE-PRESCRIPTION ADE::BVP))
 (12 12 (:REWRITE DEFAULT-CDR))
 (9 2 (:REWRITE ADE::FV-SHIFT-RIGHT=V-SHIFT-RIGHT))
 (8 8 (:REWRITE DEFAULT-CAR))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::VFT-BUF
 (1 1 (:TYPE-PRESCRIPTION ADE::FT-BUF))
 )
(ADE::LEN-VFT-BUF
 (14 7 (:REWRITE DEFAULT-+-2))
 (9 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(ADE::VFT-BUF-LEMMAS
 (130 13 (:REWRITE ZP-OPEN))
 (128 10 (:REWRITE REPEAT-WHEN-ZP))
 (36 22 (:REWRITE DEFAULT-<-2))
 (22 22 (:REWRITE DEFAULT-<-1))
 (18 6 (:REWRITE ADE::V-THREEFIX-BVP))
 (16 10 (:REWRITE DEFAULT-+-2))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP))
 (10 10 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE DEFAULT-+-1))
 (9 9 (:TYPE-PRESCRIPTION ZP))
 )
(ADE::VFT-BUF-REWRITE
 (232 24 (:REWRITE ZP-OPEN))
 (219 18 (:REWRITE REPEAT-WHEN-ZP))
 (64 40 (:REWRITE DEFAULT-<-2))
 (40 40 (:REWRITE DEFAULT-<-1))
 (26 17 (:REWRITE DEFAULT-+-2))
 (17 17 (:REWRITE DEFAULT-+-1))
 (16 16 (:TYPE-PRESCRIPTION ZP))
 (10 10 (:REWRITE DEFAULT-CDR))
 (8 1 (:DEFINITION ADE::V-THREEFIX))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 )
(ADE::FV-ADDER
 (1 1 (:TYPE-PRESCRIPTION ADE::F-XOR))
 (1 1 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 )
(ADE::LEN-FV-ADDER
 (76 25 (:REWRITE ADE::F-GATES=B-GATES))
 (36 36 (:TYPE-PRESCRIPTION BOOLEANP))
 (26 13 (:REWRITE DEFAULT-+-2))
 (15 11 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE DEFAULT-CAR))
 (13 13 (:REWRITE DEFAULT-+-1))
 (8 4 (:DEFINITION ADE::F-AND))
 (8 2 (:DEFINITION ADE::F-OR))
 )
(ADE::V-THREEFIX-FV-ADDER
 (152 50 (:REWRITE ADE::F-GATES=B-GATES))
 (72 72 (:TYPE-PRESCRIPTION BOOLEANP))
 (43 37 (:REWRITE DEFAULT-CAR))
 (27 9 (:REWRITE ADE::V-THREEFIX-BVP))
 (23 17 (:REWRITE DEFAULT-CDR))
 (18 18 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 8 (:DEFINITION ADE::F-AND))
 (16 4 (:DEFINITION ADE::F-OR))
 )
(ADE::FV-ADDER-OF-F-BUF-CANCELED
 (863 313 (:REWRITE ADE::F-GATES=B-GATES))
 (286 260 (:REWRITE DEFAULT-CAR))
 (140 114 (:REWRITE DEFAULT-CDR))
 (72 52 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (54 13 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (35 13 (:REWRITE ADE::F-BUF-OF-3VP))
 (20 20 (:TYPE-PRESCRIPTION ADE::F-OR))
 (9 3 (:REWRITE ADE::3V-FIX-IDEMPOTENT))
 )
(ADE::FV-ADDER-OF-V-THREEFIX-CANCELED-1
 (2028 618 (:REWRITE ADE::F-GATES=B-GATES))
 (626 539 (:REWRITE DEFAULT-CAR))
 (356 283 (:REWRITE DEFAULT-CDR))
 (172 62 (:REWRITE ADE::V-THREEFIX-BVP))
 (110 110 (:TYPE-PRESCRIPTION ADE::BVP))
 (10 10 (:TYPE-PRESCRIPTION ADE::F-OR))
 (2 2 (:TYPE-PRESCRIPTION ADE::F-AND))
 (1 1 (:REWRITE ADE::3VP-F-OR))
 )
(ADE::FV-ADDER-OF-V-THREEFIX-CANCELED-2
 (3936 1807 (:REWRITE ADE::F-GATES=B-GATES))
 (1103 1103 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (432 152 (:REWRITE ADE::V-THREEFIX-BVP))
 (280 280 (:TYPE-PRESCRIPTION ADE::BVP))
 (53 53 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (10 10 (:TYPE-PRESCRIPTION ADE::F-OR))
 (2 2 (:TYPE-PRESCRIPTION ADE::F-AND))
 (1 1 (:REWRITE ADE::3VP-F-OR))
 )
(ADE::FV-ADDER=V-ADDER
 (1427 1215 (:REWRITE DEFAULT-CAR))
 (845 637 (:REWRITE DEFAULT-CDR))
 (777 204 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (75 25 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (1 1 (:REWRITE ADE::3VP-F-AND))
 )
(ADE::FV-ADDER-OUTPUT)
(ADE::LEN-FV-ADDER-OUTPUT
 (74 1 (:DEFINITION ADE::FV-ADDER))
 (57 1 (:DEFINITION TAKE))
 (46 2 (:REWRITE TAKE-OF-TOO-MANY))
 (34 6 (:DEFINITION LEN))
 (33 2 (:REWRITE TAKE-OF-LEN-FREE))
 (30 10 (:REWRITE ADE::F-GATES=B-GATES))
 (27 3 (:DEFINITION ADE::F-XOR))
 (25 1 (:DEFINITION ADE::F-XOR3))
 (24 24 (:TYPE-PRESCRIPTION ADE::3VP))
 (18 18 (:TYPE-PRESCRIPTION BOOLEANP))
 (18 2 (:REWRITE ADE::LEN-FV-ADDER))
 (17 9 (:REWRITE DEFAULT-+-2))
 (12 2 (:REWRITE ADE::FV-ADDER=V-ADDER))
 (10 10 (:TYPE-PRESCRIPTION ADE::FV-ADDER))
 (10 9 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 6 (:REWRITE DEFAULT-<-2))
 (9 6 (:REWRITE DEFAULT-<-1))
 (8 7 (:REWRITE DEFAULT-CAR))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (8 1 (:REWRITE ZP-OPEN))
 (6 3 (:DEFINITION ADE::F-NOT))
 (6 2 (:REWRITE TAKE-WHEN-ATOM))
 (4 2 (:DEFINITION ADE::F-AND))
 (4 1 (:DEFINITION ADE::F-OR))
 (3 1 (:DEFINITION NOT))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 )
(ADE::V-THREEFIX-FV-ADDER-OUTPUT
 (570 10 (:DEFINITION TAKE))
 (350 20 (:REWRITE TAKE-OF-TOO-MANY))
 (287 24 (:REWRITE TAKE-OF-LEN-FREE))
 (212 70 (:REWRITE ADE::F-GATES=B-GATES))
 (124 124 (:TYPE-PRESCRIPTION BOOLEANP))
 (122 66 (:REWRITE DEFAULT-+-2))
 (116 116 (:TYPE-PRESCRIPTION ADE::FV-ADDER))
 (112 14 (:REWRITE ZP-OPEN))
 (92 13 (:REWRITE ADE::LEN-FV-ADDER))
 (91 65 (:REWRITE DEFAULT-CDR))
 (88 54 (:REWRITE DEFAULT-<-2))
 (85 10 (:REWRITE ADE::V-THREEFIX-BVP))
 (78 20 (:DEFINITION NFIX))
 (76 16 (:REWRITE ADE::FV-ADDER=V-ADDER))
 (74 57 (:REWRITE DEFAULT-CAR))
 (72 8 (:REWRITE CONSP-OF-TAKE))
 (66 66 (:REWRITE DEFAULT-+-1))
 (66 54 (:REWRITE DEFAULT-<-1))
 (60 20 (:REWRITE TAKE-WHEN-ATOM))
 (40 40 (:TYPE-PRESCRIPTION ADE::BVP))
 (40 10 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (28 4 (:REWRITE CAR-OF-TAKE))
 (24 12 (:DEFINITION ADE::F-AND))
 (24 6 (:DEFINITION ADE::F-OR))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (15 5 (:REWRITE ADE::BVP-TAKE))
 )
(ADE::FV-ADDER-OUTPUT-OF-F-BUF-CANCELED
 (1158 60 (:REWRITE TAKE-OF-LEN-FREE))
 (1158 56 (:REWRITE TAKE-OF-TOO-MANY))
 (931 335 (:REWRITE ADE::F-GATES=B-GATES))
 (412 220 (:REWRITE DEFAULT-+-2))
 (388 52 (:REWRITE ADE::LEN-FV-ADDER))
 (339 60 (:REWRITE ADE::FV-ADDER=V-ADDER))
 (330 298 (:REWRITE DEFAULT-CAR))
 (298 262 (:REWRITE DEFAULT-CDR))
 (288 288 (:TYPE-PRESCRIPTION ADE::FV-ADDER))
 (228 52 (:DEFINITION NFIX))
 (220 220 (:REWRITE DEFAULT-+-1))
 (212 132 (:REWRITE DEFAULT-<-2))
 (180 132 (:REWRITE DEFAULT-<-1))
 (168 56 (:REWRITE TAKE-WHEN-ATOM))
 (114 76 (:TYPE-PRESCRIPTION ADE::3V-FIX))
 (70 70 (:TYPE-PRESCRIPTION ADE::F-OR))
 (54 13 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (52 52 (:TYPE-PRESCRIPTION NFIX))
 (35 13 (:REWRITE ADE::F-BUF-OF-3VP))
 (9 3 (:REWRITE ADE::3V-FIX-IDEMPOTENT))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 )
(ADE::FV-ADDER-OUTPUT-OF-V-THREEFIX-CANCELED-1
 (148 2 (:DEFINITION ADE::FV-ADDER))
 (114 2 (:DEFINITION TAKE))
 (92 4 (:REWRITE TAKE-OF-TOO-MANY))
 (90 90 (:TYPE-PRESCRIPTION LEN))
 (66 4 (:REWRITE TAKE-OF-LEN-FREE))
 (60 20 (:REWRITE ADE::F-GATES=B-GATES))
 (58 10 (:DEFINITION LEN))
 (54 6 (:DEFINITION ADE::F-XOR))
 (50 2 (:DEFINITION ADE::F-XOR3))
 (49 49 (:TYPE-PRESCRIPTION ADE::3VP))
 (36 36 (:TYPE-PRESCRIPTION BOOLEANP))
 (36 4 (:REWRITE ADE::LEN-FV-ADDER))
 (30 16 (:REWRITE DEFAULT-+-2))
 (25 5 (:REWRITE ADE::FV-ADDER=V-ADDER))
 (20 20 (:TYPE-PRESCRIPTION ADE::FV-ADDER))
 (19 17 (:REWRITE DEFAULT-CDR))
 (18 9 (:DEFINITION ADE::3V-FIX))
 (18 4 (:DEFINITION NFIX))
 (17 15 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE DEFAULT-+-1))
 (16 10 (:REWRITE DEFAULT-<-2))
 (16 2 (:REWRITE ZP-OPEN))
 (14 10 (:REWRITE DEFAULT-<-1))
 (12 6 (:DEFINITION ADE::F-NOT))
 (12 4 (:REWRITE TAKE-WHEN-ATOM))
 (8 4 (:DEFINITION ADE::F-AND))
 (8 2 (:DEFINITION ADE::F-OR))
 (8 1 (:DEFINITION ADE::V-THREEFIX))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (6 2 (:DEFINITION NOT))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 )
(ADE::FV-ADDER-OUTPUT-OF-V-THREEFIX-CANCELED-2
 (114 2 (:DEFINITION TAKE))
 (108 2 (:DEFINITION ADE::FV-ADDER))
 (92 4 (:REWRITE TAKE-OF-TOO-MANY))
 (90 90 (:TYPE-PRESCRIPTION LEN))
 (66 4 (:REWRITE TAKE-OF-LEN-FREE))
 (58 10 (:DEFINITION LEN))
 (48 20 (:REWRITE ADE::F-GATES=B-GATES))
 (42 6 (:DEFINITION ADE::F-XOR))
 (38 2 (:DEFINITION ADE::F-XOR3))
 (36 36 (:TYPE-PRESCRIPTION BOOLEANP))
 (36 4 (:REWRITE ADE::LEN-FV-ADDER))
 (30 16 (:REWRITE DEFAULT-+-2))
 (20 20 (:TYPE-PRESCRIPTION ADE::FV-ADDER))
 (19 17 (:REWRITE DEFAULT-CDR))
 (18 9 (:DEFINITION ADE::3V-FIX))
 (18 4 (:DEFINITION NFIX))
 (17 15 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE DEFAULT-+-1))
 (16 10 (:REWRITE DEFAULT-<-2))
 (16 2 (:REWRITE ZP-OPEN))
 (14 10 (:REWRITE DEFAULT-<-1))
 (13 5 (:REWRITE ADE::FV-ADDER=V-ADDER))
 (12 4 (:REWRITE TAKE-WHEN-ATOM))
 (9 9 (:DEFINITION ADE::3VP))
 (8 1 (:DEFINITION ADE::V-THREEFIX))
 (6 6 (:DEFINITION ADE::F-NOT))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (6 2 (:DEFINITION NOT))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:DEFINITION ADE::F-AND))
 (2 2 (:DEFINITION ADE::F-OR))
 )
(ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT
 (114 2 (:DEFINITION TAKE))
 (92 4 (:REWRITE TAKE-OF-TOO-MANY))
 (90 90 (:TYPE-PRESCRIPTION LEN))
 (66 4 (:REWRITE TAKE-OF-LEN-FREE))
 (58 10 (:DEFINITION LEN))
 (36 4 (:REWRITE ADE::LEN-OF-V-ADDER))
 (30 16 (:REWRITE DEFAULT-+-2))
 (20 20 (:TYPE-PRESCRIPTION ADE::V-ADDER))
 (18 4 (:DEFINITION NFIX))
 (16 16 (:REWRITE DEFAULT-+-1))
 (16 10 (:REWRITE DEFAULT-<-2))
 (16 2 (:REWRITE ZP-OPEN))
 (14 12 (:REWRITE DEFAULT-CDR))
 (14 10 (:REWRITE DEFAULT-<-1))
 (12 4 (:REWRITE TAKE-WHEN-ATOM))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 2 (:REWRITE DEFAULT-CAR))
 )