File: piso2-sreg%40useless-runes.lsp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
links: PTS
area: main
in suites: trixie
size: 1,111,420 kB
sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (2896 lines) | stat: -rw-r--r-- 119,928 bytes
parent folder | download | duplicates (2)
(ADE::PISO2-SREG$DATA-INS-LEN
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-SUMS-<))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::PISO2-SREG$INS-LEN)
(ADE::PISO2-SREG*)
(ADE::PISO2-SREG*$DESTRUCTURE
 (1680 60 (:DEFINITION BINARY-APPEND))
 (1482 48 (:REWRITE ZP-OPEN))
 (1278 42 (:REWRITE CONSP-OF-REPEAT))
 (822 120 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (774 102 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (382 70 (:REWRITE DEFAULT-CDR))
 (377 65 (:REWRITE DEFAULT-CAR))
 (288 48 (:REWRITE |(+ c (+ d x))|))
 (282 12 (:REWRITE REPEAT-WHEN-ZP))
 (276 48 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (270 270 (:TYPE-PRESCRIPTION POSP))
 (108 108 (:TYPE-PRESCRIPTION REPEAT))
 (102 102 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (102 102 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (102 102 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (102 102 (:REWRITE |(< d (+ c x))|))
 (102 102 (:REWRITE |(< (- x) (- y))|))
 (96 96 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (96 96 (:REWRITE NORMALIZE-ADDENDS))
 (96 96 (:REWRITE DEFAULT-+-2))
 (96 96 (:REWRITE DEFAULT-+-1))
 (96 42 (:DEFINITION NOT))
 (72 72 (:REWRITE |(+ 0 x)|))
 (60 60 (:META META-INTEGERP-CORRECT))
 (60 36 (:REWRITE REDUCE-INTEGERP-+))
 (54 54 (:REWRITE SIMPLIFY-SUMS-<))
 (54 54 (:REWRITE DEFAULT-<-2))
 (54 54 (:REWRITE DEFAULT-<-1))
 (48 48 (:REWRITE |(< 0 (- x))|))
 (36 36 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 )
(ADE::NOT-PRIMP-PISO2-SREG
 (72 36 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (72 36 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (72 36 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 36 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::PISO2-SREG$NETLIST)
(ADE::PISO2-SREG&)
(ADE::CHECK-PISO2-SREG$NETLIST-64-7)
(ADE::PISO2-SREG$ST-FORMAT)
(ADE::PISO2-SREG$ST-FORMAT=>CONSTRAINT
 (56 8 (:DEFINITION LEN))
 (16 16 (:REWRITE NTH-WHEN-PREFIXP))
 (16 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (16 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (16 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE NORMALIZE-ADDENDS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-+-1))
 (8 8 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:REWRITE SIMPLIFY-SUMS-<))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (3 3 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::PISO2-SREG$VALID-ST
 (6 6 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE))
 )
(ADE::EXPT-LINEAR-LOWER-<=-INSTANCE
 (2 2 (:REWRITE DEFAULT-EXPT-2))
 (2 2 (:REWRITE DEFAULT-EXPT-1))
 (2 2 (:REWRITE |(expt x (- n))|))
 (2 2 (:REWRITE |(expt 2^i n)|))
 (2 2 (:REWRITE |(expt 1/c n)|))
 (2 2 (:REWRITE |(expt (- x) n)|))
 (2 2 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (1 1 (:LINEAR EXPT->-1-TWO))
 (1 1 (:LINEAR EXPT-<-1-TWO))
 (1 1 (:LINEAR EXPT-<-1-ONE))
 )
(ADE::PISO2-SREG$VALID-ST=>CONSTRAINT
 (4096 4096 (:LINEAR LEN-WHEN-PREFIXP))
 (2048 2048 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (268 257 (:REWRITE |(expt 2^i n)|))
 (257 257 (:REWRITE DEFAULT-EXPT-1))
 (257 257 (:REWRITE |(expt x (- n))|))
 (257 257 (:REWRITE |(expt 1/c n)|))
 (257 257 (:REWRITE |(expt (- x) n)|))
 (48 8 (:DEFINITION LEN))
 (41 33 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (41 33 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (41 33 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (33 33 (:REWRITE |(equal (- x) (- y))|))
 (32 32 (:REWRITE NTH-WHEN-PREFIXP))
 (18 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (10 10 (:REWRITE NORMALIZE-ADDENDS))
 (10 10 (:REWRITE DEFAULT-+-1))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(+ 0 x)|))
 )
(ADE::PISO2-SREG$VALID-ST=>ST-FORMAT
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 )
(ADE::PISO2-SREG$DATA0-IN
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-SUMS-<))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::LEN-PISO2-SREG$DATA0-IN)
(ADE::PISO2-SREG$DATA1-IN
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-SUMS-<))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::LEN-PISO2-SREG$DATA1-IN
 (116 2 (:REWRITE TAKE-OF-TOO-MANY))
 (82 1 (:DEFINITION TAKE))
 (38 4 (:DEFINITION LEN))
 (37 8 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (28 1 (:REWRITE ADE::LEN-NTHCDR))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (16 16 (:LINEAR LEN-WHEN-PREFIXP))
 (14 9 (:REWRITE DEFAULT-+-2))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 1 (:DEFINITION NTHCDR))
 (12 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 6 (:REWRITE DEFAULT-CDR))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 7 (:REWRITE SIMPLIFY-SUMS-<))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 7 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (8 8 (:REWRITE |(< (- x) (- y))|))
 (8 8 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (8 7 (:REWRITE DEFAULT-<-1))
 (7 2 (:REWRITE |(+ c (+ d x))|))
 (7 1 (:REWRITE DEFAULT-CAR))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5 1 (:REWRITE |(+ y x)|))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (3 2 (:REWRITE |(< d (+ c x))|))
 (2 2 (:TYPE-PRESCRIPTION TAKE))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE |(< (+ c x) d)|))
 (1 1 (:REWRITE |(+ 0 x)|))
 )
(ADE::PISO2-SREG$IN-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (5 5 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::PISO2-SREG$IN-ACT-INACTIVE
 (44 12 (:REWRITE ADE::F-GATES=B-GATES))
 (21 21 (:REWRITE NTH-WHEN-PREFIXP))
 (20 20 (:TYPE-PRESCRIPTION BOOLEANP))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:REWRITE DEFAULT-CAR))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (9 9 (:TYPE-PRESCRIPTION ADE::F-AND))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 2 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-OR))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::PISO2-SREG$OUT0-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (5 5 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::PISO2-SREG$OUT0-ACT-INACTIVE
 (18 4 (:REWRITE ADE::F-GATES=B-GATES))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-OR))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::PISO2-SREG$OUT1-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (5 5 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::PISO2-SREG$OUT1-ACT-INACTIVE
 (18 4 (:REWRITE ADE::F-GATES=B-GATES))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-OR))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::BOOLEANP-F$FAST-ZERO
 (234 2 (:REWRITE TAKE-OF-TOO-MANY))
 (180 2 (:REWRITE ADE::BTR-OR-NOR-IS-V-ZP-NZP))
 (143 1 (:DEFINITION TAKE))
 (116 2 (:REWRITE |(< (if a b c) x)|))
 (100 9 (:REWRITE |(< (+ c x) d)|))
 (79 18 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (79 3 (:DEFINITION NATP))
 (59 1 (:REWRITE ADE::TREE-SIZE-ATOM))
 (58 2 (:REWRITE ZP-OPEN))
 (57 3 (:REWRITE ADE::NFIX-OF-NAT))
 (56 1 (:REWRITE ADE::CONSP-MAKE-TREE))
 (52 3 (:DEFINITION NFIX))
 (49 7 (:DEFINITION LEN))
 (40 1 (:REWRITE ADE::TREE-SIZE-MAKE-TREE))
 (38 16 (:REWRITE SIMPLIFY-SUMS-<))
 (31 4 (:REWRITE |(< d (+ c x))|))
 (30 30 (:LINEAR LEN-WHEN-PREFIXP))
 (30 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (29 29 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (29 18 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (28 15 (:REWRITE DEFAULT-+-2))
 (27 1 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (25 25 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (22 1 (:REWRITE LEN-OF-TAKE))
 (21 17 (:REWRITE NORMALIZE-ADDENDS))
 (21 15 (:REWRITE DEFAULT-<-2))
 (20 20 (:TYPE-PRESCRIPTION ADE::TREE-SIZE))
 (20 15 (:REWRITE DEFAULT-<-1))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (17 4 (:REWRITE ADE::F-GATES=B-GATES))
 (15 15 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (15 15 (:REWRITE DEFAULT-+-1))
 (15 15 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (12 5 (:REWRITE |(+ c (+ d x))|))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 2 (:REWRITE |(+ y x)|))
 (7 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (5 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 1 (:REWRITE |(+ y (+ x z))|))
 (4 2 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (4 1 (:DEFINITION ADE::F-NOT))
 (3 3 (:REWRITE |(+ 0 x)|))
 (3 2 (:REWRITE |(equal (+ c x) d)|))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:TYPE-PRESCRIPTION ADE::MAKE-TREE))
 (2 2 (:REWRITE TAKE-WHEN-ATOM))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE |(+ x (- x))|))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE
 (27246 27246 (:REWRITE NTH-WHEN-PREFIXP))
 (15266 1030 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (10857 517 (:DEFINITION NTHCDR))
 (10839 5668 (:REWRITE DEFAULT-+-2))
 (5668 5668 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (5668 5668 (:REWRITE NORMALIZE-ADDENDS))
 (5668 5668 (:REWRITE DEFAULT-+-1))
 (4406 4406 (:TYPE-PRESCRIPTION LEN))
 (4133 4133 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4133 4133 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4133 4133 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4133 4133 (:REWRITE |(equal (- x) (- y))|))
 (3626 518 (:REWRITE ADE::LEN-STRIP-CARS))
 (3610 3599 (:REWRITE |(expt 2^i n)|))
 (3599 3599 (:REWRITE DEFAULT-EXPT-1))
 (3599 3599 (:REWRITE |(expt x (- n))|))
 (3599 3599 (:REWRITE |(expt 1/c n)|))
 (3599 3599 (:REWRITE |(expt (- x) n)|))
 (3108 518 (:DEFINITION LEN))
 (2048 1024 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (1036 1036 (:LINEAR LEN-WHEN-PREFIXP))
 (1036 518 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1036 518 (:REWRITE DEFAULT-<-1))
 (1024 512 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (908 518 (:REWRITE SIMPLIFY-SUMS-<))
 (908 518 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (518 518 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (518 518 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (518 518 (:REWRITE DEFAULT-<-2))
 (518 518 (:REWRITE |(< (- x) (- y))|))
 (518 518 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (12 4 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (12 4 (:REWRITE ADE::F-BUF-OF-3VP))
 (12 2 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (8 8 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::PISO2-SREG$BIT0-OUT
 (12 5 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::BOOLEANP-PISO2-SREG$BIT0-OUT
 (5528 5528 (:REWRITE NTH-WHEN-PREFIXP))
 (2688 128 (:DEFINITION NTHCDR))
 (2562 1346 (:REWRITE DEFAULT-+-2))
 (1920 128 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (1346 1346 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1346 1346 (:REWRITE NORMALIZE-ADDENDS))
 (1346 1346 (:REWRITE DEFAULT-+-1))
 (1177 1177 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1177 1177 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1177 1177 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1177 1177 (:REWRITE |(equal (- x) (- y))|))
 (908 897 (:REWRITE |(expt 2^i n)|))
 (897 897 (:REWRITE DEFAULT-EXPT-1))
 (897 897 (:REWRITE |(expt x (- n))|))
 (897 897 (:REWRITE |(expt 1/c n)|))
 (897 897 (:REWRITE |(expt (- x) n)|))
 (768 128 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (576 576 (:TYPE-PRESCRIPTION LEN))
 (448 64 (:REWRITE ADE::LEN-STRIP-CARS))
 (384 384 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (384 64 (:DEFINITION LEN))
 (192 192 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (192 64 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (128 128 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (128 128 (:LINEAR LEN-WHEN-PREFIXP))
 (128 64 (:REWRITE SIMPLIFY-SUMS-<))
 (128 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (128 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (128 64 (:REWRITE DEFAULT-<-1))
 (96 32 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (96 32 (:REWRITE ADE::F-BUF-OF-3VP))
 (64 64 (:TYPE-PRESCRIPTION ADE::3VP))
 (64 64 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (64 64 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (64 64 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::PISO2-SREG$BIT1-OUT
 (12 5 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::BOOLEANP-PISO2-SREG$BIT1-OUT
 (5528 5528 (:REWRITE NTH-WHEN-PREFIXP))
 (2688 128 (:DEFINITION NTHCDR))
 (2562 1346 (:REWRITE DEFAULT-+-2))
 (1920 128 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (1346 1346 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1346 1346 (:REWRITE NORMALIZE-ADDENDS))
 (1346 1346 (:REWRITE DEFAULT-+-1))
 (1177 1177 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1177 1177 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1177 1177 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1177 1177 (:REWRITE |(equal (- x) (- y))|))
 (908 897 (:REWRITE |(expt 2^i n)|))
 (897 897 (:REWRITE DEFAULT-EXPT-1))
 (897 897 (:REWRITE |(expt x (- n))|))
 (897 897 (:REWRITE |(expt 1/c n)|))
 (897 897 (:REWRITE |(expt (- x) n)|))
 (768 128 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (576 576 (:TYPE-PRESCRIPTION LEN))
 (448 64 (:REWRITE ADE::LEN-STRIP-CARS))
 (384 384 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (384 64 (:DEFINITION LEN))
 (192 192 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (192 64 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (128 128 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (128 128 (:LINEAR LEN-WHEN-PREFIXP))
 (128 64 (:REWRITE SIMPLIFY-SUMS-<))
 (128 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (128 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (128 64 (:REWRITE DEFAULT-<-1))
 (96 32 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (96 32 (:REWRITE ADE::F-BUF-OF-3VP))
 (64 64 (:TYPE-PRESCRIPTION ADE::3VP))
 (64 64 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (64 64 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (64 64 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::PISO2-SREG$OUTPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$BIT1-OUT))
 (1 1 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$BIT0-OUT))
 )
(ADE::PISO2-SREG$VALUE
 (3799 2111 (:REWRITE DEFAULT-+-2))
 (2562 590 (:REWRITE ADE::CAR-V-THREEFIX))
 (2111 2111 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2111 2111 (:REWRITE DEFAULT-+-1))
 (1794 102 (:REWRITE CAR-OF-APPEND))
 (1599 123 (:REWRITE CONSP-OF-REPEAT))
 (1488 124 (:REWRITE ZP-OPEN))
 (1180 590 (:DEFINITION ADE::3V-FIX))
 (1162 58 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (1154 128 (:REWRITE |(< d (+ c x))|))
 (693 290 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (676 652 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (660 44 (:REWRITE CAR-OF-TAKE))
 (634 634 (:TYPE-PRESCRIPTION ADE::3VP))
 (616 104 (:REWRITE ADE::DISJOINT-ATOM))
 (561 284 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (547 290 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (481 419 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (463 419 (:REWRITE ADE::F-BUF-OF-3VP))
 (440 44 (:REWRITE |(< (+ c x) d)|))
 (406 32 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (357 357 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (357 357 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (290 290 (:REWRITE |(equal (- x) (- y))|))
 (267 255 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (266 2 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (263 250 (:REWRITE REPEAT-WHEN-ZP))
 (233 233 (:REWRITE NTH-WHEN-PREFIXP))
 (232 185 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (185 185 (:REWRITE |(< (- x) (- y))|))
 (184 183 (:REWRITE SIMPLIFY-SUMS-<))
 (184 183 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (184 183 (:REWRITE DEFAULT-<-2))
 (183 183 (:REWRITE DEFAULT-<-1))
 (168 2 (:REWRITE PREFIXP-OF-APPEND-ARG2))
 (162 78 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (156 156 (:TYPE-PRESCRIPTION PAIRLIS$))
 (152 98 (:REWRITE TAKE-WHEN-ATOM))
 (146 2 (:DEFINITION SUBSETP-EQUAL))
 (120 10 (:DEFINITION ATOM))
 (118 78 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (98 78 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (90 74 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (76 72 (:REWRITE ADE::FV-NOT=V-NOT))
 (56 6 (:REWRITE ADE::DISJOINT-CONS))
 (54 2 (:DEFINITION MEMBER-EQUAL))
 (52 4 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (44 44 (:TYPE-PRESCRIPTION POSP))
 (44 44 (:TYPE-PRESCRIPTION NFIX))
 (44 20 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (40 8 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (38 38 (:LINEAR LEN-WHEN-PREFIXP))
 (36 12 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (32 8 (:REWRITE |(+ x x)|))
 (30 18 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (28 28 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (28 28 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (28 28 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (28 28 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (26 14 (:REWRITE |(equal (+ c x) d)|))
 (24 24 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (20 20 (:TYPE-PRESCRIPTION TAKE))
 (19 19 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (18 6 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (16 8 (:REWRITE ADE::BVP-TAKE))
 (16 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (15 1 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (12 4 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (12 3 (:DEFINITION TRUE-LISTP))
 (12 1 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (11 11 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (11 11 (:REWRITE DEFAULT-*-2))
 (11 11 (:REWRITE DEFAULT-*-1))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 2 (:REWRITE |(+ y (+ x z))|))
 (8 4 (:REWRITE |(* y x)|))
 (6 6 (:TYPE-PRESCRIPTION ATOM))
 (5 1 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (4 4 (:REWRITE ADE::T-OR-NOR$VALUE))
 (4 4 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 (4 4 (:REWRITE |(* a (/ a))|))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (3 3 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (2 2 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::PISO2-SREG$STEP
 (24 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (12 12 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::LEN-CDR
 (14 7 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE SIMPLIFY-SUMS-<))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::PISO2-SREG$STATE
 (9598 5416 (:REWRITE DEFAULT-+-2))
 (5416 5416 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (5416 5416 (:REWRITE DEFAULT-+-1))
 (5154 1566 (:REWRITE ADE::CAR-V-THREEFIX))
 (4433 341 (:REWRITE CONSP-OF-REPEAT))
 (4286 4258 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (4104 342 (:REWRITE ZP-OPEN))
 (3402 318 (:REWRITE CAR-OF-APPEND))
 (3322 166 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3165 353 (:REWRITE |(< d (+ c x))|))
 (3132 1566 (:DEFINITION ADE::3V-FIX))
 (1626 1626 (:TYPE-PRESCRIPTION ADE::3VP))
 (1546 1468 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (1528 1468 (:REWRITE ADE::F-BUF-OF-3VP))
 (1289 678 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1272 214 (:REWRITE ADE::DISJOINT-ATOM))
 (1257 674 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1252 908 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (1201 678 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1035 1022 (:REWRITE REPEAT-WHEN-ZP))
 (950 950 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (872 6 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (763 598 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (729 729 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (729 729 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (678 678 (:REWRITE |(equal (- x) (- y))|))
 (421 421 (:REWRITE NTH-WHEN-PREFIXP))
 (412 388 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (412 373 (:REWRITE SIMPLIFY-SUMS-<))
 (394 386 (:REWRITE ADE::FV-NOT=V-NOT))
 (378 378 (:REWRITE |(< (- x) (- y))|))
 (374 373 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (372 371 (:REWRITE DEFAULT-<-2))
 (371 371 (:REWRITE DEFAULT-<-1))
 (268 188 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (237 76 (:REWRITE TAKE-WHEN-ATOM))
 (234 234 (:TYPE-PRESCRIPTION PAIRLIS$))
 (228 188 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (180 16 (:DEFINITION ATOM))
 (146 2 (:DEFINITION SUBSETP-EQUAL))
 (135 60 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (107 56 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (104 8 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (82 82 (:TYPE-PRESCRIPTION POSP))
 (80 80 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (80 80 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (80 80 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (80 80 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (68 17 (:REWRITE |(+ x x)|))
 (56 6 (:REWRITE ADE::DISJOINT-CONS))
 (54 54 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (54 2 (:DEFINITION MEMBER-EQUAL))
 (50 8 (:REWRITE |(+ y (+ x z))|))
 (33 13 (:REWRITE |(equal (+ c x) d)|))
 (32 32 (:TYPE-PRESCRIPTION TAKE))
 (30 14 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (30 10 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (24 24 (:REWRITE DEFAULT-UNARY-MINUS))
 (24 8 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (21 21 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (21 21 (:REWRITE DEFAULT-*-2))
 (21 21 (:REWRITE DEFAULT-*-1))
 (18 6 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (15 1 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (12 3 (:DEFINITION TRUE-LISTP))
 (12 1 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (10 10 (:TYPE-PRESCRIPTION ATOM))
 (10 10 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (10 10 (:REWRITE DEFAULT-UNARY-/))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (6 6 (:REWRITE |(< 0 (- x))|))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (5 3 (:REWRITE CONSP-OF-APPEND))
 (5 1 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (4 4 (:REWRITE ADE::T-OR-NOR$VALUE))
 (4 4 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (4 4 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 2 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::PISO2-SREG$INPUT-FORMAT)
(ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-4
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 14 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (14 14 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (14 2 (:DEFINITION LEN))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 2 (:DEFINITION BINARY-APPEND))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (9 1 (:DEFINITION TRUE-LISTP))
 (8 5 (:REWRITE SIMPLIFY-SUMS-<))
 (8 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 5 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (8 5 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (7 7 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (7 5 (:REWRITE DEFAULT-+-2))
 (6 6 (:REWRITE NTH-WHEN-PREFIXP))
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (5 5 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (5 5 (:REWRITE NORMALIZE-ADDENDS))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-+-1))
 (5 5 (:REWRITE |(< (- x) (- y))|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (4 2 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 1 (:REWRITE ADE::BVP-NTHCDR))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (1 1 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::BOOLEANP-PISO2-SREG$IN-ACT
 (16933 16933 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (16165 16165 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (13592 13592 (:REWRITE NTH-WHEN-PREFIXP))
 (10620 2073 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10620 2073 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10620 2073 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8320 512 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (5634 3074 (:REWRITE DEFAULT-+-2))
 (5376 256 (:DEFINITION NTHCDR))
 (3074 3074 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3074 3074 (:REWRITE NORMALIZE-ADDENDS))
 (3074 3074 (:REWRITE DEFAULT-+-1))
 (2560 256 (:REWRITE ADE::LEN-STRIP-CARS))
 (2304 256 (:DEFINITION LEN))
 (2176 2176 (:TYPE-PRESCRIPTION LEN))
 (2073 2073 (:REWRITE |(equal (- x) (- y))|))
 (2060 2049 (:REWRITE |(expt 2^i n)|))
 (2049 2049 (:REWRITE DEFAULT-EXPT-1))
 (2049 2049 (:REWRITE |(expt x (- n))|))
 (2049 2049 (:REWRITE |(expt 1/c n)|))
 (2049 2049 (:REWRITE |(expt (- x) n)|))
 (1536 1536 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (1024 512 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (1024 256 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (512 512 (:LINEAR LEN-WHEN-PREFIXP))
 (512 256 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (512 256 (:REWRITE DEFAULT-<-1))
 (448 256 (:REWRITE SIMPLIFY-SUMS-<))
 (448 256 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (256 256 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (256 256 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (256 256 (:REWRITE DEFAULT-<-2))
 (256 256 (:REWRITE |(< (- x) (- y))|))
 (256 256 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (5 1 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::BOOLEANP-PISO2-SREG$OUT0-ACT
 (177812 145482 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (16165 16165 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (11608 11608 (:REWRITE NTH-WHEN-PREFIXP))
 (10620 2073 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10620 2073 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10620 2073 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5378 2946 (:REWRITE DEFAULT-+-2))
 (5376 256 (:DEFINITION NTHCDR))
 (4352 256 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (2946 2946 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2946 2946 (:REWRITE NORMALIZE-ADDENDS))
 (2946 2946 (:REWRITE DEFAULT-+-1))
 (2073 2073 (:REWRITE |(equal (- x) (- y))|))
 (2060 2049 (:REWRITE |(expt 2^i n)|))
 (2049 2049 (:REWRITE DEFAULT-EXPT-1))
 (2049 2049 (:REWRITE |(expt x (- n))|))
 (2049 2049 (:REWRITE |(expt 1/c n)|))
 (2049 2049 (:REWRITE |(expt (- x) n)|))
 (1536 256 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (1408 128 (:REWRITE ADE::LEN-STRIP-CARS))
 (1280 128 (:DEFINITION LEN))
 (1152 1152 (:TYPE-PRESCRIPTION LEN))
 (768 768 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (384 384 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (384 128 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (256 256 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (256 256 (:LINEAR LEN-WHEN-PREFIXP))
 (256 128 (:REWRITE SIMPLIFY-SUMS-<))
 (256 128 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (256 128 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (256 128 (:REWRITE DEFAULT-<-1))
 (128 128 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (128 128 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (128 128 (:REWRITE DEFAULT-<-2))
 (128 128 (:REWRITE |(< (- x) (- y))|))
 (128 128 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (80 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::BOOLEANP-PISO2-SREG$OUT1-ACT
 (177812 145482 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (16421 16421 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (11608 11608 (:REWRITE NTH-WHEN-PREFIXP))
 (10620 2073 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10620 2073 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10620 2073 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5378 2946 (:REWRITE DEFAULT-+-2))
 (5376 256 (:DEFINITION NTHCDR))
 (4096 256 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (2946 2946 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2946 2946 (:REWRITE NORMALIZE-ADDENDS))
 (2946 2946 (:REWRITE DEFAULT-+-1))
 (2073 2073 (:REWRITE |(equal (- x) (- y))|))
 (2060 2049 (:REWRITE |(expt 2^i n)|))
 (2049 2049 (:REWRITE DEFAULT-EXPT-1))
 (2049 2049 (:REWRITE |(expt x (- n))|))
 (2049 2049 (:REWRITE |(expt 1/c n)|))
 (2049 2049 (:REWRITE |(expt (- x) n)|))
 (1536 256 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (1152 1152 (:TYPE-PRESCRIPTION LEN))
 (1152 128 (:REWRITE ADE::LEN-STRIP-CARS))
 (1024 128 (:DEFINITION LEN))
 (768 768 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (384 384 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (384 128 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (256 256 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (256 256 (:LINEAR LEN-WHEN-PREFIXP))
 (256 128 (:REWRITE SIMPLIFY-SUMS-<))
 (256 128 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (256 128 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (256 128 (:REWRITE DEFAULT-<-1))
 (128 128 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (128 128 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (128 128 (:REWRITE DEFAULT-<-2))
 (128 128 (:REWRITE |(< (- x) (- y))|))
 (128 128 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (80 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::PISO2-SREG$ST-FORMAT-PRESERVED
 (272 130 (:REWRITE DEFAULT-CAR))
 (264 8 (:DEFINITION BINARY-APPEND))
 (258 38 (:DEFINITION STRIP-CARS))
 (236 24 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (216 216 (:REWRITE NTH-WHEN-PREFIXP))
 (208 16 (:REWRITE ZP-OPEN))
 (196 14 (:REWRITE CONSP-OF-REPEAT))
 (190 164 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (165 89 (:REWRITE DEFAULT-CDR))
 (144 16 (:REWRITE |(< d (+ c x))|))
 (116 98 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (98 18 (:REWRITE ADE::F-GATES=B-GATES))
 (84 18 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (72 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (70 70 (:TYPE-PRESCRIPTION BOOLEANP))
 (69 49 (:REWRITE DEFAULT-+-2))
 (64 64 (:TYPE-PRESCRIPTION ADE::BVP))
 (60 6 (:DEFINITION ADE::V-THREEFIX))
 (54 54 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (49 49 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (49 49 (:REWRITE DEFAULT-+-1))
 (40 8 (:DEFINITION PAIRLIS$))
 (39 3 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (39 3 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (36 36 (:TYPE-PRESCRIPTION ADE::F-OR))
 (36 36 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (36 36 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (36 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (36 12 (:REWRITE ADE::V-THREEFIX-BVP))
 (36 8 (:REWRITE REPEAT-WHEN-ZP))
 (32 12 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (32 12 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (32 12 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (30 30 (:TYPE-PRESCRIPTION ADE::F-AND))
 (28 4 (:REWRITE ADE::CAR-V-THREEFIX))
 (20 20 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (20 20 (:REWRITE SIMPLIFY-SUMS-<))
 (20 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (20 20 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (20 20 (:REWRITE DEFAULT-<-2))
 (20 20 (:REWRITE DEFAULT-<-1))
 (20 20 (:REWRITE |(< (- x) (- y))|))
 (20 10 (:DEFINITION ADE::3V-FIX))
 (18 18 (:TYPE-PRESCRIPTION ADE::JOINT-ACT))
 (14 6 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (12 12 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (12 12 (:REWRITE |(equal (- x) (- y))|))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (12 4 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (12 4 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (11 5 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (10 10 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (10 10 (:TYPE-PRESCRIPTION ADE::3VP))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 4 (:REWRITE ADE::FV-NOT=V-NOT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN-ACT))
 (6 6 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (6 2 (:REWRITE ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (5 5 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (5 5 (:REWRITE DEFAULT-*-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::PISO2-SREG$VALUE-ALT
 (1704 24 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-4))
 (570 6 (:REWRITE CONS-EQUAL))
 (564 64 (:DEFINITION BINARY-APPEND))
 (559 43 (:DEFINITION NTHCDR))
 (473 43 (:REWRITE |(+ (+ x y) z)|))
 (420 15 (:REWRITE ADE::LEN-NTHCDR))
 (360 24 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (316 172 (:REWRITE DEFAULT-CDR))
 (278 128 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (232 88 (:REWRITE DEFAULT-CAR))
 (210 30 (:DEFINITION LEN))
 (207 177 (:REWRITE DEFAULT-+-2))
 (177 177 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (177 177 (:REWRITE DEFAULT-+-1))
 (158 158 (:REWRITE NTH-WHEN-PREFIXP))
 (143 22 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (117 11 (:DEFINITION TRUE-LISTP))
 (99 33 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (99 33 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (99 33 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (92 11 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (88 12 (:REWRITE CONSP-OF-APPEND))
 (84 11 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (52 52 (:LINEAR LEN-WHEN-PREFIXP))
 (44 22 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (43 43 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (43 43 (:REWRITE DEFAULT-*-2))
 (43 43 (:REWRITE DEFAULT-*-1))
 (33 33 (:REWRITE |(equal (- x) (- y))|))
 (33 11 (:REWRITE ADE::BVP-NTHCDR))
 (30 15 (:REWRITE SIMPLIFY-SUMS-<))
 (30 15 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (30 15 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (30 15 (:REWRITE DEFAULT-<-1))
 (26 26 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 24 (:REWRITE CDR-CONS))
 (24 24 (:REWRITE CAR-CONS))
 (22 22 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (15 15 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (15 15 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (15 15 (:REWRITE DEFAULT-<-2))
 (15 15 (:REWRITE |(< d (+ c x))|))
 (15 15 (:REWRITE |(< (- x) (- y))|))
 (12 12 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 8 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (8 8 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (3 3 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::PISO2-SREG$STATE-ALT
 (1704 24 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-4))
 (570 6 (:REWRITE CONS-EQUAL))
 (528 58 (:DEFINITION BINARY-APPEND))
 (520 40 (:DEFINITION NTHCDR))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (420 15 (:REWRITE ADE::LEN-NTHCDR))
 (360 24 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (307 163 (:REWRITE DEFAULT-CDR))
 (266 116 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (226 82 (:REWRITE DEFAULT-CAR))
 (210 30 (:DEFINITION LEN))
 (198 168 (:REWRITE DEFAULT-+-2))
 (168 168 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (168 168 (:REWRITE DEFAULT-+-1))
 (143 22 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (117 11 (:DEFINITION TRUE-LISTP))
 (99 33 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (99 33 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (99 33 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (93 93 (:REWRITE NTH-WHEN-PREFIXP))
 (88 12 (:REWRITE CONSP-OF-APPEND))
 (52 52 (:LINEAR LEN-WHEN-PREFIXP))
 (44 22 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (33 33 (:REWRITE |(equal (- x) (- y))|))
 (33 11 (:REWRITE ADE::BVP-NTHCDR))
 (30 15 (:REWRITE SIMPLIFY-SUMS-<))
 (30 15 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (30 15 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (30 15 (:REWRITE DEFAULT-<-1))
 (26 26 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 24 (:REWRITE CDR-CONS))
 (24 24 (:REWRITE CAR-CONS))
 (15 15 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (15 15 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (15 15 (:REWRITE DEFAULT-<-2))
 (15 15 (:REWRITE |(< d (+ c x))|))
 (15 15 (:REWRITE |(< (- x) (- y))|))
 (12 12 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 8 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (8 8 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (3 3 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::PISO2-SREG$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO2-SREG$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO2-SREG$RUN)
(ADE::PISO2-SREG$RUN-PLUS
 (349 25 (:REWRITE ZP-OPEN))
 (122 34 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (76 28 (:REWRITE |(< d (+ c x))|))
 (50 24 (:REWRITE |(+ c (+ d x))|))
 (41 41 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (34 34 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (34 34 (:REWRITE |(< (- x) (- y))|))
 (32 15 (:REWRITE DEFAULT-CDR))
 (27 10 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE SIMPLIFY-SUMS-<))
 (26 26 (:REWRITE DEFAULT-<-2))
 (26 26 (:REWRITE DEFAULT-<-1))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-2))
 (18 18 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE |(< d (+ c x y))|))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::PISO2-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 SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE SIMPLIFY-SUMS-<))
 (4 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (4 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:META META-INTEGERP-CORRECT))
 )
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO2-SREG$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-PISO2-SREG$INPUT-FORMAT-N)
(ADE::PISO2-SREG$INPUT-FORMAT-PLUS
 (87 39 (:REWRITE |(< d (+ c x))|))
 (56 56 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (47 47 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (47 47 (:REWRITE |(< (- x) (- y))|))
 (35 35 (:REWRITE SIMPLIFY-SUMS-<))
 (35 35 (:REWRITE DEFAULT-<-2))
 (35 35 (:REWRITE DEFAULT-<-1))
 (27 15 (:REWRITE DEFAULT-CDR))
 (27 15 (:REWRITE DEFAULT-CAR))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (22 22 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (22 22 (:REWRITE NORMALIZE-ADDENDS))
 (22 22 (:REWRITE DEFAULT-+-2))
 (22 22 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 12 (:REWRITE |(< d (+ c x y))|))
 (12 12 (:REWRITE |(< 0 (- x))|))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::PISO2-SREG$DE-N
 (265 30 (:REWRITE ZP-OPEN))
 (108 12 (:REWRITE |(< d (+ c x))|))
 (62 2 (:DEFINITION ADE::PISO2-SREG$RUN))
 (36 36 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (31 31 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (24 24 (:REWRITE SIMPLIFY-SUMS-<))
 (24 24 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (24 24 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE |(< (- x) (- y))|))
 (11 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (11 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (11 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::PISO2-SREG$OP)
(ADE::APPEND-OF-PISO2-SREG$OP-WITH-SINGLETON)
(ADE::PISO2-SREG$OP-MAP)
(ADE::PISO2-SREG$OP-MAP-OF-APPEND
 (80 80 (:TYPE-PRESCRIPTION ADE::PISO2-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))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::PISO2-SREG$EXTRACT0
 (30 30 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (12 12 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 )
(ADE::PISO2-SREG$EXTRACT1
 (24 24 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 )
(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))
 (19 19 (:REWRITE DEFAULT-CDR))
 (17 17 (:REWRITE ADE::NOT-V-NZP-TAKE-NTHCDR))
 (15 15 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (12 12 (:REWRITE DEFAULT-*-1))
 (12 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (12 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (12 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (11 6 (:REWRITE DEFAULT-+-2))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (6 6 (:REWRITE NORMALIZE-ADDENDS))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE |(equal (- x) 0)|))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (5 5 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 )
(ADE::PISO2-SREG$EXTRACT0-NOT-EMPTY
 (8834 7291 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (4820 3048 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (1550 695 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (1044 1044 (:LINEAR LEN-WHEN-PREFIXP))
 (880 880 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (777 777 (:REWRITE NTH-WHEN-PREFIXP))
 (695 695 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (682 399 (:REWRITE DEFAULT-+-2))
 (522 522 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (450 106 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (450 106 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (450 106 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (440 58 (:DEFINITION STRIP-CARS))
 (399 399 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (399 399 (:REWRITE NORMALIZE-ADDENDS))
 (399 399 (:REWRITE DEFAULT-+-1))
 (384 64 (:LINEAR EXPT-X->=-X))
 (384 64 (:LINEAR EXPT-X->-X))
 (384 64 (:LINEAR EXPT->-1-ONE))
 (376 310 (:REWRITE |(expt 2^i n)|))
 (367 361 (:REWRITE DEFAULT-CDR))
 (310 310 (:REWRITE DEFAULT-EXPT-1))
 (310 310 (:REWRITE |(expt x (- n))|))
 (310 310 (:REWRITE |(expt 1/c n)|))
 (310 310 (:REWRITE |(expt (- x) n)|))
 (254 4 (:REWRITE TAKE-OF-TOO-MANY))
 (248 2 (:DEFINITION TAKE))
 (242 20 (:DEFINITION NTHCDR))
 (213 23 (:REWRITE ADE::F-GATES=B-GATES))
 (210 132 (:REWRITE DEFAULT-CAR))
 (198 18 (:REWRITE |(+ (+ x y) z)|))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (128 128 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (106 106 (:REWRITE |(equal (- x) (- y))|))
 (94 30 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (94 20 (:REWRITE |(+ c (+ d x))|))
 (90 18 (:REWRITE |(+ y x)|))
 (68 34 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT0-ACT))
 (64 64 (:LINEAR EXPT->-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-ONE))
 (62 2 (:REWRITE ADE::LEN-CDR))
 (60 12 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (40 40 (:TYPE-PRESCRIPTION STRIP-CARS))
 (40 30 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (38 38 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (38 2 (:REWRITE ZP-OPEN))
 (38 2 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (36 28 (:REWRITE SIMPLIFY-SUMS-<))
 (36 28 (:REWRITE DEFAULT-<-2))
 (36 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (30 30 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (30 30 (:REWRITE |(< (- x) (- y))|))
 (30 28 (:REWRITE DEFAULT-<-1))
 (28 28 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (28 2 (:DEFINITION NATP))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (20 20 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (20 20 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (20 20 (:REWRITE |(equal (- x) 0)|))
 (20 20 (:REWRITE |(< (- x) 0)|))
 (18 18 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (18 18 (:REWRITE DEFAULT-*-2))
 (18 18 (:REWRITE DEFAULT-*-1))
 (18 18 (:META META-INTEGERP-CORRECT))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (14 2 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (12 12 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 4 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (8 8 (:REWRITE |(+ 0 x)|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (4 4 (:TYPE-PRESCRIPTION TAKE))
 (4 4 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN-ACT))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 2 (:REWRITE |(< d (+ c x))|))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 )
(ADE::PISO2-SREG$EXTRACT1-NOT-EMPTY
 (8575 7083 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (3789 2239 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (1734 1522 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (1550 695 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (1044 1044 (:LINEAR LEN-WHEN-PREFIXP))
 (777 777 (:REWRITE NTH-WHEN-PREFIXP))
 (695 695 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (682 399 (:REWRITE DEFAULT-+-2))
 (522 522 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (402 106 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (402 106 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (402 106 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (399 399 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (399 399 (:REWRITE NORMALIZE-ADDENDS))
 (399 399 (:REWRITE DEFAULT-+-1))
 (384 64 (:LINEAR EXPT-X->=-X))
 (384 64 (:LINEAR EXPT-X->-X))
 (384 64 (:LINEAR EXPT->-1-ONE))
 (376 310 (:REWRITE |(expt 2^i n)|))
 (367 361 (:REWRITE DEFAULT-CDR))
 (360 58 (:DEFINITION STRIP-CARS))
 (310 310 (:REWRITE DEFAULT-EXPT-1))
 (310 310 (:REWRITE |(expt x (- n))|))
 (310 310 (:REWRITE |(expt 1/c n)|))
 (310 310 (:REWRITE |(expt (- x) n)|))
 (246 4 (:REWRITE TAKE-OF-TOO-MANY))
 (244 2 (:DEFINITION TAKE))
 (242 20 (:DEFINITION NTHCDR))
 (198 18 (:REWRITE |(+ (+ x y) z)|))
 (180 132 (:REWRITE DEFAULT-CAR))
 (180 23 (:REWRITE ADE::F-GATES=B-GATES))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (128 128 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (106 106 (:REWRITE |(equal (- x) (- y))|))
 (94 30 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (94 20 (:REWRITE |(+ c (+ d x))|))
 (90 18 (:REWRITE |(+ y x)|))
 (68 34 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT1-ACT))
 (64 64 (:LINEAR EXPT->-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-ONE))
 (60 12 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (58 2 (:REWRITE ADE::LEN-CDR))
 (40 40 (:TYPE-PRESCRIPTION STRIP-CARS))
 (40 30 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (38 38 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (38 2 (:REWRITE ZP-OPEN))
 (38 2 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (36 28 (:REWRITE SIMPLIFY-SUMS-<))
 (36 28 (:REWRITE DEFAULT-<-2))
 (36 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (30 30 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (30 30 (:REWRITE |(< (- x) (- y))|))
 (30 28 (:REWRITE DEFAULT-<-1))
 (28 28 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (28 2 (:DEFINITION NATP))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (20 20 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (20 20 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (20 20 (:REWRITE |(equal (- x) 0)|))
 (20 20 (:REWRITE |(< (- x) 0)|))
 (18 18 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (18 18 (:REWRITE DEFAULT-*-2))
 (18 18 (:REWRITE DEFAULT-*-1))
 (18 18 (:META META-INTEGERP-CORRECT))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (14 2 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (12 12 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 4 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (8 8 (:REWRITE |(+ 0 x)|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (4 4 (:TYPE-PRESCRIPTION TAKE))
 (4 4 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN-ACT))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 2 (:REWRITE |(< d (+ c x))|))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 )
(ADE::LENS-OF-PISO2-SREG$EXTRACTS-LEMMA
 (13030 9235 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (1945 859 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (1445 1369 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (949 949 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (859 859 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (533 533 (:REWRITE NTH-WHEN-PREFIXP))
 (412 102 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (410 102 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (410 102 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (312 172 (:REWRITE DEFAULT-+-2))
 (306 44 (:DEFINITION STRIP-CARS))
 (277 7 (:REWRITE TAKE-OF-TOO-MANY))
 (258 3 (:DEFINITION TAKE))
 (223 115 (:REWRITE DEFAULT-CAR))
 (182 173 (:REWRITE DEFAULT-CDR))
 (172 172 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (172 172 (:REWRITE NORMALIZE-ADDENDS))
 (172 172 (:REWRITE DEFAULT-+-1))
 (164 164 (:LINEAR LEN-WHEN-PREFIXP))
 (130 66 (:REWRITE |(expt 2^i n)|))
 (102 102 (:REWRITE |(equal (- x) (- y))|))
 (82 82 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (82 3 (:REWRITE ADE::LEN-CDR))
 (66 66 (:REWRITE DEFAULT-EXPT-1))
 (66 66 (:REWRITE |(expt x (- n))|))
 (66 66 (:REWRITE |(expt 1/c n)|))
 (66 66 (:REWRITE |(expt (- x) n)|))
 (60 17 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (58 6 (:DEFINITION NTHCDR))
 (54 9 (:LINEAR EXPT-X->=-X))
 (54 9 (:LINEAR EXPT-X->-X))
 (54 9 (:LINEAR EXPT->-1-ONE))
 (44 4 (:REWRITE |(+ (+ x y) z)|))
 (40 8 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (39 39 (:TYPE-PRESCRIPTION STRIP-CARS))
 (38 2 (:REWRITE ZP-OPEN))
 (32 10 (:REWRITE |(+ c (+ d x))|))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (28 7 (:REWRITE TAKE-WHEN-ATOM))
 (21 17 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (20 4 (:REWRITE |(+ y x)|))
 (18 18 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (18 18 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (18 18 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (18 18 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (18 14 (:REWRITE SIMPLIFY-SUMS-<))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (17 17 (:REWRITE |(< (- x) (- y))|))
 (16 14 (:REWRITE DEFAULT-<-2))
 (16 14 (:REWRITE DEFAULT-<-1))
 (14 14 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:META META-INTEGERP-CORRECT))
 (10 10 (:REWRITE |(+ 0 x)|))
 (9 9 (:LINEAR EXPT->-1-TWO))
 (9 9 (:LINEAR EXPT-<-1-TWO))
 (9 9 (:LINEAR EXPT-<-1-ONE))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (7 7 (:TYPE-PRESCRIPTION NFIX))
 (7 7 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (7 7 (:REWRITE |(equal (- x) 0)|))
 (6 6 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (5 5 (:REWRITE |(< (- x) 0)|))
 (5 5 (:LINEAR ADE::PISO2-SREG$EXTRACT1-NOT-EMPTY))
 (5 5 (:LINEAR ADE::PISO2-SREG$EXTRACT0-NOT-EMPTY))
 (4 4 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (4 4 (:REWRITE DEFAULT-*-2))
 (4 4 (:REWRITE DEFAULT-*-1))
 (4 1 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (3 3 (:REWRITE |(< d (+ c x))|))
 (3 3 (:REWRITE |(< 0 (- x))|))
 (3 3 (:REWRITE |(< (+ d x) (+ c y))|))
 (3 3 (:REWRITE |(< (+ c x) d)|))
 (3 3 (:REWRITE |(< (+ c x) (+ d y))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1
 (3593 2683 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (1500 24 (:REWRITE TAKE-OF-TOO-MANY))
 (1468 12 (:DEFINITION TAKE))
 (748 650 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (591 139 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (591 139 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (591 139 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (496 73 (:DEFINITION STRIP-CARS))
 (469 469 (:REWRITE NTH-WHEN-PREFIXP))
 (469 76 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (429 204 (:REWRITE DEFAULT-CAR))
 (390 185 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (360 12 (:REWRITE ADE::LEN-CDR))
 (308 184 (:REWRITE DEFAULT-+-2))
 (306 306 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (241 205 (:REWRITE DEFAULT-CDR))
 (228 228 (:LINEAR LEN-WHEN-PREFIXP))
 (220 12 (:REWRITE ZP-OPEN))
 (185 185 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (184 184 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (184 184 (:REWRITE NORMALIZE-ADDENDS))
 (184 184 (:REWRITE DEFAULT-+-1))
 (182 50 (:REWRITE |(expt 2^i n)|))
 (168 168 (:TYPE-PRESCRIPTION STRIP-CARS))
 (139 139 (:REWRITE |(equal (- x) (- y))|))
 (139 76 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (121 64 (:REWRITE DEFAULT-<-2))
 (120 24 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (115 64 (:REWRITE SIMPLIFY-SUMS-<))
 (114 114 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (96 24 (:REWRITE TAKE-WHEN-ATOM))
 (84 8 (:DEFINITION NTHCDR))
 (76 76 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (76 76 (:REWRITE |(< (- x) (- y))|))
 (76 64 (:REWRITE DEFAULT-<-1))
 (66 6 (:REWRITE |(+ (+ x y) z)|))
 (64 64 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (54 18 (:REWRITE |(+ c (+ d x))|))
 (50 50 (:REWRITE DEFAULT-EXPT-1))
 (50 50 (:REWRITE |(expt x (- n))|))
 (50 50 (:REWRITE |(expt 1/c n)|))
 (50 50 (:REWRITE |(expt (- x) n)|))
 (48 8 (:LINEAR EXPT-X->=-X))
 (48 8 (:LINEAR EXPT-X->-X))
 (48 8 (:LINEAR EXPT->-1-ONE))
 (33 33 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (33 33 (:REWRITE |(< 0 (- x))|))
 (31 31 (:META META-INTEGERP-CORRECT))
 (30 6 (:REWRITE |(+ y x)|))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (24 24 (:TYPE-PRESCRIPTION TAKE))
 (24 24 (:REWRITE |(+ 0 x)|))
 (24 12 (:REWRITE |(< d (+ c x))|))
 (19 19 (:REWRITE REDUCE-INTEGERP-+))
 (19 19 (:REWRITE INTEGERP-MINUS-X))
 (16 16 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (16 16 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (16 16 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (16 16 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (14 14 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:REWRITE |(< (+ c x) d)|))
 (8 8 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (8 8 (:LINEAR EXPT->-1-TWO))
 (8 8 (:LINEAR EXPT-<-1-TWO))
 (8 8 (:LINEAR EXPT-<-1-ONE))
 (7 7 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (7 7 (:REWRITE |(< (- x) 0)|))
 (6 6 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (6 6 (:REWRITE DEFAULT-*-2))
 (6 6 (:REWRITE DEFAULT-*-1))
 (4 1 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:LINEAR ADE::PISO2-SREG$EXTRACT1-NOT-EMPTY))
 (1 1 (:LINEAR ADE::PISO2-SREG$EXTRACT0-NOT-EMPTY))
 )
(ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2
 (30 15 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (15 15 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 )
(ADE::PISO2-SREG$INV
 (54 54 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (54 54 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 )
(ADE::LENS-OF-PISO2-SREG$EXTRACTS-UPPER-BOUND
 (562322 460840 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (97219 88871 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (61560 61560 (:REWRITE NTH-WHEN-PREFIXP))
 (54915 54915 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (36864 36864 (:LINEAR LEN-WHEN-PREFIXP))
 (34050 17034 (:REWRITE DEFAULT-+-2))
 (32396 7713 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (32396 7713 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (32396 7713 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (18432 18432 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (17034 17034 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (17034 17034 (:REWRITE NORMALIZE-ADDENDS))
 (17034 17034 (:REWRITE DEFAULT-+-1))
 (13340 10761 (:REWRITE |(expt 2^i n)|))
 (10761 10761 (:REWRITE DEFAULT-EXPT-1))
 (10761 10761 (:REWRITE |(expt x (- n))|))
 (10761 10761 (:REWRITE |(expt 1/c n)|))
 (10761 10761 (:REWRITE |(expt (- x) n)|))
 (7713 7713 (:REWRITE |(equal (- x) (- y))|))
 (4096 4096 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (4096 4096 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (4096 4096 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (4096 4096 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (2048 2048 (:LINEAR EXPT->-1-TWO))
 (2048 2048 (:LINEAR EXPT-<-1-TWO))
 (2048 2048 (:LINEAR EXPT-<-1-ONE))
 (1024 1024 (:LINEAR ADE::PISO2-SREG$EXTRACT1-NOT-EMPTY))
 (1024 1024 (:LINEAR ADE::PISO2-SREG$EXTRACT0-NOT-EMPTY))
 (672 16 (:REWRITE TAKE-OF-TOO-MANY))
 (648 8 (:DEFINITION TAKE))
 (312 112 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (240 24 (:REWRITE ADE::LEN-STRIP-CARS))
 (208 112 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (208 8 (:REWRITE ADE::LEN-CDR))
 (200 104 (:REWRITE SIMPLIFY-SUMS-<))
 (192 104 (:REWRITE DEFAULT-<-2))
 (128 8 (:REWRITE ZP-OPEN))
 (112 112 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (112 112 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (112 112 (:REWRITE |(< (- x) (- y))|))
 (112 104 (:REWRITE DEFAULT-<-1))
 (64 16 (:REWRITE TAKE-WHEN-ATOM))
 (48 48 (:TYPE-PRESCRIPTION STRIP-CARS))
 (32 16 (:REWRITE |(+ c (+ d x))|))
 (17 17 (:REWRITE |(+ 0 x)|))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (8 8 (:REWRITE |(< d (+ c x))|))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (8 8 (:REWRITE |(< (+ d x) (+ c y))|))
 (8 8 (:REWRITE |(< (+ c x) d)|))
 (8 8 (:REWRITE |(< (+ c x) (+ d y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::V-TO-NAT-OF-REPEAT-LEMMA
 (291 40 (:REWRITE CONSP-OF-REPEAT))
 (250 41 (:REWRITE ZP-OPEN))
 (197 9 (:DEFINITION BINARY-APPEND))
 (168 19 (:REWRITE |(< d (+ c x))|))
 (145 8 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (116 18 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (96 18 (:REWRITE DEFAULT-CDR))
 (80 14 (:REWRITE DEFAULT-CAR))
 (70 70 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (68 4 (:REWRITE CAR-OF-APPEND))
 (57 6 (:LINEAR ADE::EXPT-LINEAR-LOWER-<=-INSTANCE))
 (53 49 (:REWRITE SIMPLIFY-SUMS-<))
 (53 49 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (53 49 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (52 49 (:REWRITE DEFAULT-<-2))
 (51 6 (:LINEAR EXPT-X->=-X))
 (51 6 (:LINEAR EXPT-X->-X))
 (50 49 (:REWRITE DEFAULT-<-1))
 (49 49 (:REWRITE |(< (- x) (- y))|))
 (24 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (24 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (24 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 8 (:REWRITE DEFAULT-*-2))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (14 1 (:DEFINITION NATP))
 (13 9 (:REWRITE DEFAULT-+-2))
 (12 12 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (12 12 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (12 12 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-EXPT-2))
 (9 9 (:REWRITE DEFAULT-EXPT-1))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE |(expt x (- n))|))
 (9 9 (:REWRITE |(expt 2^i n)|))
 (9 9 (:REWRITE |(expt 1/c n)|))
 (9 9 (:REWRITE |(expt (- x) n)|))
 (9 1 (:REWRITE |(< (+ c x) d)|))
 (8 8 (:REWRITE DEFAULT-*-1))
 (7 6 (:LINEAR EXPT-<-1-TWO))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (6 6 (:LINEAR EXPT->-1-TWO))
 (6 6 (:LINEAR EXPT-<-1-ONE))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (5 5 (:REWRITE REDUCE-INTEGERP-+))
 (5 5 (:REWRITE INTEGERP-MINUS-X))
 (5 5 (:REWRITE |(< (- x) 0)|))
 (5 5 (:META META-INTEGERP-CORRECT))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (3 3 (:REWRITE |(< 0 (- x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::PISO2-SREG$INV-PRESERVED
 (39104 39104 (:REWRITE NTH-WHEN-PREFIXP))
 (26444 14066 (:REWRITE DEFAULT-+-2))
 (18544 4497 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (18544 4497 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (18544 4497 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (17032 17032 (:LINEAR LEN-WHEN-PREFIXP))
 (14066 14066 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (14066 14066 (:REWRITE DEFAULT-+-1))
 (11259 5713 (:REWRITE DEFAULT-<-2))
 (11252 5713 (:REWRITE SIMPLIFY-SUMS-<))
 (8516 8516 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (7124 5829 (:REWRITE |(expt 2^i n)|))
 (6372 1062 (:LINEAR EXPT-X->=-X))
 (6372 1062 (:LINEAR EXPT-X->-X))
 (6372 1062 (:LINEAR EXPT->-1-ONE))
 (5829 5829 (:REWRITE DEFAULT-EXPT-1))
 (5829 5829 (:REWRITE |(expt x (- n))|))
 (5829 5829 (:REWRITE |(expt 1/c n)|))
 (5829 5829 (:REWRITE |(expt (- x) n)|))
 (5735 5713 (:REWRITE DEFAULT-<-1))
 (5726 5726 (:REWRITE |(< (- x) (- y))|))
 (5476 5476 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (5476 5476 (:REWRITE |(< 0 (- x))|))
 (4497 4497 (:REWRITE |(equal (- x) (- y))|))
 (3812 138 (:DEFINITION PAIRLIS$))
 (3607 138 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (3598 1788 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (2777 31 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (2124 2124 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (2124 2124 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (2124 2124 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (2124 2124 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (1788 1788 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1062 1062 (:LINEAR EXPT->-1-TWO))
 (1062 1062 (:LINEAR EXPT-<-1-TWO))
 (1062 1062 (:LINEAR EXPT-<-1-ONE))
 (940 31 (:REWRITE CAR-OF-APPEND))
 (899 23 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (757 91 (:REWRITE |(< d (+ c x))|))
 (574 88 (:REWRITE REPEAT-WHEN-ZP))
 (572 2 (:REWRITE TAKE-WHEN-PREFIXP))
 (489 489 (:TYPE-PRESCRIPTION BOOLEANP))
 (444 4 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (423 16 (:REWRITE ADE::NTHCDR-APPEND))
 (390 10 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (322 4 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (296 22 (:REWRITE CONSP-OF-REPEAT))
 (294 98 (:REWRITE ADE::CAR-V-THREEFIX))
 (275 275 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (275 275 (:REWRITE DEFAULT-*-2))
 (275 275 (:REWRITE DEFAULT-*-1))
 (237 237 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (210 12 (:DEFINITION NFIX))
 (196 98 (:DEFINITION ADE::3V-FIX))
 (183 25 (:REWRITE |(< (+ c x) d)|))
 (152 152 (:TYPE-PRESCRIPTION ADE::3VP))
 (132 12 (:REWRITE |(+ (if a b c) x)|))
 (90 88 (:REWRITE DEFAULT-UNARY-MINUS))
 (82 2 (:REWRITE TAKE-WHEN-ATOM))
 (82 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (82 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (74 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (70 4 (:REWRITE |(< x (if a b c))|))
 (52 52 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (52 52 (:REWRITE |(equal (- x) 0)|))
 (50 2 (:DEFINITION NATP))
 (36 36 (:TYPE-PRESCRIPTION ZP))
 (26 26 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (26 26 (:REWRITE |(< (- x) 0)|))
 (24 4 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (24 4 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (16 4 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (16 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (12 12 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (11 11 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (9 9 (:TYPE-PRESCRIPTION ADE::F-AND3))
 (8 8 (:TYPE-PRESCRIPTION PREFIXP))
 (8 8 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (6 2 (:REWRITE |(< (if a b c) x)|))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::PISO2-SREG$EXTRACTED0-STEP
 (12 12 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT0-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 )
(ADE::PISO2-SREG$EXTRACTED1-STEP
 (12 12 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT1-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 )
(ADE::PISO2-SREG$EXTRACTED-STEP-CORRECT
 (80012 80012 (:REWRITE NTH-WHEN-PREFIXP))
 (58486 31426 (:REWRITE DEFAULT-+-2))
 (38662 9459 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (38662 9459 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (38662 9459 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (34662 34662 (:LINEAR LEN-WHEN-PREFIXP))
 (31426 31426 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (31426 31426 (:REWRITE DEFAULT-+-1))
 (23630 12156 (:REWRITE SIMPLIFY-SUMS-<))
 (23582 12156 (:REWRITE DEFAULT-<-2))
 (17331 17331 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (15473 7688 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (14421 11842 (:REWRITE |(expt 2^i n)|))
 (12972 2162 (:LINEAR EXPT-X->=-X))
 (12972 2162 (:LINEAR EXPT-X->-X))
 (12972 2162 (:LINEAR EXPT->-1-ONE))
 (12387 12387 (:REWRITE |(< (- x) (- y))|))
 (12264 12156 (:REWRITE DEFAULT-<-1))
 (11842 11842 (:REWRITE DEFAULT-EXPT-1))
 (11842 11842 (:REWRITE |(expt x (- n))|))
 (11842 11842 (:REWRITE |(expt 1/c n)|))
 (11842 11842 (:REWRITE |(expt (- x) n)|))
 (11297 11297 (:REWRITE |(< 0 (- x))|))
 (11286 11286 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (9459 9459 (:REWRITE |(equal (- x) (- y))|))
 (9148 319 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (7929 87 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (7815 323 (:REWRITE TAKE-WHEN-ATOM))
 (7745 284 (:DEFINITION PAIRLIS$))
 (7688 7688 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (4324 4324 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (4324 4324 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (4324 4324 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (4324 4324 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (2944 94 (:REWRITE CAR-OF-APPEND))
 (2517 60 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (2491 445 (:REWRITE |(< d (+ c x))|))
 (2162 2162 (:LINEAR EXPT->-1-TWO))
 (2162 2162 (:LINEAR EXPT-<-1-TWO))
 (2162 2162 (:LINEAR EXPT-<-1-ONE))
 (1404 36 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (1372 50 (:REWRITE ADE::NTHCDR-APPEND))
 (1144 198 (:REWRITE REPEAT-WHEN-ZP))
 (1144 4 (:REWRITE TAKE-WHEN-PREFIXP))
 (935 242 (:REWRITE ADE::CAR-V-THREEFIX))
 (888 8 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (696 52 (:REWRITE CONSP-OF-REPEAT))
 (644 8 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (554 554 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (554 554 (:REWRITE DEFAULT-*-2))
 (554 554 (:REWRITE DEFAULT-*-1))
 (542 226 (:REWRITE |(< (+ c x) d)|))
 (484 242 (:DEFINITION ADE::3V-FIX))
 (434 434 (:TYPE-PRESCRIPTION ADE::3VP))
 (430 48 (:DEFINITION NATP))
 (420 24 (:DEFINITION NFIX))
 (284 280 (:REWRITE DEFAULT-UNARY-MINUS))
 (264 24 (:REWRITE |(+ (if a b c) x)|))
 (165 165 (:REWRITE |(< (+ d x) (+ c y))|))
 (165 165 (:REWRITE |(< (+ c x) (+ d y))|))
 (164 4 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (164 4 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (148 4 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (140 8 (:REWRITE |(< x (if a b c))|))
 (139 139 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (139 139 (:REWRITE |(equal (- x) 0)|))
 (116 3 (:REWRITE ADE::BVP-TAKE))
 (72 12 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (72 12 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (70 70 (:TYPE-PRESCRIPTION ZP))
 (64 16 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (48 48 (:TYPE-PRESCRIPTION NATP))
 (44 44 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (44 44 (:REWRITE DEFAULT-UNARY-/))
 (39 3 (:REWRITE CONSP-OF-TAKE))
 (36 36 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (36 36 (:TYPE-PRESCRIPTION ADE::F-AND3))
 (35 35 (:REWRITE |(< (- x) 0)|))
 (32 4 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (24 24 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (24 24 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (16 16 (:TYPE-PRESCRIPTION PREFIXP))
 (16 16 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (12 4 (:REWRITE |(< (if a b c) x)|))
 (11 11 (:REWRITE FOLD-CONSTS-IN-+))
 (10 2 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (9 3 (:REWRITE CAR-OF-TAKE))
 (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))
 (6 3 (:REWRITE LEN-OF-TAKE))
 (4 4 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 )
(ADE::PISO2-SREG$VALID-ST-PRESERVED-AUX
 (7 7 (:REWRITE DEFAULT-CDR))
 (6 6 (:TYPE-PRESCRIPTION LEN))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1 1 (:REWRITE NORMALIZE-ADDENDS))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::PISO2-SREG$VALID-ST-PRESERVED
 (131098 131098 (:REWRITE NTH-WHEN-PREFIXP))
 (92364 52718 (:REWRITE DEFAULT-+-2))
 (52718 52718 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (52718 52718 (:REWRITE DEFAULT-+-1))
 (33237 1648 (:DEFINITION PAIRLIS$))
 (33184 1545 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (27899 7937 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (27835 7937 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (27835 7937 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (18872 1048 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (11780 5890 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (10673 115 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (9432 3144 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (8639 4935 (:REWRITE SIMPLIFY-SUMS-<))
 (8639 4935 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8639 4935 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (8328 694 (:REWRITE ZP-OPEN))
 (8177 4935 (:REWRITE DEFAULT-<-2))
 (7937 7937 (:REWRITE |(equal (- x) (- y))|))
 (7408 7408 (:LINEAR LEN-WHEN-PREFIXP))
 (6966 766 (:REWRITE |(< d (+ c x))|))
 (6324 1358 (:REWRITE REPEAT-WHEN-ZP))
 (6322 6322 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (5890 5890 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (5397 4935 (:REWRITE DEFAULT-<-1))
 (4935 4935 (:REWRITE |(< (- x) (- y))|))
 (4494 1498 (:REWRITE ADE::CAR-V-THREEFIX))
 (4056 312 (:REWRITE CONSP-OF-REPEAT))
 (3705 3705 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (3705 3705 (:REWRITE |(< 0 (- x))|))
 (3704 3704 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3600 115 (:REWRITE CAR-OF-APPEND))
 (3144 3144 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (2996 1498 (:DEFINITION ADE::3V-FIX))
 (2772 462 (:LINEAR EXPT-X->=-X))
 (2772 462 (:LINEAR EXPT-X->-X))
 (2772 462 (:LINEAR EXPT->-1-ONE))
 (2676 2676 (:REWRITE DEFAULT-EXPT-1))
 (2676 2676 (:REWRITE |(expt x (- n))|))
 (2676 2676 (:REWRITE |(expt 2^i n)|))
 (2676 2676 (:REWRITE |(expt 1/c n)|))
 (2676 2676 (:REWRITE |(expt (- x) n)|))
 (2328 2328 (:REWRITE DEFAULT-UNARY-MINUS))
 (1991 72 (:REWRITE ADE::NTHCDR-APPEND))
 (1871 1871 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1871 1871 (:REWRITE DEFAULT-*-2))
 (1871 1871 (:REWRITE DEFAULT-*-1))
 (1720 1720 (:TYPE-PRESCRIPTION ADE::3VP))
 (1536 1536 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (1536 256 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (1536 256 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (1482 38 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (1024 256 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (974 974 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (974 974 (:REWRITE |(equal (- x) 0)|))
 (924 924 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (924 924 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (924 924 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (924 924 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (512 512 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (463 463 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (462 462 (:LINEAR EXPT->-1-TWO))
 (462 462 (:LINEAR EXPT-<-1-TWO))
 (462 462 (:LINEAR EXPT-<-1-ONE))
 (382 382 (:TYPE-PRESCRIPTION ZP))
 (256 256 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (238 238 (:TYPE-PRESCRIPTION ADE::BOOLEANP-IF*))
 (82 82 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::PISO2-SREG$EXTRACT0-LEMMA
 (37260 30558 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (22200 13770 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (7780 3010 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (3515 3515 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (3362 250 (:DEFINITION STRIP-CARS))
 (3275 3275 (:REWRITE NTH-WHEN-PREFIXP))
 (3010 3010 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2242 604 (:REWRITE DEFAULT-CAR))
 (2197 531 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2197 531 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2197 531 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2139 1138 (:REWRITE DEFAULT-+-2))
 (1744 48 (:REWRITE TAKE-OF-TOO-MANY))
 (1173 1125 (:REWRITE DEFAULT-CDR))
 (1138 1138 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1138 1138 (:REWRITE NORMALIZE-ADDENDS))
 (1138 1138 (:REWRITE DEFAULT-+-1))
 (1136 16 (:DEFINITION TAKE))
 (1024 1024 (:LINEAR LEN-WHEN-PREFIXP))
 (660 467 (:REWRITE |(expt 2^i n)|))
 (531 531 (:REWRITE |(equal (- x) (- y))|))
 (512 512 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (480 16 (:REWRITE ADE::LEN-CDR))
 (467 467 (:REWRITE DEFAULT-EXPT-1))
 (467 467 (:REWRITE |(expt x (- n))|))
 (467 467 (:REWRITE |(expt 1/c n)|))
 (467 467 (:REWRITE |(expt (- x) n)|))
 (384 64 (:LINEAR EXPT-X->=-X))
 (384 64 (:LINEAR EXPT-X->-X))
 (384 64 (:LINEAR EXPT->-1-ONE))
 (290 82 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (225 18 (:DEFINITION NTHCDR))
 (192 48 (:REWRITE TAKE-WHEN-ATOM))
 (187 17 (:REWRITE |(+ (+ x y) z)|))
 (149 49 (:REWRITE |(+ c (+ d x))|))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (128 128 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (85 17 (:REWRITE |(+ y x)|))
 (82 82 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (82 82 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (82 82 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (82 82 (:REWRITE |(< (- x) (- y))|))
 (66 66 (:REWRITE SIMPLIFY-SUMS-<))
 (66 66 (:REWRITE DEFAULT-<-2))
 (66 66 (:REWRITE DEFAULT-<-1))
 (64 64 (:LINEAR EXPT->-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-ONE))
 (35 35 (:REWRITE |(+ 0 x)|))
 (30 6 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT0-ACT))
 (19 1 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (18 18 (:REWRITE |(< (- x) 0)|))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (17 17 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (17 17 (:REWRITE DEFAULT-*-2))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 16 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (16 16 (:REWRITE |(equal (- x) 0)|))
 (16 16 (:REWRITE |(< d (+ c x))|))
 (16 16 (:REWRITE |(< 0 (- x))|))
 (16 16 (:REWRITE |(< (+ d x) (+ c y))|))
 (16 16 (:REWRITE |(< (+ c x) d)|))
 (16 16 (:REWRITE |(< (+ c x) (+ d y))|))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (9 9 (:META META-INTEGERP-CORRECT))
 (7 1 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (6 6 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 2 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (4 2 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (3 3 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN-ACT))
 (2 2 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-CAR-OF-PISO2-SREG$EXTRACT0
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT0-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 )
(ADE::PISO2-SREG$EXTRACT1-LEMMA
 (36918 30252 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (18706 10894 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (7812 3010 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (6617 6223 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (3275 3275 (:REWRITE NTH-WHEN-PREFIXP))
 (3102 250 (:DEFINITION STRIP-CARS))
 (3010 3010 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2224 604 (:REWRITE DEFAULT-CAR))
 (2197 531 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2197 531 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2197 531 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2139 1138 (:REWRITE DEFAULT-+-2))
 (1616 48 (:REWRITE TAKE-OF-TOO-MANY))
 (1173 1125 (:REWRITE DEFAULT-CDR))
 (1138 1138 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1138 1138 (:REWRITE NORMALIZE-ADDENDS))
 (1138 1138 (:REWRITE DEFAULT-+-1))
 (1072 16 (:DEFINITION TAKE))
 (1024 1024 (:LINEAR LEN-WHEN-PREFIXP))
 (660 467 (:REWRITE |(expt 2^i n)|))
 (531 531 (:REWRITE |(equal (- x) (- y))|))
 (512 512 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (467 467 (:REWRITE DEFAULT-EXPT-1))
 (467 467 (:REWRITE |(expt x (- n))|))
 (467 467 (:REWRITE |(expt 1/c n)|))
 (467 467 (:REWRITE |(expt (- x) n)|))
 (416 16 (:REWRITE ADE::LEN-CDR))
 (384 64 (:LINEAR EXPT-X->=-X))
 (384 64 (:LINEAR EXPT-X->-X))
 (384 64 (:LINEAR EXPT->-1-ONE))
 (290 82 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (225 18 (:DEFINITION NTHCDR))
 (192 48 (:REWRITE TAKE-WHEN-ATOM))
 (187 17 (:REWRITE |(+ (+ x y) z)|))
 (149 49 (:REWRITE |(+ c (+ d x))|))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (128 128 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (128 128 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (85 17 (:REWRITE |(+ y x)|))
 (82 82 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (82 82 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (82 82 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (82 82 (:REWRITE |(< (- x) (- y))|))
 (66 66 (:REWRITE SIMPLIFY-SUMS-<))
 (66 66 (:REWRITE DEFAULT-<-2))
 (66 66 (:REWRITE DEFAULT-<-1))
 (64 64 (:LINEAR EXPT->-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-TWO))
 (64 64 (:LINEAR EXPT-<-1-ONE))
 (35 35 (:REWRITE |(+ 0 x)|))
 (30 6 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT1-ACT))
 (19 1 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (18 18 (:REWRITE |(< (- x) 0)|))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (17 17 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (17 17 (:REWRITE DEFAULT-*-2))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 16 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (16 16 (:REWRITE |(equal (- x) 0)|))
 (16 16 (:REWRITE |(< d (+ c x))|))
 (16 16 (:REWRITE |(< 0 (- x))|))
 (16 16 (:REWRITE |(< (+ d x) (+ c y))|))
 (16 16 (:REWRITE |(< (+ c x) d)|))
 (16 16 (:REWRITE |(< (+ c x) (+ d y))|))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (9 9 (:META META-INTEGERP-CORRECT))
 (7 1 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (6 6 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 2 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (4 2 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (3 3 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN-ACT))
 (2 2 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-CAR-OF-PISO2-SREG$EXTRACT1
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT1-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 )
(ADE::PISO2-SREG$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 )
(ADE::PISO2-SREG$IN-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::PISO2-SREG$IN-SEQ-LEMMA
 (2035 607 (:REWRITE DEFAULT-CAR))
 (1792 240 (:REWRITE ADE::F-GATES=B-GATES))
 (926 926 (:REWRITE NTH-WHEN-PREFIXP))
 (725 65 (:REWRITE ZP-OPEN))
 (592 296 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (584 80 (:DEFINITION STRIP-CARS))
 (520 40 (:DEFINITION NTHCDR))
 (462 402 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (410 58 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (410 58 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (410 58 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (354 282 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (296 296 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (280 56 (:REWRITE |(+ c (+ d x))|))
 (240 80 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (213 35 (:DEFINITION BINARY-APPEND))
 (211 211 (:REWRITE DEFAULT-CDR))
 (200 40 (:REWRITE |(+ y x)|))
 (176 176 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (176 176 (:REWRITE NORMALIZE-ADDENDS))
 (176 176 (:REWRITE DEFAULT-+-2))
 (176 176 (:REWRITE DEFAULT-+-1))
 (170 170 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$STEP))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (160 160 (:TYPE-PRESCRIPTION ADE::BVP))
 (144 36 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (64 64 (:REWRITE SIMPLIFY-SUMS-<))
 (64 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (58 58 (:REWRITE |(equal (- x) (- y))|))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (36 36 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (34 34 (:TYPE-PRESCRIPTION ADE::DE))
 (28 28 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (14 14 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT1-LEMMA))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT0-LEMMA))
 (12 12 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::PISO2-SREG$IN0-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 )
(ADE::PISO2-SREG$IN0-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::PISO2-SREG$IN0-SEQ-LEMMA
 (2032 604 (:REWRITE DEFAULT-CAR))
 (1792 240 (:REWRITE ADE::F-GATES=B-GATES))
 (926 926 (:REWRITE NTH-WHEN-PREFIXP))
 (725 65 (:REWRITE ZP-OPEN))
 (592 296 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (584 80 (:DEFINITION STRIP-CARS))
 (520 40 (:DEFINITION NTHCDR))
 (462 402 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (410 58 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (410 58 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (410 58 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (354 282 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (296 296 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (280 56 (:REWRITE |(+ c (+ d x))|))
 (240 80 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (213 35 (:DEFINITION BINARY-APPEND))
 (211 211 (:REWRITE DEFAULT-CDR))
 (200 40 (:REWRITE |(+ y x)|))
 (176 176 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (176 176 (:REWRITE NORMALIZE-ADDENDS))
 (176 176 (:REWRITE DEFAULT-+-2))
 (176 176 (:REWRITE DEFAULT-+-1))
 (170 170 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$STEP))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (160 160 (:TYPE-PRESCRIPTION ADE::BVP))
 (144 36 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (64 64 (:REWRITE SIMPLIFY-SUMS-<))
 (64 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (58 58 (:REWRITE |(equal (- x) (- y))|))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (36 36 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (34 34 (:TYPE-PRESCRIPTION ADE::DE))
 (28 28 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (14 14 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT1-LEMMA))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT0-LEMMA))
 (12 12 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::PISO2-SREG$IN1-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 )
(ADE::PISO2-SREG$IN1-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::PISO2-SREG$IN1-SEQ-LEMMA
 (2032 604 (:REWRITE DEFAULT-CAR))
 (1792 240 (:REWRITE ADE::F-GATES=B-GATES))
 (926 926 (:REWRITE NTH-WHEN-PREFIXP))
 (725 65 (:REWRITE ZP-OPEN))
 (592 296 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (584 80 (:DEFINITION STRIP-CARS))
 (520 40 (:DEFINITION NTHCDR))
 (462 402 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (410 58 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (410 58 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (410 58 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (354 282 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (296 296 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (280 56 (:REWRITE |(+ c (+ d x))|))
 (240 80 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (213 35 (:DEFINITION BINARY-APPEND))
 (211 211 (:REWRITE DEFAULT-CDR))
 (200 40 (:REWRITE |(+ y x)|))
 (176 176 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (176 176 (:REWRITE NORMALIZE-ADDENDS))
 (176 176 (:REWRITE DEFAULT-+-2))
 (176 176 (:REWRITE DEFAULT-+-1))
 (170 170 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$STEP))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (160 160 (:TYPE-PRESCRIPTION ADE::BVP))
 (144 36 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (64 64 (:REWRITE SIMPLIFY-SUMS-<))
 (64 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (58 58 (:REWRITE |(equal (- x) (- y))|))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (36 36 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (34 34 (:TYPE-PRESCRIPTION ADE::DE))
 (28 28 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (14 14 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT1-LEMMA))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT0-LEMMA))
 (12 12 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::PISO2-SREG$OUT0-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT0-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (6 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$BIT0-OUT))
 )
(ADE::PISO2-SREG$OUT0-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 )
(ADE::PISO2-SREG$OUT0-SEQ-LEMMA
 (1792 160 (:REWRITE ADE::F-GATES=B-GATES))
 (1528 988 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (1309 361 (:REWRITE DEFAULT-CAR))
 (725 65 (:REWRITE ZP-OPEN))
 (614 614 (:REWRITE NTH-WHEN-PREFIXP))
 (592 296 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (520 40 (:DEFINITION NTHCDR))
 (466 72 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (466 72 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (466 72 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (398 36 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (360 120 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (354 282 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (344 40 (:DEFINITION STRIP-CARS))
 (296 296 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (280 280 (:TYPE-PRESCRIPTION ADE::BVP))
 (280 56 (:REWRITE |(+ c (+ d x))|))
 (213 35 (:DEFINITION BINARY-APPEND))
 (200 40 (:REWRITE |(+ y x)|))
 (176 176 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (176 176 (:REWRITE NORMALIZE-ADDENDS))
 (176 176 (:REWRITE DEFAULT-+-2))
 (176 176 (:REWRITE DEFAULT-+-1))
 (171 171 (:REWRITE DEFAULT-CDR))
 (170 170 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$STEP))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 120 (:TYPE-PRESCRIPTION STRIP-CARS))
 (120 120 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (120 40 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (120 40 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (72 72 (:REWRITE |(equal (- x) (- y))|))
 (64 64 (:REWRITE SIMPLIFY-SUMS-<))
 (64 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (56 14 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (50 50 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (39 39 (:REWRITE ADE::PISO2-SREG$EXTRACT0-LEMMA))
 (34 34 (:TYPE-PRESCRIPTION ADE::DE))
 (14 14 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT1-LEMMA))
 (14 14 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (12 12 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::PISO2-SREG$OUT1-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT1-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (6 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$BIT1-OUT))
 )
(ADE::PISO2-SREG$OUT1-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 )
(ADE::PISO2-SREG$OUT1-SEQ-LEMMA
 (1480 160 (:REWRITE ADE::F-GATES=B-GATES))
 (841 361 (:REWRITE DEFAULT-CAR))
 (748 748 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (725 65 (:REWRITE ZP-OPEN))
 (634 634 (:REWRITE NTH-WHEN-PREFIXP))
 (592 296 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (520 40 (:DEFINITION NTHCDR))
 (466 72 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (466 72 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (466 72 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (398 36 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (360 120 (:TYPE-PRESCRIPTION ADE::BOOLEANP-F$FAST-ZERO))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (296 296 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (280 280 (:TYPE-PRESCRIPTION ADE::BVP))
 (280 56 (:REWRITE |(+ c (+ d x))|))
 (240 40 (:DEFINITION STRIP-CARS))
 (213 35 (:DEFINITION BINARY-APPEND))
 (200 40 (:REWRITE |(+ y x)|))
 (176 176 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (176 176 (:REWRITE NORMALIZE-ADDENDS))
 (176 176 (:REWRITE DEFAULT-+-2))
 (176 176 (:REWRITE DEFAULT-+-1))
 (171 171 (:REWRITE DEFAULT-CDR))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (122 122 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (120 120 (:TYPE-PRESCRIPTION STRIP-CARS))
 (120 120 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (120 40 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (120 40 (:REWRITE ADE::BOOLEANP-F$FAST-ZERO))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (84 14 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (72 72 (:REWRITE |(equal (- x) (- y))|))
 (64 64 (:REWRITE SIMPLIFY-SUMS-<))
 (64 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (56 14 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (50 50 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (39 39 (:REWRITE ADE::PISO2-SREG$EXTRACT1-LEMMA))
 (14 14 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (14 14 (:REWRITE ADE::PISO2-SREG$EXTRACT0-LEMMA))
 (14 14 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (12 12 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::PISO2-SREG$OP-OF-LEN-0
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (7 4 (:REWRITE DEFAULT-+-2))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4 4 (:REWRITE NORMALIZE-ADDENDS))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE |(equal (- x) 0)|))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::PISO2-SREG$DATAFLOW-CORRECT-AUX
 (184 172 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (94 2 (:DEFINITION ADE::PISO2-SREG$OP-MAP))
 (53 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (52 2 (:REWRITE ADE::PISO2-SREG$OP-OF-LEN-0))
 (26 12 (:REWRITE DEFAULT-CDR))
 (20 20 (:TYPE-PRESCRIPTION LEN))
 (20 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (14 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (14 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (14 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (14 2 (:DEFINITION LEN))
 (12 12 (:REWRITE DEFAULT-CAR))
 (10 10 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$OP))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (5 5 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2 2 (:REWRITE NORMALIZE-ADDENDS))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::PISO2-SREG$DATAFLOW0-CORRECT
 (8899 565 (:DEFINITION LEN))
 (2313 128 (:REWRITE ADE::LEN-CDR))
 (2114 187 (:REWRITE DEFAULT-CAR))
 (1728 750 (:REWRITE DEFAULT-CDR))
 (1275 40 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1268 657 (:REWRITE DEFAULT-+-2))
 (1121 89 (:REWRITE ZP-OPEN))
 (1104 609 (:REWRITE DEFAULT-<-2))
 (1005 609 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (978 978 (:LINEAR LEN-WHEN-PREFIXP))
 (730 609 (:REWRITE SIMPLIFY-SUMS-<))
 (730 609 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (710 710 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (657 657 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (657 657 (:REWRITE NORMALIZE-ADDENDS))
 (657 657 (:REWRITE DEFAULT-+-1))
 (609 609 (:REWRITE DEFAULT-<-1))
 (609 609 (:REWRITE |(< (- x) (- y))|))
 (504 56 (:REWRITE |(< d (+ c x))|))
 (495 495 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (495 495 (:REWRITE |(< 0 (- x))|))
 (489 489 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (458 14 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (294 91 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (268 91 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (268 91 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (225 45 (:REWRITE |(< x (if a b c))|))
 (186 20 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (155 5 (:REWRITE ADE::LEN-PISO2-SREG$DATA0-IN))
 (146 146 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (144 144 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN0-SEQ))
 (132 36 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (121 1 (:REWRITE |(equal (+ c x) d)|))
 (115 115 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (92 92 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$EXTRACT1))
 (91 91 (:REWRITE |(equal (- x) (- y))|))
 (80 5 (:REWRITE ADE::NFIX-OF-NAT))
 (70 5 (:DEFINITION NFIX))
 (70 5 (:DEFINITION NATP))
 (55 55 (:REWRITE NTH-WHEN-PREFIXP))
 (50 50 (:LINEAR ADE::PISO2-SREG$EXTRACT1-NOT-EMPTY))
 (47 47 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (47 47 (:REWRITE |(equal (- x) 0)|))
 (40 40 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$STEP))
 (40 10 (:REWRITE |(equal (if a b c) x)|))
 (40 8 (:REWRITE |(+ c (+ d x))|))
 (12 12 (:REWRITE ADE::PISO2-SREG$RUN-PLUS))
 (12 12 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (10 10 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (10 10 (:REWRITE REDUCE-INTEGERP-+))
 (10 10 (:REWRITE INTEGERP-MINUS-X))
 (10 10 (:REWRITE |(< (- x) 0)|))
 (10 10 (:META META-INTEGERP-CORRECT))
 (6 2 (:REWRITE ADE::PISO2-SREG$INV-PRESERVED))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$RUN))
 )
(ADE::PISO2-SREG$DATAFLOW1-CORRECT
 (9025 569 (:DEFINITION LEN))
 (2313 128 (:REWRITE ADE::LEN-CDR))
 (2114 187 (:REWRITE DEFAULT-CAR))
 (1732 754 (:REWRITE DEFAULT-CDR))
 (1276 661 (:REWRITE DEFAULT-+-2))
 (1275 40 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1121 89 (:REWRITE ZP-OPEN))
 (1116 615 (:REWRITE DEFAULT-<-2))
 (1017 615 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (986 986 (:LINEAR LEN-WHEN-PREFIXP))
 (742 615 (:REWRITE SIMPLIFY-SUMS-<))
 (742 615 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (716 716 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (661 661 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (661 661 (:REWRITE NORMALIZE-ADDENDS))
 (661 661 (:REWRITE DEFAULT-+-1))
 (615 615 (:REWRITE DEFAULT-<-1))
 (615 615 (:REWRITE |(< (- x) (- y))|))
 (504 56 (:REWRITE |(< d (+ c x))|))
 (501 501 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (501 501 (:REWRITE |(< 0 (- x))|))
 (493 493 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (458 14 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (294 91 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (268 91 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (268 91 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (225 45 (:REWRITE |(< x (if a b c))|))
 (186 20 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (155 5 (:REWRITE ADE::LEN-PISO2-SREG$DATA1-IN))
 (146 146 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (144 144 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN1-SEQ))
 (132 36 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (121 1 (:REWRITE |(equal (+ c x) d)|))
 (115 115 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (100 100 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$EXTRACT0))
 (91 91 (:REWRITE |(equal (- x) (- y))|))
 (80 5 (:REWRITE ADE::NFIX-OF-NAT))
 (70 5 (:DEFINITION NFIX))
 (70 5 (:DEFINITION NATP))
 (55 55 (:REWRITE NTH-WHEN-PREFIXP))
 (54 54 (:LINEAR ADE::PISO2-SREG$EXTRACT0-NOT-EMPTY))
 (47 47 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (47 47 (:REWRITE |(equal (- x) 0)|))
 (40 40 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$STEP))
 (40 10 (:REWRITE |(equal (if a b c) x)|))
 (40 8 (:REWRITE |(+ c (+ d x))|))
 (12 12 (:REWRITE ADE::PISO2-SREG$RUN-PLUS))
 (12 12 (:REWRITE ADE::PISO2-SREG$INPUT-FORMAT-PLUS))
 (10 10 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (10 10 (:REWRITE REDUCE-INTEGERP-+))
 (10 10 (:REWRITE INTEGERP-MINUS-X))
 (10 10 (:REWRITE |(< (- x) 0)|))
 (10 10 (:META META-INTEGERP-CORRECT))
 (6 2 (:REWRITE ADE::PISO2-SREG$INV-PRESERVED))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$RUN))
 )
(ADE::PISO2-SREG$FUNCTIONALLY-CORRECT-1
 (423 4 (:DEFINITION ADE::PISO2-SREG$IN0-SEQ))
 (361 12 (:REWRITE ADE::PISO2-SREG$OP-OF-LEN-0))
 (259 4 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (250 4 (:DEFINITION ADE::PISO2-SREG$OUT0-SEQ))
 (235 27 (:DEFINITION LEN))
 (188 188 (:TYPE-PRESCRIPTION LEN))
 (188 4 (:DEFINITION ADE::PISO2-SREG$OP-MAP))
 (113 14 (:LINEAR ADE::LENS-OF-PISO2-SREG$EXTRACTS-UPPER-BOUND))
 (100 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (87 27 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (79 27 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (79 27 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (76 4 (:REWRITE ADE::PISO2-SREG$OUT0-ACT-INACTIVE))
 (62 35 (:REWRITE DEFAULT-+-2))
 (59 59 (:REWRITE DEFAULT-CDR))
 (52 52 (:TYPE-PRESCRIPTION ZP))
 (52 52 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-2))
 (52 26 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (46 46 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT0-ACT))
 (36 36 (:LINEAR LEN-WHEN-PREFIXP))
 (35 35 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (35 35 (:REWRITE NORMALIZE-ADDENDS))
 (35 35 (:REWRITE DEFAULT-+-1))
 (34 34 (:REWRITE ZP-OPEN))
 (32 32 (:REWRITE DEFAULT-CAR))
 (32 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (28 28 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN0-SEQ))
 (27 27 (:REWRITE |(equal (- x) (- y))|))
 (26 26 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN-ACT))
 (24 6 (:REWRITE ADE::OPEN-PISO2-SREG$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-PISO2-SREG$INPUT-FORMAT-N))
 (22 4 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (20 20 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$OUT0-ACT))
 (18 18 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 4 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (12 12 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$EXTRACT1))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (12 12 (:REWRITE |(equal (- x) 0)|))
 (12 6 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 6 (:REWRITE DEFAULT-<-2))
 (12 3 (:REWRITE ADE::OPEN-PISO2-SREG$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-PISO2-SREG$RUN))
 (11 11 (:LINEAR ADE::PISO2-SREG$EXTRACT0-NOT-EMPTY))
 (9 6 (:REWRITE SIMPLIFY-SUMS-<))
 (9 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 8 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (6 6 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (6 6 (:REWRITE DEFAULT-<-1))
 (6 6 (:REWRITE |(< 0 (- x))|))
 (6 6 (:REWRITE |(< (- x) (- y))|))
 (5 5 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (4 4 (:REWRITE ADE::PISO2-SREG$EXTRACT0-LEMMA))
 (3 3 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$RUN))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:LINEAR ADE::PISO2-SREG$EXTRACT1-NOT-EMPTY))
 )
(ADE::PISO2-SREG$FUNCTIONALLY-CORRECT-2
 (423 4 (:DEFINITION ADE::PISO2-SREG$IN1-SEQ))
 (361 12 (:REWRITE ADE::PISO2-SREG$OP-OF-LEN-0))
 (259 4 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-2))
 (250 4 (:DEFINITION ADE::PISO2-SREG$OUT1-SEQ))
 (235 27 (:DEFINITION LEN))
 (188 188 (:TYPE-PRESCRIPTION LEN))
 (188 4 (:DEFINITION ADE::PISO2-SREG$OP-MAP))
 (113 14 (:LINEAR ADE::LENS-OF-PISO2-SREG$EXTRACTS-UPPER-BOUND))
 (100 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (87 27 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (79 27 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (79 27 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (76 4 (:REWRITE ADE::PISO2-SREG$OUT1-ACT-INACTIVE))
 (62 35 (:REWRITE DEFAULT-+-2))
 (59 59 (:REWRITE DEFAULT-CDR))
 (52 52 (:TYPE-PRESCRIPTION ZP))
 (52 52 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-3))
 (52 26 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$IN-ACT))
 (46 46 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-PISO2-SREG$OUT1-ACT))
 (36 36 (:LINEAR LEN-WHEN-PREFIXP))
 (35 35 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (35 35 (:REWRITE NORMALIZE-ADDENDS))
 (35 35 (:REWRITE DEFAULT-+-1))
 (34 34 (:REWRITE ZP-OPEN))
 (32 32 (:REWRITE DEFAULT-CAR))
 (32 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (28 28 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN1-SEQ))
 (27 27 (:REWRITE |(equal (- x) (- y))|))
 (26 26 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$IN-ACT))
 (24 6 (:REWRITE ADE::OPEN-PISO2-SREG$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-PISO2-SREG$INPUT-FORMAT-N))
 (22 4 (:REWRITE ADE::PISO2-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (20 20 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$OUT1-ACT))
 (18 18 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 4 (:REWRITE ADE::PISO2-SREG$IN-ACT-INACTIVE))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (12 12 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$EXTRACT0))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (12 12 (:REWRITE |(equal (- x) 0)|))
 (12 6 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 6 (:REWRITE DEFAULT-<-2))
 (12 3 (:REWRITE ADE::OPEN-PISO2-SREG$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-PISO2-SREG$RUN))
 (11 11 (:LINEAR ADE::PISO2-SREG$EXTRACT1-NOT-EMPTY))
 (9 6 (:REWRITE SIMPLIFY-SUMS-<))
 (9 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 8 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$INPUT-FORMAT-LEMMA-1))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (6 6 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (6 6 (:REWRITE DEFAULT-<-1))
 (6 6 (:REWRITE |(< 0 (- x))|))
 (6 6 (:REWRITE |(< (- x) (- y))|))
 (5 5 (:REWRITE ADE::LENS-OF-PISO2-SREG$EXTRACTS-CONTRAPOSITIVE-LEMMA-1))
 (4 4 (:REWRITE ADE::PISO2-SREG$EXTRACT1-LEMMA))
 (3 3 (:TYPE-PRESCRIPTION ADE::PISO2-SREG$RUN))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:LINEAR ADE::PISO2-SREG$EXTRACT0-NOT-EMPTY))
 )