Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | 1 : U*v1 = v1 |
2 | 2 : I(v1)*v1 = U | |
3 | 3 : (v3*v2)*v1 = v3*(v2*v1) | |
4 | 4 : A*B = B*A | |
5 | 5 : C*C = U | |
6 | 6 : I(A) = C*(A*I(C)) | |
7 | 7 : C*(B*I(C)) = B | |
8 | 8 : I(v2)*(v2*v1) = v1 | |
9 | 9 : A*(B*v1) = B*(A*v1) | |
10 | 10 : C*(C*v1) = v1 | |
11 | 11 : C*(A*(I(C)*A)) = U | |
12 | 12 : C*(B*(I(C)*v1)) = B*v1 | |
13 | 13 : I(U)*v1 = v1 | |
14 | 14 : I(I(v1))*U = v1 | |
15 | 15 : I(v3*v2)*(v3*(v2*v1)) = v1 | |
16 | 16 : C*(A*(I(C)*(B*A))) = B | |
17 | 17 : I(C)*U = C | |
18 | 18 : C*(A*(I(C)*(A*v1))) = v1 | |
19 | 19 : I(C)*B = B*I(C) | |
20 | 20 : I(I(v2))*v1 = v2*v1 | |
21 | Rule 14 deleted | |
22 | 21 : v1*U = v1 | |
23 | Rule 17 deleted | |
24 | 22 : I(C) = C | |
25 | Rule 19 deleted | |
26 | Rule 18 deleted | |
27 | Rule 16 deleted | |
28 | Rule 12 deleted | |
29 | Rule 11 deleted | |
30 | Rule 7 deleted | |
31 | 23 : C*B = B*C | |
32 | 24 : C*(A*(C*(A*v1))) = v1 | |
33 | 25 : C*(A*(C*(B*A))) = B | |
34 | 26 : C*(B*(C*v1)) = B*v1 | |
35 | 27 : C*(A*(C*A)) = U | |
36 | 28 : C*(B*C) = B | |
37 | 29 : C*(A*(C*(B*(A*v1)))) = B*v1 | |
38 | 30 : I(I(v2*v1)*v2) = v1 | |
39 | 31 : I(v2*I(v1))*v2 = v1 | |
40 | 32 : I(v4*(v3*v2))*(v4*(v3*(v2*v1))) = v1 | |
41 | 33 : I(v1*A)*(v1*(B*A)) = B | |
42 | 34 : I(v1*C)*v1 = C | |
43 | 35 : I(v3*I(v2))*(v3*v1) = v2*v1 | |
44 | 36 : I(v2*A)*(v2*(B*(A*v1))) = B*v1 | |
45 | 37 : I(v2*C)*(v2*v1) = C*v1 | |
46 | 38 : v1*I(v1) = U | |
47 | 39 : I(C*(A*C))*v1 = A*v1 | |
48 | 40 : v2*(I(v2)*v1) = v1 | |
49 | 41 : I(U) = U | |
50 | Rule 13 deleted | |
51 | 42 : I(I(v1)) = v1 | |
52 | Rule 20 deleted | |
53 | 43 : C*(B*v1) = B*(C*v1) | |
54 | Rule 29 deleted | |
55 | Rule 28 deleted | |
56 | Rule 26 deleted | |
57 | Rule 25 deleted | |
58 | 44 : A*(C*(A*v1)) = C*v1 | |
59 | Rule 24 deleted | |
60 | 45 : A*(C*A) = C | |
61 | Rule 27 deleted | |
62 | 46 : v2*(I(v1*v2)*v1) = U | |
63 | 47 : I(I(v3*(v2*v1))*(v3*v2)) = v1 | |
64 | 48 : I(I(B*A)*A) = B | |
65 | 49 : v3*(I(v2*v3)*(v2*v1)) = v1 | |
66 | 50 : I(I(v2)*I(v1)) = v1*v2 | |
67 | 51 : I(I(B*(A*v1))*A) = B*v1 | |
68 | 52 : I(I(v1)*C) = C*v1 | |
69 | 53 : I(v2*I(v1*v2)) = v1 | |
70 | 54 : I(v3*(v2*I(v1)))*(v3*v2) = v1 | |
71 | 55 : I(v1*(C*(A*C)))*v1 = A | |
72 | 56 : v2*I(I(v1)*v2) = v1 | |
73 | 57 : I(v3*(I(v2*v1)*v2))*v3 = v1 | |
74 | 58 : I(v5*(v4*(v3*v2)))*(v5*(v4*(v3*(v2*v1)))) = v1 | |
75 | 59 : I(v2*(v1*A))*(v2*(v1*(B*A))) = B | |
76 | 60 : I(v2*(v1*C))*(v2*v1) = C | |
77 | 61 : I(v4*(v3*I(v2)))*(v4*(v3*v1)) = v2*v1 | |
78 | 62 : I(v3*(v2*A))*(v3*(v2*(B*(A*v1)))) = B*v1 | |
79 | 63 : I(v3*(v2*C))*(v3*(v2*v1)) = C*v1 | |
80 | 64 : I(v4*(I(v3*v2)*v3))*(v4*v1) = v2*v1 | |
81 | 65 : v4*(I(v3*(v2*v4))*(v3*(v2*v1))) = v1 | |
82 | 66 : I(I(B)*A)*A = B | |
83 | 67 : I(A*A)*(B*(A*A)) = B | |
84 | 68 : v1*(I(A*v1)*(B*A)) = B | |
85 | 69 : I(I(v1*A)*(v1*B))*B = A | |
86 | 70 : v1*I(C*v1) = C | |
87 | 71 : I(A*I(v1))*(B*A) = v1*B | |
88 | 72 : I(C*I(v1)) = v1*C | |
89 | 73 : I(v2*(C*(A*C)))*(v2*v1) = A*v1 | |
90 | 74 : I(A*I(v2))*(B*(A*v1)) = v2*(B*v1) | |
91 | 75 : v3*(I(I(v2)*v3)*v1) = v2*v1 | |
92 | 76 : I(I(B*I(v1))*A)*(v1*A) = B | |
93 | 77 : I(v1*A)*(v1*(B*(B*A))) = B*B | |
94 | 78 : I(I(B)*A)*(A*v1) = B*v1 | |
95 | 79 : I(A*A)*(B*(A*(A*v1))) = B*v1 | |
96 | 80 : I(v2*A)*(v2*(B*(B*(A*v1)))) = B*(B*v1) | |
97 | 81 : v2*(I(A*v2)*(B*(A*v1))) = B*v1 | |
98 | 82 : I(I(v2*A)*(v2*B))*(B*v1) = A*v1 | |
99 | 83 : I(I(B*I(v2))*A)*(v2*(A*v1)) = B*v1 | |
100 | 84 : I(A*C)*(B*A) = B*C | |
101 | 85 : I(A*C)*(B*(A*v1)) = B*(C*v1) | |
102 | 86 : v2*(I(C*v2)*v1) = C*v1 | |
103 | 87 : I(I(B*C)*A)*(C*A) = B | |
104 | 88 : I(I(B*C)*A)*(C*(A*v1)) = B*v1 | |
105 | 89 : v2*(v1*I(v2*v1)) = U | |
106 | 90 : B*(A*I(B)) = A | |
107 | 91 : I(v2*v1)*v2 = I(v1) | |
108 | Rule 64 deleted | |
109 | Rule 57 deleted | |
110 | Rule 55 deleted | |
111 | Rule 46 deleted | |
112 | Rule 34 deleted | |
113 | Rule 31 deleted | |
114 | Rule 30 deleted | |
115 | 92 : I(C*(A*C)) = A | |
116 | Rule 39 deleted | |
117 | 93 : I(v3*(v2*v1))*(v3*v2) = I(v1) | |
118 | Rule 60 deleted | |
119 | Rule 54 deleted | |
120 | Rule 47 deleted | |
121 | 94 : I(v2*I(v1)) = v1*I(v2) | |
122 | Rule 83 deleted | |
123 | Rule 76 deleted | |
124 | Rule 74 deleted | |
125 | Rule 72 deleted | |
126 | Rule 71 deleted | |
127 | Rule 53 deleted | |
128 | Rule 50 deleted | |
129 | Rule 35 deleted | |
130 | 95 : I(v2*(I(B)*A))*(v2*(A*v1)) = B*v1 | |
131 | 96 : I(v1*(I(B)*A))*(v1*A) = B | |
132 | 97 : I(v1*A)*(v1*B) = B*(C*(A*C)) | |
133 | Rule 82 deleted | |
134 | Rule 69 deleted | |
135 | 98 : I(v1*C) = C*I(v1) | |
136 | Rule 88 deleted | |
137 | Rule 87 deleted | |
138 | Rule 85 deleted | |
139 | Rule 84 deleted | |
140 | Rule 52 deleted | |
141 | Rule 37 deleted | |
142 | 99 : v3*(v2*(I(v3*v2)*v1)) = v1 | |
143 | 100 : B*(A*(I(B)*v1)) = A*v1 | |
144 | 101 : I(v3*v2)*(v3*v1) = I(v2)*v1 | |
145 | Rule 97 deleted | |
146 | Rule 96 deleted | |
147 | Rule 95 deleted | |
148 | Rule 93 deleted | |
149 | Rule 80 deleted | |
150 | Rule 77 deleted | |
151 | Rule 73 deleted | |
152 | Rule 65 deleted | |
153 | Rule 63 deleted | |
154 | Rule 62 deleted | |
155 | Rule 61 deleted | |
156 | Rule 59 deleted | |
157 | Rule 58 deleted | |
158 | Rule 49 deleted | |
159 | Rule 36 deleted | |
160 | Rule 33 deleted | |
161 | Rule 32 deleted | |
162 | Rule 15 deleted | |
163 | 102 : B*(C*I(B)) = C | |
164 | 103 : B*(C*(I(B)*v1)) = C*v1 | |
165 | 104 : B*(I(B*A)*A) = U | |
166 | 105 : B*(I(B*A)*(A*v1)) = v1 | |
167 | 106 : I(B*A)*A = I(B) | |
168 | Rule 104 deleted | |
169 | Rule 48 deleted | |
170 | 107 : B*(v1*(I(B*(A*v1))*A)) = U | |
171 | 108 : I(I(B*(B*A))*A) = B*B | |
172 | 109 : B*(v2*(I(B*(A*v2))*(A*v1))) = v1 | |
173 | 110 : I(I(B*(B*(A*v1)))*A) = B*(B*v1) | |
174 | 111 : I(I(B)*A) = B*(C*(A*C)) | |
175 | Rule 78 deleted | |
176 | Rule 66 deleted | |
177 | 112 : I(I(B*v1)*A) = B*(C*(A*(C*v1))) | |
178 | Rule 110 deleted | |
179 | Rule 108 deleted | |
180 | Rule 51 deleted | |
181 | 113 : v3*(v2*I(I(v1)*(v3*v2))) = v1 | |
182 | 114 : v1*I(C*(A*(C*v1))) = A | |
183 | 115 : I(I(v2)*v1) = I(v1)*v2 | |
184 | Rule 113 deleted | |
185 | Rule 112 deleted | |
186 | Rule 111 deleted | |
187 | Rule 75 deleted | |
188 | Rule 56 deleted | |
189 | 116 : v2*(v1*(I(A*(v2*v1))*(B*A))) = B | |
190 | 117 : I(A*v1)*(B*A) = I(v1)*B | |
191 | Rule 116 deleted | |
192 | Rule 68 deleted | |
193 | 118 : v2*(v1*I(C*(v2*v1))) = C | |
194 | 119 : I(C*v1) = I(v1)*C | |
195 | Rule 118 deleted | |
196 | Rule 114 deleted | |
197 | Rule 92 deleted | |
198 | Rule 86 deleted | |
199 | Rule 70 deleted | |
200 | 120 : v1*(I(A*(C*v1))*C) = A | |
201 | 121 : I(A*A)*(B*(B*(A*A))) = B*B | |
202 | 122 : I(A*A)*(B*(B*(A*(A*v1)))) = B*(B*v1) | |
203 | 123 : I(A*A)*(B*(A*v1)) = B*(C*(A*(C*v1))) | |
204 | Rule 79 deleted | |
205 | Rule 67 deleted | |
206 | 124 : v3*(v2*(I(A*(v3*v2))*(B*(A*v1)))) = B*v1 | |
207 | 125 : v1*(I(A*v1)*(B*(B*A))) = B*B | |
208 | 126 : I(A*v2)*(B*(A*v1)) = I(v2)*(B*v1) | |
209 | Rule 124 deleted | |
210 | Rule 123 deleted | |
211 | Rule 81 deleted | |
212 | 127 : v3*(v2*(v1*I(v3*(v2*v1)))) = U | |
213 | 128 : v2*I(v1*v2) = I(v1) | |
214 | Rule 89 deleted | |
215 | 129 : A*I(B) = I(B)*A | |
216 | Rule 90 deleted | |
217 | 130 : I(v2*v1) = I(v1)*I(v2) | |
218 | Rule 128 deleted | |
219 | Rule 127 deleted | |
220 | Rule 126 deleted | |
221 | Rule 125 deleted | |
222 | Rule 122 deleted | |
223 | Rule 121 deleted | |
224 | Rule 120 deleted | |
225 | Rule 119 deleted | |
226 | Rule 117 deleted | |
227 | Rule 115 deleted | |
228 | Rule 109 deleted | |
229 | Rule 107 deleted | |
230 | Rule 106 deleted | |
231 | Rule 105 deleted | |
232 | Rule 101 deleted | |
233 | Rule 99 deleted | |
234 | Rule 98 deleted | |
235 | Rule 94 deleted | |
236 | Rule 91 deleted | |
237 | 131 : B*(C*(A*(C*(I(B)*(A*v1))))) = v1 | |
238 | 132 : B*(C*(A*(C*(I(B)*A)))) = U | |
239 | 133 : C*(A*(C*(I(B)*A))) = I(B) | |
240 | Rule 132 deleted | |
241 | 134 : A*(I(B)*v1) = I(B)*(A*v1) | |
242 | Rule 100 deleted | |
243 | 135 : C*I(B) = I(B)*C | |
244 | Rule 102 deleted | |
245 | 136 : C*(I(B)*v1) = I(B)*(C*v1) | |
246 | Rule 133 deleted | |
247 | Rule 131 deleted | |
248 | Rule 103 deleted | |
249 | Canonical set found : | |
250 | 1 : U*v1 = v1 | |
251 | 2 : I(v1)*v1 = U | |
252 | 3 : (v3*v2)*v1 = v3*(v2*v1) | |
253 | 4 : A*B = B*A | |
254 | 5 : C*C = U | |
255 | 6 : I(A) = C*(A*C) | |
256 | 8 : I(v2)*(v2*v1) = v1 | |
257 | 9 : A*(B*v1) = B*(A*v1) | |
258 | 10 : C*(C*v1) = v1 | |
259 | 21 : v1*U = v1 | |
260 | 22 : I(C) = C | |
261 | 23 : C*B = B*C | |
262 | 38 : v1*I(v1) = U | |
263 | 40 : v2*(I(v2)*v1) = v1 | |
264 | 41 : I(U) = U | |
265 | 42 : I(I(v1)) = v1 | |
266 | 43 : C*(B*v1) = B*(C*v1) | |
267 | 44 : A*(C*(A*v1)) = C*v1 | |
268 | 45 : A*(C*A) = C | |
269 | 129 : A*I(B) = I(B)*A | |
270 | 130 : I(v2*v1) = I(v1)*I(v2) | |
271 | 134 : A*(I(B)*v1) = I(B)*(A*v1) | |
272 | 135 : C*I(B) = I(B)*C | |
273 | 136 : C*(I(B)*v1) = I(B)*(C*v1) | |
274 | 1 : U*v1 = v1 | |
275 | 2 : I(v1)*v1 = U | |
276 | 3 : (v3*v2)*v1 = v3*(v2*v1) | |
277 | 4 : A*B = B*A | |
278 | 5 : C*C = U | |
279 | 6 : I(A) = C*(A*I(C)) | |
280 | 7 : C*(B*I(C)) = B | |
281 | 8 : I(v2)*(v2*v1) = v1 | |
282 | 9 : A*(B*v1) = B*(A*v1) | |
283 | 10 : C*(C*v1) = v1 | |
284 | 11 : C*(A*(I(C)*A)) = U | |
285 | 12 : C*(B*(I(C)*v1)) = B*v1 | |
286 | 13 : I(U)*v1 = v1 | |
287 | 14 : I(I(v1))*U = v1 | |
288 | 15 : I(v3*v2)*(v3*(v2*v1)) = v1 | |
289 | 16 : C*(A*(I(C)*(B*A))) = B | |
290 | 17 : I(C)*U = C | |
291 | 18 : C*(A*(I(C)*(A*v1))) = v1 | |
292 | 19 : I(C)*B = B*I(C) | |
293 | 20 : I(I(v2))*v1 = v2*v1 | |
294 | Rule 14 deleted | |
295 | 21 : v1*U = v1 | |
296 | Rule 17 deleted | |
297 | 22 : I(C) = C | |
298 | Rule 19 deleted | |
299 | Rule 18 deleted | |
300 | Rule 16 deleted | |
301 | Rule 12 deleted | |
302 | Rule 11 deleted | |
303 | Rule 7 deleted | |
304 | 23 : C*B = B*C | |
305 | 24 : C*(A*(C*(A*v1))) = v1 | |
306 | 25 : C*(A*(C*(B*A))) = B | |
307 | 26 : C*(B*(C*v1)) = B*v1 | |
308 | 27 : C*(A*(C*A)) = U | |
309 | 28 : C*(B*C) = B | |
310 | 29 : C*(A*(C*(B*(A*v1)))) = B*v1 | |
311 | 30 : I(I(v2*v1)*v2) = v1 | |
312 | 31 : I(v2*I(v1))*v2 = v1 | |
313 | 32 : I(v4*(v3*v2))*(v4*(v3*(v2*v1))) = v1 | |
314 | 33 : I(v1*A)*(v1*(B*A)) = B | |
315 | 34 : I(v1*C)*v1 = C | |
316 | 35 : I(v3*I(v2))*(v3*v1) = v2*v1 | |
317 | 36 : I(v2*A)*(v2*(B*(A*v1))) = B*v1 | |
318 | 37 : I(v2*C)*(v2*v1) = C*v1 | |
319 | 38 : v1*I(v1) = U | |
320 | 39 : I(C*(A*C))*v1 = A*v1 | |
321 | 40 : v2*(I(v2)*v1) = v1 | |
322 | 41 : I(U) = U | |
323 | Rule 13 deleted | |
324 | 42 : I(I(v1)) = v1 | |
325 | Rule 20 deleted | |
326 | 43 : C*(B*v1) = B*(C*v1) | |
327 | Rule 29 deleted | |
328 | Rule 28 deleted | |
329 | Rule 26 deleted | |
330 | Rule 25 deleted | |
331 | 44 : A*(C*(A*v1)) = C*v1 | |
332 | Rule 24 deleted | |
333 | 45 : A*(C*A) = C | |
334 | Rule 27 deleted | |
335 | 46 : v2*(I(v1*v2)*v1) = U | |
336 | 47 : I(I(v3*(v2*v1))*(v3*v2)) = v1 | |
337 | 48 : I(I(B*A)*A) = B | |
338 | 49 : v3*(I(v2*v3)*(v2*v1)) = v1 | |
339 | 50 : I(I(v2)*I(v1)) = v1*v2 | |
340 | 51 : I(I(B*(A*v1))*A) = B*v1 | |
341 | 52 : I(I(v1)*C) = C*v1 | |
342 | 53 : I(v2*I(v1*v2)) = v1 | |
343 | 54 : I(v3*(v2*I(v1)))*(v3*v2) = v1 | |
344 | 55 : I(v1*(C*(A*C)))*v1 = A | |
345 | 56 : v2*I(I(v1)*v2) = v1 | |
346 | 57 : I(v3*(I(v2*v1)*v2))*v3 = v1 | |
347 | 58 : I(v5*(v4*(v3*v2)))*(v5*(v4*(v3*(v2*v1)))) = v1 | |
348 | 59 : I(v2*(v1*A))*(v2*(v1*(B*A))) = B | |
349 | 60 : I(v2*(v1*C))*(v2*v1) = C | |
350 | 61 : I(v4*(v3*I(v2)))*(v4*(v3*v1)) = v2*v1 | |
351 | 62 : I(v3*(v2*A))*(v3*(v2*(B*(A*v1)))) = B*v1 | |
352 | 63 : I(v3*(v2*C))*(v3*(v2*v1)) = C*v1 | |
353 | 64 : I(v4*(I(v3*v2)*v3))*(v4*v1) = v2*v1 | |
354 | 65 : v4*(I(v3*(v2*v4))*(v3*(v2*v1))) = v1 | |
355 | 66 : I(I(B)*A)*A = B | |
356 | 67 : I(A*A)*(B*(A*A)) = B | |
357 | 68 : v1*(I(A*v1)*(B*A)) = B | |
358 | 69 : I(I(v1*A)*(v1*B))*B = A | |
359 | 70 : v1*I(C*v1) = C | |
360 | 71 : I(A*I(v1))*(B*A) = v1*B | |
361 | 72 : I(C*I(v1)) = v1*C | |
362 | 73 : I(v2*(C*(A*C)))*(v2*v1) = A*v1 | |
363 | 74 : I(A*I(v2))*(B*(A*v1)) = v2*(B*v1) | |
364 | 75 : v3*(I(I(v2)*v3)*v1) = v2*v1 | |
365 | 76 : I(I(B*I(v1))*A)*(v1*A) = B | |
366 | 77 : I(v1*A)*(v1*(B*(B*A))) = B*B | |
367 | 78 : I(I(B)*A)*(A*v1) = B*v1 | |
368 | 79 : I(A*A)*(B*(A*(A*v1))) = B*v1 | |
369 | 80 : I(v2*A)*(v2*(B*(B*(A*v1)))) = B*(B*v1) | |
370 | 81 : v2*(I(A*v2)*(B*(A*v1))) = B*v1 | |
371 | 82 : I(I(v2*A)*(v2*B))*(B*v1) = A*v1 | |
372 | 83 : I(I(B*I(v2))*A)*(v2*(A*v1)) = B*v1 | |
373 | 84 : I(A*C)*(B*A) = B*C | |
374 | 85 : I(A*C)*(B*(A*v1)) = B*(C*v1) | |
375 | 86 : v2*(I(C*v2)*v1) = C*v1 | |
376 | 87 : I(I(B*C)*A)*(C*A) = B | |
377 | 88 : I(I(B*C)*A)*(C*(A*v1)) = B*v1 | |
378 | 89 : v2*(v1*I(v2*v1)) = U | |
379 | 90 : B*(A*I(B)) = A | |
380 | 91 : I(v2*v1)*v2 = I(v1) | |
381 | Rule 64 deleted | |
382 | Rule 57 deleted | |
383 | Rule 55 deleted | |
384 | Rule 46 deleted | |
385 | Rule 34 deleted | |
386 | Rule 31 deleted | |
387 | Rule 30 deleted | |
388 | 92 : I(C*(A*C)) = A | |
389 | Rule 39 deleted | |
390 | 93 : I(v3*(v2*v1))*(v3*v2) = I(v1) | |
391 | Rule 60 deleted | |
392 | Rule 54 deleted | |
393 | Rule 47 deleted | |
394 | 94 : I(v2*I(v1)) = v1*I(v2) | |
395 | Rule 83 deleted | |
396 | Rule 76 deleted | |
397 | Rule 74 deleted | |
398 | Rule 72 deleted | |
399 | Rule 71 deleted | |
400 | Rule 53 deleted | |
401 | Rule 50 deleted | |
402 | Rule 35 deleted | |
403 | 95 : I(v2*(I(B)*A))*(v2*(A*v1)) = B*v1 | |
404 | 96 : I(v1*(I(B)*A))*(v1*A) = B | |
405 | 97 : I(v1*A)*(v1*B) = B*(C*(A*C)) | |
406 | Rule 82 deleted | |
407 | Rule 69 deleted | |
408 | 98 : I(v1*C) = C*I(v1) | |
409 | Rule 88 deleted | |
410 | Rule 87 deleted | |
411 | Rule 85 deleted | |
412 | Rule 84 deleted | |
413 | Rule 52 deleted | |
414 | Rule 37 deleted | |
415 | 99 : v3*(v2*(I(v3*v2)*v1)) = v1 | |
416 | 100 : B*(A*(I(B)*v1)) = A*v1 | |
417 | 101 : I(v3*v2)*(v3*v1) = I(v2)*v1 | |
418 | Rule 97 deleted | |
419 | Rule 96 deleted | |
420 | Rule 95 deleted | |
421 | Rule 93 deleted | |
422 | Rule 80 deleted | |
423 | Rule 77 deleted | |
424 | Rule 73 deleted | |
425 | Rule 65 deleted | |
426 | Rule 63 deleted | |
427 | Rule 62 deleted | |
428 | Rule 61 deleted | |
429 | Rule 59 deleted | |
430 | Rule 58 deleted | |
431 | Rule 49 deleted | |
432 | Rule 36 deleted | |
433 | Rule 33 deleted | |
434 | Rule 32 deleted | |
435 | Rule 15 deleted | |
436 | 102 : B*(C*I(B)) = C | |
437 | 103 : B*(C*(I(B)*v1)) = C*v1 | |
438 | 104 : B*(I(B*A)*A) = U | |
439 | 105 : B*(I(B*A)*(A*v1)) = v1 | |
440 | 106 : I(B*A)*A = I(B) | |
441 | Rule 104 deleted | |
442 | Rule 48 deleted | |
443 | 107 : B*(v1*(I(B*(A*v1))*A)) = U | |
444 | 108 : I(I(B*(B*A))*A) = B*B | |
445 | 109 : B*(v2*(I(B*(A*v2))*(A*v1))) = v1 | |
446 | 110 : I(I(B*(B*(A*v1)))*A) = B*(B*v1) | |
447 | 111 : I(I(B)*A) = B*(C*(A*C)) | |
448 | Rule 78 deleted | |
449 | Rule 66 deleted | |
450 | 112 : I(I(B*v1)*A) = B*(C*(A*(C*v1))) | |
451 | Rule 110 deleted | |
452 | Rule 108 deleted | |
453 | Rule 51 deleted | |
454 | 113 : v3*(v2*I(I(v1)*(v3*v2))) = v1 | |
455 | 114 : v1*I(C*(A*(C*v1))) = A | |
456 | 115 : I(I(v2)*v1) = I(v1)*v2 | |
457 | Rule 113 deleted | |
458 | Rule 112 deleted | |
459 | Rule 111 deleted | |
460 | Rule 75 deleted | |
461 | Rule 56 deleted | |
462 | 116 : v2*(v1*(I(A*(v2*v1))*(B*A))) = B | |
463 | 117 : I(A*v1)*(B*A) = I(v1)*B | |
464 | Rule 116 deleted | |
465 | Rule 68 deleted | |
466 | 118 : v2*(v1*I(C*(v2*v1))) = C | |
467 | 119 : I(C*v1) = I(v1)*C | |
468 | Rule 118 deleted | |
469 | Rule 114 deleted | |
470 | Rule 92 deleted | |
471 | Rule 86 deleted | |
472 | Rule 70 deleted | |
473 | 120 : v1*(I(A*(C*v1))*C) = A | |
474 | 121 : I(A*A)*(B*(B*(A*A))) = B*B | |
475 | 122 : I(A*A)*(B*(B*(A*(A*v1)))) = B*(B*v1) | |
476 | 123 : I(A*A)*(B*(A*v1)) = B*(C*(A*(C*v1))) | |
477 | Rule 79 deleted | |
478 | Rule 67 deleted | |
479 | 124 : v3*(v2*(I(A*(v3*v2))*(B*(A*v1)))) = B*v1 | |
480 | 125 : v1*(I(A*v1)*(B*(B*A))) = B*B | |
481 | 126 : I(A*v2)*(B*(A*v1)) = I(v2)*(B*v1) | |
482 | Rule 124 deleted | |
483 | Rule 123 deleted | |
484 | Rule 81 deleted | |
485 | 127 : v3*(v2*(v1*I(v3*(v2*v1)))) = U | |
486 | 128 : v2*I(v1*v2) = I(v1) | |
487 | Rule 89 deleted | |
488 | 129 : A*I(B) = I(B)*A | |
489 | Rule 90 deleted | |
490 | 130 : I(v2*v1) = I(v1)*I(v2) | |
491 | Rule 128 deleted | |
492 | Rule 127 deleted | |
493 | Rule 126 deleted | |
494 | Rule 125 deleted | |
495 | Rule 122 deleted | |
496 | Rule 121 deleted | |
497 | Rule 120 deleted | |
498 | Rule 119 deleted | |
499 | Rule 117 deleted | |
500 | Rule 115 deleted | |
501 | Rule 109 deleted | |
502 | Rule 107 deleted | |
503 | Rule 106 deleted | |
504 | Rule 105 deleted | |
505 | Rule 101 deleted | |
506 | Rule 99 deleted | |
507 | Rule 98 deleted | |
508 | Rule 94 deleted | |
509 | Rule 91 deleted | |
510 | 131 : B*(C*(A*(C*(I(B)*(A*v1))))) = v1 | |
511 | 132 : B*(C*(A*(C*(I(B)*A)))) = U | |
512 | 133 : C*(A*(C*(I(B)*A))) = I(B) | |
513 | Rule 132 deleted | |
514 | 134 : A*(I(B)*v1) = I(B)*(A*v1) | |
515 | Rule 100 deleted | |
516 | 135 : C*I(B) = I(B)*C | |
517 | Rule 102 deleted | |
518 | 136 : C*(I(B)*v1) = I(B)*(C*v1) | |
519 | Rule 133 deleted | |
520 | Rule 131 deleted | |
521 | Rule 103 deleted | |
522 | Canonical set found : | |
523 | 1 : U*v1 = v1 | |
524 | 2 : I(v1)*v1 = U | |
525 | 3 : (v3*v2)*v1 = v3*(v2*v1) | |
526 | 4 : A*B = B*A | |
527 | 5 : C*C = U | |
528 | 6 : I(A) = C*(A*C) | |
529 | 8 : I(v2)*(v2*v1) = v1 | |
530 | 9 : A*(B*v1) = B*(A*v1) | |
531 | 10 : C*(C*v1) = v1 | |
532 | 21 : v1*U = v1 | |
533 | 22 : I(C) = C | |
534 | 23 : C*B = B*C | |
535 | 38 : v1*I(v1) = U | |
536 | 40 : v2*(I(v2)*v1) = v1 | |
537 | 41 : I(U) = U | |
538 | 42 : I(I(v1)) = v1 | |
539 | 43 : C*(B*v1) = B*(C*v1) | |
540 | 44 : A*(C*(A*v1)) = C*v1 | |
541 | 45 : A*(C*A) = C | |
542 | 129 : A*I(B) = I(B)*A | |
543 | 130 : I(v2*v1) = I(v1)*I(v2) | |
544 | 134 : A*(I(B)*v1) = I(B)*(A*v1) | |
545 | 135 : C*I(B) = I(B)*C | |
546 | 136 : C*(I(B)*v1) = I(B)*(C*v1) | |
547 | 1 : U*v1 = v1 | |
548 | 2 : I(v1)*v1 = U | |
549 | 3 : (v3*v2)*v1 = v3*(v2*v1) | |
550 | 4 : A*B = B*A | |
551 | 5 : C*C = U | |
552 | 6 : I(A) = C*(A*I(C)) | |
553 | 7 : C*(B*I(C)) = B | |
554 | 8 : I(v2)*(v2*v1) = v1 | |
555 | 9 : A*(B*v1) = B*(A*v1) | |
556 | 10 : C*(C*v1) = v1 | |
557 | 11 : C*(A*(I(C)*A)) = U | |
558 | 12 : C*(B*(I(C)*v1)) = B*v1 | |
559 | 13 : I(U)*v1 = v1 | |
560 | 14 : I(I(v1))*U = v1 | |
561 | 15 : I(v3*v2)*(v3*(v2*v1)) = v1 | |
562 | 16 : C*(A*(I(C)*(B*A))) = B | |
563 | 17 : I(C)*U = C | |
564 | 18 : C*(A*(I(C)*(A*v1))) = v1 | |
565 | 19 : I(C)*B = B*I(C) | |
566 | 20 : I(I(v2))*v1 = v2*v1 | |
567 | Rule 14 deleted | |
568 | 21 : v1*U = v1 | |
569 | Rule 17 deleted | |
570 | 22 : I(C) = C | |
571 | Rule 19 deleted | |
572 | Rule 18 deleted | |
573 | Rule 16 deleted | |
574 | Rule 12 deleted | |
575 | Rule 11 deleted | |
576 | Rule 7 deleted | |
577 | 23 : C*B = B*C | |
578 | 24 : C*(A*(C*(A*v1))) = v1 | |
579 | 25 : C*(A*(C*(B*A))) = B | |
580 | 26 : C*(B*(C*v1)) = B*v1 | |
581 | 27 : C*(A*(C*A)) = U | |
582 | 28 : C*(B*C) = B | |
583 | 29 : C*(A*(C*(B*(A*v1)))) = B*v1 | |
584 | 30 : I(I(v2*v1)*v2) = v1 | |
585 | 31 : I(v2*I(v1))*v2 = v1 | |
586 | 32 : I(v4*(v3*v2))*(v4*(v3*(v2*v1))) = v1 | |
587 | 33 : I(v1*A)*(v1*(B*A)) = B | |
588 | 34 : I(v1*C)*v1 = C | |
589 | 35 : I(v3*I(v2))*(v3*v1) = v2*v1 | |
590 | 36 : I(v2*A)*(v2*(B*(A*v1))) = B*v1 | |
591 | 37 : I(v2*C)*(v2*v1) = C*v1 | |
592 | 38 : v1*I(v1) = U | |
593 | 39 : I(C*(A*C))*v1 = A*v1 | |
594 | 40 : v2*(I(v2)*v1) = v1 | |
595 | 41 : I(U) = U | |
596 | Rule 13 deleted | |
597 | 42 : I(I(v1)) = v1 | |
598 | Rule 20 deleted | |
599 | 43 : C*(B*v1) = B*(C*v1) | |
600 | Rule 29 deleted | |
601 | Rule 28 deleted | |
602 | Rule 26 deleted | |
603 | Rule 25 deleted | |
604 | 44 : A*(C*(A*v1)) = C*v1 | |
605 | Rule 24 deleted | |
606 | 45 : A*(C*A) = C | |
607 | Rule 27 deleted | |
608 | 46 : v2*(I(v1*v2)*v1) = U | |
609 | 47 : I(I(v3*(v2*v1))*(v3*v2)) = v1 | |
610 | 48 : I(I(B*A)*A) = B | |
611 | 49 : v3*(I(v2*v3)*(v2*v1)) = v1 | |
612 | 50 : I(I(v2)*I(v1)) = v1*v2 | |
613 | 51 : I(I(B*(A*v1))*A) = B*v1 | |
614 | 52 : I(I(v1)*C) = C*v1 | |
615 | 53 : I(v2*I(v1*v2)) = v1 | |
616 | 54 : I(v3*(v2*I(v1)))*(v3*v2) = v1 | |
617 | 55 : I(v1*(C*(A*C)))*v1 = A | |
618 | 56 : v2*I(I(v1)*v2) = v1 | |
619 | 57 : I(v3*(I(v2*v1)*v2))*v3 = v1 | |
620 | 58 : I(v5*(v4*(v3*v2)))*(v5*(v4*(v3*(v2*v1)))) = v1 | |
621 | 59 : I(v2*(v1*A))*(v2*(v1*(B*A))) = B | |
622 | 60 : I(v2*(v1*C))*(v2*v1) = C | |
623 | 61 : I(v4*(v3*I(v2)))*(v4*(v3*v1)) = v2*v1 | |
624 | 62 : I(v3*(v2*A))*(v3*(v2*(B*(A*v1)))) = B*v1 | |
625 | 63 : I(v3*(v2*C))*(v3*(v2*v1)) = C*v1 | |
626 | 64 : I(v4*(I(v3*v2)*v3))*(v4*v1) = v2*v1 | |
627 | 65 : v4*(I(v3*(v2*v4))*(v3*(v2*v1))) = v1 | |
628 | 66 : I(I(B)*A)*A = B | |
629 | 67 : I(A*A)*(B*(A*A)) = B | |
630 | 68 : v1*(I(A*v1)*(B*A)) = B | |
631 | 69 : I(I(v1*A)*(v1*B))*B = A | |
632 | 70 : v1*I(C*v1) = C | |
633 | 71 : I(A*I(v1))*(B*A) = v1*B | |
634 | 72 : I(C*I(v1)) = v1*C | |
635 | 73 : I(v2*(C*(A*C)))*(v2*v1) = A*v1 | |
636 | 74 : I(A*I(v2))*(B*(A*v1)) = v2*(B*v1) | |
637 | 75 : v3*(I(I(v2)*v3)*v1) = v2*v1 | |
638 | 76 : I(I(B*I(v1))*A)*(v1*A) = B | |
639 | 77 : I(v1*A)*(v1*(B*(B*A))) = B*B | |
640 | 78 : I(I(B)*A)*(A*v1) = B*v1 | |
641 | 79 : I(A*A)*(B*(A*(A*v1))) = B*v1 | |
642 | 80 : I(v2*A)*(v2*(B*(B*(A*v1)))) = B*(B*v1) | |
643 | 81 : v2*(I(A*v2)*(B*(A*v1))) = B*v1 | |
644 | 82 : I(I(v2*A)*(v2*B))*(B*v1) = A*v1 | |
645 | 83 : I(I(B*I(v2))*A)*(v2*(A*v1)) = B*v1 | |
646 | 84 : I(A*C)*(B*A) = B*C | |
647 | 85 : I(A*C)*(B*(A*v1)) = B*(C*v1) | |
648 | 86 : v2*(I(C*v2)*v1) = C*v1 | |
649 | 87 : I(I(B*C)*A)*(C*A) = B | |
650 | 88 : I(I(B*C)*A)*(C*(A*v1)) = B*v1 | |
651 | 89 : v2*(v1*I(v2*v1)) = U | |
652 | 90 : B*(A*I(B)) = A | |
653 | 91 : I(v2*v1)*v2 = I(v1) | |
654 | Rule 64 deleted | |
655 | Rule 57 deleted | |
656 | Rule 55 deleted | |
657 | Rule 46 deleted | |
658 | Rule 34 deleted | |
659 | Rule 31 deleted | |
660 | Rule 30 deleted | |
661 | 92 : I(C*(A*C)) = A | |
662 | Rule 39 deleted | |
663 | 93 : I(v3*(v2*v1))*(v3*v2) = I(v1) | |
664 | Rule 60 deleted | |
665 | Rule 54 deleted | |
666 | Rule 47 deleted | |
667 | 94 : I(v2*I(v1)) = v1*I(v2) | |
668 | Rule 83 deleted | |
669 | Rule 76 deleted | |
670 | Rule 74 deleted | |
671 | Rule 72 deleted | |
672 | Rule 71 deleted | |
673 | Rule 53 deleted | |
674 | Rule 50 deleted | |
675 | Rule 35 deleted | |
676 | 95 : I(v2*(I(B)*A))*(v2*(A*v1)) = B*v1 | |
677 | 96 : I(v1*(I(B)*A))*(v1*A) = B | |
678 | 97 : I(v1*A)*(v1*B) = B*(C*(A*C)) | |
679 | Rule 82 deleted | |
680 | Rule 69 deleted | |
681 | 98 : I(v1*C) = C*I(v1) | |
682 | Rule 88 deleted | |
683 | Rule 87 deleted | |
684 | Rule 85 deleted | |
685 | Rule 84 deleted | |
686 | Rule 52 deleted | |
687 | Rule 37 deleted | |
688 | 99 : v3*(v2*(I(v3*v2)*v1)) = v1 | |
689 | 100 : B*(A*(I(B)*v1)) = A*v1 | |
690 | 101 : I(v3*v2)*(v3*v1) = I(v2)*v1 | |
691 | Rule 97 deleted | |
692 | Rule 96 deleted | |
693 | Rule 95 deleted | |
694 | Rule 93 deleted | |
695 | Rule 80 deleted | |
696 | Rule 77 deleted | |
697 | Rule 73 deleted | |
698 | Rule 65 deleted | |
699 | Rule 63 deleted | |
700 | Rule 62 deleted | |
701 | Rule 61 deleted | |
702 | Rule 59 deleted | |
703 | Rule 58 deleted | |
704 | Rule 49 deleted | |
705 | Rule 36 deleted | |
706 | Rule 33 deleted | |
707 | Rule 32 deleted | |
708 | Rule 15 deleted | |
709 | 102 : B*(C*I(B)) = C | |
710 | 103 : B*(C*(I(B)*v1)) = C*v1 | |
711 | 104 : B*(I(B*A)*A) = U | |
712 | 105 : B*(I(B*A)*(A*v1)) = v1 | |
713 | 106 : I(B*A)*A = I(B) | |
714 | Rule 104 deleted | |
715 | Rule 48 deleted | |
716 | 107 : B*(v1*(I(B*(A*v1))*A)) = U | |
717 | 108 : I(I(B*(B*A))*A) = B*B | |
718 | 109 : B*(v2*(I(B*(A*v2))*(A*v1))) = v1 | |
719 | 110 : I(I(B*(B*(A*v1)))*A) = B*(B*v1) | |
720 | 111 : I(I(B)*A) = B*(C*(A*C)) | |
721 | Rule 78 deleted | |
722 | Rule 66 deleted | |
723 | 112 : I(I(B*v1)*A) = B*(C*(A*(C*v1))) | |
724 | Rule 110 deleted | |
725 | Rule 108 deleted | |
726 | Rule 51 deleted | |
727 | 113 : v3*(v2*I(I(v1)*(v3*v2))) = v1 | |
728 | 114 : v1*I(C*(A*(C*v1))) = A | |
729 | 115 : I(I(v2)*v1) = I(v1)*v2 | |
730 | Rule 113 deleted | |
731 | Rule 112 deleted | |
732 | Rule 111 deleted | |
733 | Rule 75 deleted | |
734 | Rule 56 deleted | |
735 | 116 : v2*(v1*(I(A*(v2*v1))*(B*A))) = B | |
736 | 117 : I(A*v1)*(B*A) = I(v1)*B | |
737 | Rule 116 deleted | |
738 | Rule 68 deleted | |
739 | 118 : v2*(v1*I(C*(v2*v1))) = C | |
740 | 119 : I(C*v1) = I(v1)*C | |
741 | Rule 118 deleted | |
742 | Rule 114 deleted | |
743 | Rule 92 deleted | |
744 | Rule 86 deleted | |
745 | Rule 70 deleted | |
746 | 120 : v1*(I(A*(C*v1))*C) = A | |
747 | 121 : I(A*A)*(B*(B*(A*A))) = B*B | |
748 | 122 : I(A*A)*(B*(B*(A*(A*v1)))) = B*(B*v1) | |
749 | 123 : I(A*A)*(B*(A*v1)) = B*(C*(A*(C*v1))) | |
750 | Rule 79 deleted | |
751 | Rule 67 deleted | |
752 | 124 : v3*(v2*(I(A*(v3*v2))*(B*(A*v1)))) = B*v1 | |
753 | 125 : v1*(I(A*v1)*(B*(B*A))) = B*B | |
754 | 126 : I(A*v2)*(B*(A*v1)) = I(v2)*(B*v1) | |
755 | Rule 124 deleted | |
756 | Rule 123 deleted | |
757 | Rule 81 deleted | |
758 | 127 : v3*(v2*(v1*I(v3*(v2*v1)))) = U | |
759 | 128 : v2*I(v1*v2) = I(v1) | |
760 | Rule 89 deleted | |
761 | 129 : A*I(B) = I(B)*A | |
762 | Rule 90 deleted | |
763 | 130 : I(v2*v1) = I(v1)*I(v2) | |
764 | Rule 128 deleted | |
765 | Rule 127 deleted | |
766 | Rule 126 deleted | |
767 | Rule 125 deleted | |
768 | Rule 122 deleted | |
769 | Rule 121 deleted | |
770 | Rule 120 deleted | |
771 | Rule 119 deleted | |
772 | Rule 117 deleted | |
773 | Rule 115 deleted | |
774 | Rule 109 deleted | |
775 | Rule 107 deleted | |
776 | Rule 106 deleted | |
777 | Rule 105 deleted | |
778 | Rule 101 deleted | |
779 | Rule 99 deleted | |
780 | Rule 98 deleted | |
781 | Rule 94 deleted | |
782 | Rule 91 deleted | |
783 | 131 : B*(C*(A*(C*(I(B)*(A*v1))))) = v1 | |
784 | 132 : B*(C*(A*(C*(I(B)*A)))) = U | |
785 | 133 : C*(A*(C*(I(B)*A))) = I(B) | |
786 | Rule 132 deleted | |
787 | 134 : A*(I(B)*v1) = I(B)*(A*v1) | |
788 | Rule 100 deleted | |
789 | 135 : C*I(B) = I(B)*C | |
790 | Rule 102 deleted | |
791 | 136 : C*(I(B)*v1) = I(B)*(C*v1) | |
792 | Rule 133 deleted | |
793 | Rule 131 deleted | |
794 | Rule 103 deleted | |
795 | Canonical set found : | |
796 | 1 : U*v1 = v1 | |
797 | 2 : I(v1)*v1 = U | |
798 | 3 : (v3*v2)*v1 = v3*(v2*v1) | |
799 | 4 : A*B = B*A | |
800 | 5 : C*C = U | |
801 | 6 : I(A) = C*(A*C) | |
802 | 8 : I(v2)*(v2*v1) = v1 | |
803 | 9 : A*(B*v1) = B*(A*v1) | |
804 | 10 : C*(C*v1) = v1 | |
805 | 21 : v1*U = v1 | |
806 | 22 : I(C) = C | |
807 | 23 : C*B = B*C | |
808 | 38 : v1*I(v1) = U | |
809 | 40 : v2*(I(v2)*v1) = v1 | |
810 | 41 : I(U) = U | |
811 | 42 : I(I(v1)) = v1 | |
812 | 43 : C*(B*v1) = B*(C*v1) | |
813 | 44 : A*(C*(A*v1)) = C*v1 | |
814 | 45 : A*(C*A) = C | |
815 | 129 : A*I(B) = I(B)*A | |
816 | 130 : I(v2*v1) = I(v1)*I(v2) | |
817 | 134 : A*(I(B)*v1) = I(B)*(A*v1) | |
818 | 135 : C*I(B) = I(B)*C | |
819 | 136 : C*(I(B)*v1) = I(B)*(C*v1) |