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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
(ADE::BINARY-AND*)
(ADE::BOOLEANP-BINARY-AND*)
(ADE::AND*-MACRO)
(ADE::BINARY-OR*)
(ADE::BOOLEANP-BINARY-OR*)
(ADE::OR*-MACRO)
(ADE::NOT*)
(ADE::BOOLEANP-NOT*)
(ADE::INSERT)
(ADE::TRUE-LISTP-INSERT
(11 8 (:REWRITE DEFAULT-CDR))
(4 4 (:REWRITE ZP-OPEN))
(3 3 (:REWRITE DEFAULT-CAR))
(2 2 (:REWRITE DEFAULT-+-2))
(2 2 (:REWRITE DEFAULT-+-1))
(1 1 (:REWRITE CDR-CONS))
)
(ADE::INSERT-UP-TO-I
(4 2 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-INSERT))
(2 2 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(ADE::TRUE-LIST-LISTP-INSERT-UP-TO-I
(20 7 (:DEFINITION TRUE-LISTP))
(16 12 (:REWRITE DEFAULT-CDR))
(9 5 (:REWRITE DEFAULT-CAR))
(4 4 (:REWRITE ZP-OPEN))
(2 2 (:REWRITE DEFAULT-+-2))
(2 2 (:REWRITE DEFAULT-+-1))
)
(ADE::CONS-OR-APPEND)
(ADE::CONS-OR-APPEND-AT-I)
(ADE::TRUE-LISTP-CONS-OR-APPEND-AT-I
(10 10 (:REWRITE DEFAULT-CDR))
(6 6 (:REWRITE DEFAULT-CAR))
(4 4 (:REWRITE DEFAULT-<-2))
(4 4 (:REWRITE DEFAULT-<-1))
(2 2 (:REWRITE DEFAULT-+-2))
(2 2 (:REWRITE DEFAULT-+-1))
)
(ADE::CONS-OR-APPEND-UP-TO-I
(4 4 (:REWRITE DEFAULT-<-2))
(4 4 (:REWRITE DEFAULT-<-1))
(4 4 (:REWRITE DEFAULT-+-2))
(4 4 (:REWRITE DEFAULT-+-1))
(2 1 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-CONS-OR-APPEND-AT-I))
(1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(ADE::TRUE-LIST-LISTP-CONS-OR-APPEND-UP-TO-I
(16 8 (:DEFINITION TRUE-LISTP))
(13 12 (:REWRITE DEFAULT-CDR))
(5 4 (:REWRITE DEFAULT-CAR))
(4 4 (:REWRITE DEFAULT-<-2))
(4 4 (:REWRITE DEFAULT-<-1))
(2 2 (:REWRITE DEFAULT-+-2))
(2 2 (:REWRITE DEFAULT-+-1))
)
(ADE::INDEX-OF-NESTED)
(ADE::INSERT-UP-TO-REC
(26 24 (:REWRITE DEFAULT-CDR))
(25 23 (:REWRITE DEFAULT-CAR))
(18 9 (:DEFINITION TRUE-LISTP))
(12 2 (:DEFINITION BINARY-APPEND))
(10 6 (:REWRITE DEFAULT-+-2))
(10 2 (:DEFINITION LEN))
(6 6 (:REWRITE DEFAULT-+-1))
(2 2 (:REWRITE DEFAULT-<-2))
(2 2 (:REWRITE DEFAULT-<-1))
)
(ADE::TRUE-LIST-LISTP-OF-APPEND
(27 25 (:REWRITE DEFAULT-CDR))
(24 12 (:DEFINITION TRUE-LISTP))
(18 16 (:REWRITE DEFAULT-CAR))
(5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(ADE::TRUE-LIST-LISTP-INSERT-UP-TO-REC
(54 6 (:DEFINITION BINARY-APPEND))
(29 26 (:REWRITE DEFAULT-CAR))
(28 25 (:REWRITE DEFAULT-CDR))
(16 8 (:DEFINITION TRUE-LISTP))
(15 6 (:REWRITE DEFAULT-+-2))
(15 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
(15 3 (:DEFINITION LEN))
(6 6 (:REWRITE DEFAULT-+-1))
(3 3 (:REWRITE DEFAULT-<-2))
(3 3 (:REWRITE DEFAULT-<-1))
)
(ADE::SHUFFLE
(45 45 (:REWRITE DEFAULT-CDR))
(20 20 (:REWRITE DEFAULT-CAR))
)
(ADE::TRUE-LIST-LISTP-SHUFFLE
(20 20 (:REWRITE DEFAULT-CDR))
(11 11 (:REWRITE DEFAULT-CAR))
(2 2 (:TYPE-PRESCRIPTION ADE::INSERT-UP-TO-REC))
)
(ADE::SHUFFLE-REC1
(6 3 (:DEFINITION TRUE-LISTP))
(4 4 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE DEFAULT-CAR))
)
(ADE::SHUFFLE-REC2
(2 2 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE DEFAULT-CAR))
(2 1 (:DEFINITION TRUE-LISTP))
)
(ADE::COMBINE)
(ADE::COMBINE-REC)
(ADE::NO-EMPTY-POWERSET)
(ADE::POWERSET)
|
