1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
(F1)
(F2)
(NTH-I-OUT-OF-RANGE
(18 13 (:REWRITE DEFAULT-<-2))
(17 11 (:REWRITE DEFAULT-+-2))
(13 13 (:REWRITE DEFAULT-<-1))
(11 11 (:REWRITE DEFAULT-+-1))
(6 6 (:REWRITE DEFAULT-CDR))
(5 5 (:REWRITE ZP-OPEN))
(3 3 (:REWRITE DEFAULT-CAR))
)
(NTH-I-F2-F1-BETTER
(42 2 (:DEFINITION NTH))
(38 6 (:DEFINITION LEN))
(14 8 (:REWRITE DEFAULT-+-2))
(12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-F1))
(12 7 (:REWRITE DEFAULT-<-2))
(8 8 (:REWRITE DEFAULT-CDR))
(8 8 (:REWRITE DEFAULT-+-1))
(7 7 (:REWRITE DEFAULT-<-1))
(2 2 (:REWRITE ZP-OPEN))
(2 2 (:REWRITE DEFAULT-CAR))
)
(BADGUY
(58 28 (:REWRITE DEFAULT-+-2))
(39 28 (:REWRITE DEFAULT-+-1))
(24 6 (:REWRITE COMMUTATIVITY-OF-+))
(24 6 (:DEFINITION INTEGER-ABS))
(24 3 (:DEFINITION LENGTH))
(15 3 (:DEFINITION LEN))
(9 9 (:REWRITE DEFAULT-CDR))
(9 7 (:REWRITE DEFAULT-<-2))
(8 8 (:REWRITE FOLD-CONSTS-IN-+))
(8 7 (:REWRITE DEFAULT-<-1))
(7 7 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE DEFAULT-UNARY-MINUS))
(3 3 (:TYPE-PRESCRIPTION LEN))
(3 3 (:REWRITE DEFAULT-REALPART))
(3 3 (:REWRITE DEFAULT-NUMERATOR))
(3 3 (:REWRITE DEFAULT-IMAGPART))
(3 3 (:REWRITE DEFAULT-DENOMINATOR))
(3 3 (:REWRITE DEFAULT-COERCE-2))
(3 3 (:REWRITE DEFAULT-COERCE-1))
)
(BADGUY-IS-CORRECT
(796 48 (:REWRITE NTH-I-OUT-OF-RANGE))
(234 127 (:REWRITE DEFAULT-+-2))
(174 174 (:REWRITE DEFAULT-CDR))
(160 20 (:REWRITE ZP-OPEN))
(136 68 (:REWRITE DEFAULT-<-2))
(127 127 (:REWRITE DEFAULT-+-1))
(92 68 (:REWRITE DEFAULT-<-1))
(82 82 (:REWRITE DEFAULT-CAR))
)
(F1-EQUALS-F2
(64 2 (:DEFINITION NTH))
(50 4 (:REWRITE NTH-I-OUT-OF-RANGE))
(41 7 (:DEFINITION LEN))
(37 1 (:DEFINITION BADGUY))
(18 10 (:REWRITE DEFAULT-+-2))
(16 2 (:REWRITE ZP-OPEN))
(11 11 (:REWRITE DEFAULT-CDR))
(10 10 (:REWRITE DEFAULT-+-1))
(10 5 (:REWRITE DEFAULT-<-2))
(6 5 (:REWRITE DEFAULT-<-1))
(6 2 (:DEFINITION NOT))
(4 4 (:REWRITE DEFAULT-CAR))
)
|
