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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
|
(PROOF-CHECKER-ARRAY::SUBSETP
(37 2 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-EQLABLE-LISTP))
(32 3 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(12 12 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(5 5 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(5 5 (:REWRITE DEFAULT-CDR))
(5 5 (:REWRITE DEFAULT-CAR))
(4 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-IMPLIES-EQLABLEP))
)
(PROOF-CHECKER-ARRAY::SUBSETP-CDR
(50 50 (:REWRITE DEFAULT-CAR))
(2 2 (:REWRITE CDR-CONS))
(2 2 (:REWRITE CAR-CONS))
)
(PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER
(29 29 (:REWRITE DEFAULT-CDR))
(27 27 (:REWRITE DEFAULT-CAR))
)
(PROOF-CHECKER-ARRAY::SUBSETP-APPEND
(186 93 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(93 93 (:TYPE-PRESCRIPTION TRUE-LISTP))
(93 93 (:TYPE-PRESCRIPTION BINARY-APPEND))
(89 71 (:REWRITE DEFAULT-CAR))
)
(PROOF-CHECKER-ARRAY::SUBSETP-IMPLIES-SUBSETP-APPEND
(172 106 (:REWRITE DEFAULT-CDR))
(152 96 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(130 65 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(98 95 (:REWRITE DEFAULT-CAR))
(65 65 (:TYPE-PRESCRIPTION TRUE-LISTP))
(65 65 (:TYPE-PRESCRIPTION BINARY-APPEND))
)
(PROOF-CHECKER-ARRAY::SET-EQUALP)
(PROOF-CHECKER-ARRAY::UNION
(61 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-EQLABLE-LISTP))
(50 5 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(22 22 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(16 16 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(8 8 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(8 8 (:REWRITE DEFAULT-CDR))
(8 8 (:REWRITE DEFAULT-CAR))
(8 2 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-IMPLIES-EQLABLEP))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP
(34 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(21 3 (:DEFINITION MEMBER-EQUAL))
(7 7 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(6 6 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE
(35 35 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(30 30 (:REWRITE DEFAULT-CAR))
(20 20 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-CONS
(77 77 (:REWRITE DEFAULT-CAR))
(69 69 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(37 37 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-APPEND
(253 205 (:REWRITE DEFAULT-CAR))
(219 177 (:REWRITE DEFAULT-CDR))
(217 217 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(166 83 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(83 83 (:TYPE-PRESCRIPTION TRUE-LISTP))
(83 83 (:TYPE-PRESCRIPTION BINARY-APPEND))
)
(PROOF-CHECKER-ARRAY::SET-EQUAL-VARIABLESP)
(PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES
(34 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(21 3 (:DEFINITION MEMBER-EQUAL))
(7 7 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(6 6 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::EQUAL-SET-DIFFERENCE-VARIABLES-CONS
(131 131 (:REWRITE DEFAULT-CAR))
(113 113 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(73 73 (:REWRITE DEFAULT-CDR))
(53 53 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(13 13 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP
(76 26 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(68 68 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(67 67 (:REWRITE DEFAULT-CAR))
(44 44 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::MEMBER-SET-DIFFERENCE-VARIABLES
(369 369 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(335 328 (:REWRITE DEFAULT-CAR))
(264 258 (:REWRITE DEFAULT-CDR))
(126 126 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::SUBSETP-SET-DIFFERENCE-VARIABLES
(77 55 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(58 56 (:REWRITE DEFAULT-CAR))
(27 1 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-SET-DIFFERENCE-VARIABLES))
(14 14 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-SET-DIFFERENCE-VARIABLES
(1873 274 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(1223 26 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-SET-DIFFERENCE-VARIABLES))
(698 698 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(601 595 (:REWRITE DEFAULT-CAR))
(569 563 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::UNION-VARIABLES
(34 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(21 3 (:DEFINITION MEMBER-EQUAL))
(7 7 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(6 6 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1
(96 94 (:REWRITE DEFAULT-CAR))
(77 77 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(58 56 (:REWRITE DEFAULT-CDR))
(22 22 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(22 22 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES2
(101 101 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(101 101 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(100 92 (:REWRITE DEFAULT-CAR))
(52 50 (:REWRITE DEFAULT-CDR))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES3
(121 121 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(121 121 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(121 113 (:REWRITE DEFAULT-CAR))
(61 59 (:REWRITE DEFAULT-CDR))
(60 8 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES2))
(50 50 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::SUBSETP-UNION-VARIABLES
(140 64 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(71 67 (:REWRITE DEFAULT-CAR))
(64 64 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(28 2 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES3))
(28 2 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES2))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-UNION-VARIABLES
(230 230 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(223 223 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(222 216 (:REWRITE DEFAULT-CAR))
(201 195 (:REWRITE DEFAULT-CDR))
(195 15 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES3))
(195 15 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES2))
)
(PROOF-CHECKER-ARRAY::LITERAL-LISTP-UNION-VARIABLES
(85 85 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(85 85 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(85 83 (:REWRITE DEFAULT-CAR))
(78 6 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES3))
(78 6 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES2))
(60 58 (:REWRITE DEFAULT-CDR))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::EQLABLE-LIST-LISTP)
(PROOF-CHECKER-ARRAY::SUBSETP-LIST
(96 8 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-EQLABLE-LISTP))
(72 8 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(40 40 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(24 24 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(16 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-IMPLIES-EQLABLEP))
(14 14 (:REWRITE DEFAULT-CAR))
(13 13 (:REWRITE DEFAULT-CDR))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::SUBSETP-LIST-APPEND
(683 27 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSETP))
(543 70 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(273 27 (:DEFINITION MEMBER-EQUAL))
(179 89 (:REWRITE DEFAULT-CDR))
(120 60 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(91 91 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(78 78 (:REWRITE DEFAULT-CAR))
(60 60 (:TYPE-PRESCRIPTION TRUE-LISTP))
(60 60 (:TYPE-PRESCRIPTION BINARY-APPEND))
(54 54 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(54 54 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(27 9 (:DEFINITION BINARY-APPEND))
)
(PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP
(10 2 (:DEFINITION MEMBER-EQUAL))
(5 5 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(4 4 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(2 2 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE DEFAULT-CAR))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE
(544 544 (:REWRITE DEFAULT-CAR))
(513 513 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(507 507 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(505 505 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::SET-EQUAL-VARIABLESP-TRANSITIVE
(720 18 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(692 6 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(666 18 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(398 58 (:DEFINITION MEMBER-EQUAL))
(144 144 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(144 48 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(126 126 (:REWRITE DEFAULT-CDR))
(126 126 (:REWRITE DEFAULT-CAR))
(116 116 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(116 116 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(106 106 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(48 48 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(34 2 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(26 2 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(2 2 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
)
|
