Created
January 7, 2018 15:26
-
-
Save gebner/9ceb13e4cb8852d96b332aeb0f16314b to your computer and use it in GitHub Desktop.
char_zero_lt_d800.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
1 #NS 0 u | |
2 #NS 0 eq | |
3 #NS 0 α | |
1 #UP 1 | |
0 #ES 1 | |
4 #NS 0 a | |
1 #EV 0 | |
2 #EV 1 | |
3 #ES 0 | |
4 #EP #BD 4 2 3 | |
5 #EP #BD 4 1 4 | |
6 #EP #BI 3 0 5 | |
5 #NS 2 refl | |
7 #EC 2 1 | |
8 #EA 7 2 | |
9 #EA 8 1 | |
10 #EA 9 1 | |
11 #EP #BD 4 1 10 | |
12 #EP #BI 3 0 11 | |
#IND 2 2 6 1 5 12 1 | |
#QUOT | |
6 #NS 0 char | |
7 #NS 6 zero_lt_d800 | |
8 #NS 0 has_lt | |
9 #NS 8 lt | |
2 #US 1 | |
13 #ES 2 | |
14 #EP #BD 3 13 13 | |
10 #NS 8 mk | |
11 #NS 0 lt | |
15 #EC 8 1 | |
16 #EA 15 2 | |
17 #EP #BD 11 5 16 | |
18 #EP #BI 3 13 17 | |
#IND 1 8 14 1 10 18 1 | |
12 #NS 0 c | |
19 #EA 15 1 | |
20 #EV 2 | |
21 #EP #BD 4 20 3 | |
22 #EP #BD 4 2 21 | |
23 #EP #BC 12 19 22 | |
24 #EP #BI 3 13 23 | |
13 #NS 8 rec | |
3 #US 0 | |
4 #UM 2 3 | |
25 #EC 13 4 1 | |
26 #EA 25 2 | |
27 #EV 3 | |
28 #EP #BD 4 27 3 | |
29 #EP #BD 4 20 28 | |
30 #EL #BC 12 16 29 | |
31 #EA 26 30 | |
32 #EL #BD 11 22 1 | |
33 #EA 31 32 | |
34 #EA 33 1 | |
35 #EL #BC 12 19 34 | |
36 #EL #BD 3 13 35 | |
#DEF 9 24 36 1 | |
14 #NS 0 nat | |
37 #ES 3 | |
15 #NS 14 zero | |
38 #EC 14 | |
16 #NS 14 succ | |
17 #NS 0 n | |
39 #EP #BD 17 38 38 | |
#IND 0 14 37 2 15 38 16 39 | |
18 #NS 14 has_lt | |
19 #NS 14 lt | |
20 #NS 14 less_than_or_equal | |
40 #EP #BD 4 38 3 | |
41 #EP #BD 4 38 40 | |
21 #NS 20 refl | |
42 #EC 20 | |
43 #EA 42 1 | |
44 #EA 43 1 | |
45 #EP #BD 4 38 44 | |
22 #NS 20 step | |
23 #NS 0 b | |
46 #EA 42 2 | |
47 #EA 46 1 | |
48 #EA 42 20 | |
49 #EC 16 | |
50 #EA 49 2 | |
51 #EA 48 50 | |
52 #EP #BD 4 47 51 | |
53 #EP #BI 23 38 52 | |
54 #EP #BI 4 38 53 | |
#IND 1 20 41 2 21 45 22 54 | |
24 #NS 0 m | |
55 #EP #BD 24 38 3 | |
56 #EP #BD 17 38 55 | |
57 #EA 42 50 | |
58 #EA 57 1 | |
59 #EL #BD 24 38 58 | |
60 #EL #BD 17 38 59 | |
#DEF 19 56 60 | |
61 #EC 8 0 | |
62 #EA 61 38 | |
63 #EC 10 0 | |
64 #EA 63 38 | |
65 #EC 19 | |
66 #EA 64 65 | |
#DEF 18 62 66 | |
25 #NS 0 has_zero | |
26 #NS 25 zero | |
27 #NS 25 mk | |
28 #NS 0 zero | |
67 #EC 25 1 | |
68 #EA 67 2 | |
69 #EP #BD 28 1 68 | |
70 #EP #BI 3 13 69 | |
#IND 1 25 14 1 27 70 1 | |
71 #EA 67 1 | |
72 #EP #BC 12 71 2 | |
73 #EP #BD 3 13 72 | |
29 #NS 25 rec | |
74 #EC 29 2 1 | |
75 #EA 74 2 | |
76 #EL #BC 12 68 20 | |
77 #EA 75 76 | |
78 #EL #BD 28 2 1 | |
79 #EA 77 78 | |
80 #EA 79 1 | |
81 #EL #BC 12 71 80 | |
82 #EL #BD 3 13 81 | |
#DEF 26 73 82 1 | |
30 #NS 14 has_zero | |
83 #EC 25 0 | |
84 #EA 83 38 | |
85 #EC 27 0 | |
86 #EA 85 38 | |
87 #EC 15 | |
88 #EA 86 87 | |
#DEF 30 84 88 | |
31 #NS 0 bit0 | |
32 #NS 0 has_add | |
33 #NS 32 mk | |
34 #NS 0 add | |
89 #EP #BD 4 2 20 | |
90 #EP #BD 4 1 89 | |
91 #EC 32 1 | |
92 #EA 91 2 | |
93 #EP #BD 34 90 92 | |
94 #EP #BI 3 13 93 | |
#IND 1 32 14 1 33 94 1 | |
35 #NS 32 add | |
95 #EA 91 1 | |
96 #EP #BD 4 20 27 | |
97 #EP #BD 4 2 96 | |
98 #EP #BC 12 95 97 | |
99 #EP #BI 3 13 98 | |
36 #NS 32 rec | |
100 #EC 36 2 1 | |
101 #EA 100 2 | |
102 #EV 4 | |
103 #EP #BD 4 27 102 | |
104 #EP #BD 4 20 103 | |
105 #EL #BC 12 92 104 | |
106 #EA 101 105 | |
107 #EL #BD 34 97 1 | |
108 #EA 106 107 | |
109 #EA 108 1 | |
110 #EL #BC 12 95 109 | |
111 #EL #BD 3 13 110 | |
#DEF 35 99 111 1 | |
37 #NS 0 s | |
112 #EP #BC 37 95 89 | |
113 #EP #BI 3 13 112 | |
114 #EC 35 1 | |
115 #EA 114 20 | |
116 #EA 115 2 | |
117 #EA 116 1 | |
118 #EA 117 1 | |
119 #EL #BD 4 2 118 | |
120 #EL #BC 37 95 119 | |
121 #EL #BI 3 13 120 | |
#DEF 31 113 121 1 | |
38 #NS 14 has_add | |
39 #NS 14 add | |
40 #NS 39 _main | |
41 #NS 14 brec_on | |
42 #NS 14 below | |
43 #NS 0 punit | |
44 #NS 43 star | |
122 #EC 43 1 | |
#IND 0 43 0 1 44 122 1 | |
45 #NS 0 v | |
46 #NS 0 pprod | |
47 #NS 0 β | |
5 #UP 45 | |
123 #ES 5 | |
6 #UM 1 5 | |
7 #UM 3 6 | |
124 #ES 7 | |
125 #EP #BD 47 123 124 | |
126 #EP #BD 3 0 125 | |
48 #NS 46 mk | |
49 #NS 0 fst | |
50 #NS 0 snd | |
127 #EC 46 1 5 | |
128 #EA 127 27 | |
129 #EA 128 20 | |
130 #EP #BD 50 2 129 | |
131 #EP #BD 49 2 130 | |
132 #EP #BI 47 123 131 | |
133 #EP #BI 3 0 132 | |
#IND 2 46 126 1 48 133 1 45 | |
51 #NS 0 l | |
52 #NS 0 C | |
8 #UP 51 | |
134 #ES 8 | |
135 #EP #BD 17 38 134 | |
9 #UM 3 8 | |
136 #ES 9 | |
137 #EP #BD 17 38 136 | |
138 #EP #BD 52 135 137 | |
53 #NS 14 rec | |
10 #US 9 | |
139 #EC 53 10 | |
140 #EL #BD 17 38 136 | |
141 #EA 139 140 | |
142 #EC 43 9 | |
143 #EA 141 142 | |
54 #NS 0 ih | |
144 #EC 46 9 9 | |
145 #EC 46 8 9 | |
146 #EA 27 2 | |
147 #EA 145 146 | |
148 #EA 147 1 | |
149 #EA 144 148 | |
150 #EA 149 142 | |
151 #EL #BD 54 136 150 | |
152 #EL #BD 17 38 151 | |
153 #EA 143 152 | |
154 #EA 153 1 | |
155 #EL #BD 17 38 154 | |
156 #EL #BD 52 135 155 | |
#DEF 42 138 156 51 | |
55 #NS 46 fst | |
157 #EA 127 2 | |
158 #EA 157 1 | |
159 #EP #BD 12 158 20 | |
160 #EP #BI 47 123 159 | |
161 #EP #BI 3 0 160 | |
56 #NS 46 rec | |
162 #EC 56 1 1 5 | |
163 #EA 162 20 | |
164 #EA 163 2 | |
165 #EA 127 20 | |
166 #EA 165 2 | |
167 #EL #BD 12 166 27 | |
168 #EA 164 167 | |
169 #EL #BD 50 20 2 | |
170 #EL #BD 49 20 169 | |
171 #EA 168 170 | |
172 #EA 171 1 | |
173 #EL #BD 12 158 172 | |
174 #EL #BD 47 123 173 | |
175 #EL #BD 3 0 174 | |
#DEF 55 161 175 1 45 | |
57 #NS 0 F | |
58 #NS 0 f | |
176 #EC 42 8 | |
177 #EA 176 20 | |
178 #EA 177 1 | |
179 #EP #BD 58 178 146 | |
180 #EP #BD 17 38 179 | |
181 #EA 20 2 | |
182 #EP #BD 57 180 181 | |
183 #EP #BD 17 38 182 | |
184 #EP #BI 52 135 183 | |
185 #EC 55 8 9 | |
186 #EA 185 181 | |
187 #EA 177 2 | |
188 #EA 186 187 | |
189 #EC 53 9 | |
190 #EA 27 1 | |
191 #EA 145 190 | |
192 #EA 176 27 | |
193 #EA 192 1 | |
194 #EA 191 193 | |
195 #EL #BD 17 38 194 | |
196 #EA 189 195 | |
197 #EC 48 8 9 | |
198 #EA 20 87 | |
199 #EA 197 198 | |
200 #EA 199 142 | |
201 #EA 1 87 | |
202 #EC 44 9 | |
203 #EA 201 202 | |
204 #EA 200 203 | |
205 #EA 204 202 | |
206 #EA 196 205 | |
207 #EA 102 50 | |
208 #EA 197 207 | |
209 #EA 102 2 | |
210 #EA 145 209 | |
211 #EA 176 102 | |
212 #EA 211 2 | |
213 #EA 210 212 | |
214 #EA 144 213 | |
215 #EA 214 142 | |
216 #EA 208 215 | |
217 #EA 20 50 | |
218 #EC 48 9 9 | |
219 #EA 218 213 | |
220 #EA 219 142 | |
221 #EA 220 1 | |
222 #EA 221 202 | |
223 #EA 217 222 | |
224 #EA 216 223 | |
225 #EA 224 222 | |
226 #EL #BD 54 194 225 | |
227 #EL #BD 17 38 226 | |
228 #EA 206 227 | |
229 #EA 228 2 | |
230 #EA 188 229 | |
231 #EL #BD 57 180 230 | |
232 #EL #BD 17 38 231 | |
233 #EL #BI 52 135 232 | |
#DEF 41 184 233 51 | |
59 #NS 14 cases_on | |
60 #NS 0 e_1 | |
234 #EA 2 87 | |
61 #NS 0 e_2 | |
235 #EA 49 1 | |
236 #EA 27 235 | |
237 #EP #BD 17 38 236 | |
238 #EA 27 20 | |
239 #EP #BD 61 237 238 | |
240 #EP #BD 60 234 239 | |
241 #EP #BD 17 38 240 | |
242 #EP #BI 52 135 241 | |
243 #EC 53 8 | |
244 #EA 243 27 | |
245 #EA 244 2 | |
246 #EA 102 1 | |
247 #EL #BD 54 246 181 | |
248 #EL #BD 17 38 247 | |
249 #EA 245 248 | |
250 #EA 249 20 | |
251 #EL #BD 61 237 250 | |
252 #EL #BD 60 234 251 | |
253 #EL #BD 17 38 252 | |
254 #EL #BI 52 135 253 | |
#DEF 59 242 254 51 | |
62 #NS 0 id_rhs | |
255 #EP #BD 4 1 2 | |
256 #EP #BD 3 0 255 | |
257 #EL #BD 4 1 1 | |
258 #EL #BD 3 0 257 | |
#DEF 62 256 258 1 | |
259 #EP #BD 4 38 38 | |
260 #EP #BD 4 38 259 | |
261 #EC 41 3 | |
262 #EL #BD 4 38 259 | |
263 #EA 261 262 | |
264 #EA 263 1 | |
63 #NS 0 _F | |
265 #EC 42 3 | |
266 #EA 265 262 | |
267 #EA 266 1 | |
268 #EC 59 3 | |
269 #EP #BD 63 267 38 | |
270 #EL #BD 4 38 269 | |
271 #EA 268 270 | |
272 #EA 271 2 | |
273 #EA 266 87 | |
274 #EC 62 3 | |
275 #EA 274 38 | |
276 #EA 275 27 | |
277 #EL #BD 63 273 276 | |
278 #EA 272 277 | |
64 #NS 0 a_1 | |
279 #EA 266 235 | |
280 #EC 55 3 3 | |
281 #EA 262 2 | |
282 #EA 280 281 | |
11 #US 3 | |
283 #EC 53 11 | |
284 #EL #BD 17 38 37 | |
285 #EA 283 284 | |
286 #EC 43 3 | |
287 #EA 285 286 | |
288 #EC 46 3 3 | |
289 #EA 288 281 | |
290 #EA 289 1 | |
291 #EA 288 290 | |
292 #EA 291 286 | |
293 #EL #BD 54 37 292 | |
294 #EL #BD 17 38 293 | |
295 #EA 287 294 | |
296 #EA 295 2 | |
297 #EA 282 296 | |
298 #EA 289 296 | |
299 #EA 280 298 | |
300 #EA 299 286 | |
301 #EA 300 1 | |
302 #EA 297 301 | |
303 #EA 302 102 | |
304 #EA 49 303 | |
305 #EA 275 304 | |
306 #EL #BD 63 279 305 | |
307 #EL #BD 64 38 306 | |
308 #EA 278 307 | |
309 #EA 308 1 | |
310 #EL #BD 63 267 309 | |
311 #EL #BD 4 38 310 | |
312 #EL #BD 4 38 311 | |
313 #EA 312 1 | |
314 #EA 313 20 | |
315 #EA 314 2 | |
316 #EL #BD 4 38 315 | |
317 #EL #BD 63 267 316 | |
318 #EL #BD 4 38 317 | |
319 #EA 264 318 | |
320 #EA 319 2 | |
321 #EL #BD 4 38 320 | |
322 #EL #BD 4 38 321 | |
#DEF 40 260 322 | |
323 #EC 40 | |
#DEF 39 260 323 | |
324 #EC 32 0 | |
325 #EA 324 38 | |
326 #EC 33 0 | |
327 #EA 326 38 | |
328 #EC 39 | |
329 #EA 327 328 | |
#DEF 38 325 329 | |
65 #NS 0 bit1 | |
66 #NS 0 has_one | |
67 #NS 66 mk | |
68 #NS 0 one | |
330 #EC 66 1 | |
331 #EA 330 2 | |
332 #EP #BD 68 1 331 | |
333 #EP #BI 3 13 332 | |
#IND 1 66 14 1 67 333 1 | |
69 #NS 66 one | |
334 #EA 330 1 | |
335 #EP #BC 12 334 2 | |
336 #EP #BD 3 13 335 | |
70 #NS 66 rec | |
337 #EC 70 2 1 | |
338 #EA 337 2 | |
339 #EL #BC 12 331 20 | |
340 #EA 338 339 | |
341 #EL #BD 68 2 1 | |
342 #EA 340 341 | |
343 #EA 342 1 | |
344 #EL #BC 12 334 343 | |
345 #EL #BD 3 13 344 | |
#DEF 69 336 345 1 | |
71 #NS 0 s₁ | |
72 #NS 0 s₂ | |
346 #EP #BC 72 92 96 | |
347 #EP #BC 71 334 346 | |
348 #EP #BI 3 13 347 | |
349 #EA 114 27 | |
350 #EA 349 2 | |
351 #EC 31 1 | |
352 #EA 351 27 | |
353 #EA 352 2 | |
354 #EA 353 1 | |
355 #EA 350 354 | |
356 #EC 69 1 | |
357 #EA 356 27 | |
358 #EA 357 20 | |
359 #EA 355 358 | |
360 #EL #BD 4 20 359 | |
361 #EL #BC 72 92 360 | |
362 #EL #BC 71 334 361 | |
363 #EL #BI 3 13 362 | |
#DEF 65 348 363 1 | |
73 #NS 14 has_one | |
364 #EC 66 0 | |
365 #EA 364 38 | |
366 #EC 67 0 | |
367 #EA 366 38 | |
368 #EA 49 87 | |
369 #EA 367 368 | |
#DEF 73 365 369 | |
74 #NS 14 zero_lt_succ | |
75 #NS 14 succ_le_succ | |
76 #NS 0 has_le | |
77 #NS 76 le | |
78 #NS 76 mk | |
79 #NS 0 le | |
370 #EC 76 1 | |
371 #EA 370 2 | |
372 #EP #BD 79 5 371 | |
373 #EP #BI 3 13 372 | |
#IND 1 76 14 1 78 373 1 | |
374 #EA 370 1 | |
375 #EP #BC 12 374 22 | |
376 #EP #BI 3 13 375 | |
80 #NS 76 rec | |
377 #EC 80 4 1 | |
378 #EA 377 2 | |
379 #EL #BC 12 371 29 | |
380 #EA 378 379 | |
381 #EL #BD 79 22 1 | |
382 #EA 380 381 | |
383 #EA 382 1 | |
384 #EL #BC 12 374 383 | |
385 #EL #BD 3 13 384 | |
#DEF 77 376 385 1 | |
81 #NS 14 has_le | |
386 #EC 76 0 | |
387 #EA 386 38 | |
388 #EC 78 0 | |
389 #EA 388 38 | |
390 #EA 389 42 | |
#DEF 81 387 390 | |
82 #NS 14 le_refl | |
391 #EC 77 0 | |
392 #EA 391 38 | |
393 #EC 81 | |
394 #EA 392 393 | |
395 #EA 394 1 | |
396 #EA 395 1 | |
397 #EP #BD 4 38 396 | |
398 #EC 21 | |
#DEF 82 397 398 | |
399 #EA 394 2 | |
400 #EA 399 1 | |
401 #EA 49 20 | |
402 #EA 394 401 | |
403 #EA 402 50 | |
404 #EP #BD 4 400 403 | |
405 #EP #BI 24 38 404 | |
406 #EP #BI 17 38 405 | |
83 #NS 0 h | |
84 #NS 20 rec | |
407 #EC 84 | |
408 #EA 407 20 | |
85 #NS 0 _x | |
409 #EA 49 27 | |
410 #EA 394 409 | |
411 #EA 410 235 | |
412 #EL #BD 85 38 411 | |
413 #EA 408 412 | |
414 #EC 82 | |
415 #EA 414 401 | |
416 #EA 413 415 | |
417 #EA 42 27 | |
418 #EA 417 1 | |
419 #EC 22 | |
420 #EA 49 102 | |
421 #EA 419 420 | |
422 #EA 421 50 | |
423 #EL #BD 23 418 422 | |
424 #EL #BD 4 38 423 | |
425 #EA 416 424 | |
426 #EA 425 2 | |
427 #EA 426 1 | |
428 #EL #BD 83 400 427 | |
429 #EL #BI 24 38 428 | |
430 #EL #BI 17 38 429 | |
#DEF 75 406 430 | |
86 #NS 14 zero_le | |
431 #EC 26 0 | |
432 #EA 431 38 | |
433 #EC 30 | |
434 #EA 432 433 | |
435 #EA 394 434 | |
436 #EA 435 1 | |
437 #EP #BD 17 38 436 | |
438 #EC 41 0 | |
439 #EL #BD 17 38 436 | |
440 #EA 438 439 | |
441 #EA 440 1 | |
442 #EC 42 0 | |
443 #EA 442 439 | |
444 #EA 443 1 | |
445 #EC 59 0 | |
446 #EA 435 2 | |
447 #EP #BD 63 444 446 | |
448 #EL #BD 17 38 447 | |
449 #EA 445 448 | |
450 #EA 449 2 | |
451 #EA 443 87 | |
452 #EA 414 434 | |
453 #EL #BD 63 451 452 | |
454 #EA 450 453 | |
455 #EA 443 235 | |
456 #EA 419 434 | |
457 #EA 456 2 | |
458 #EC 55 0 3 | |
459 #EA 262 87 | |
460 #EA 280 459 | |
461 #EA 295 87 | |
462 #EA 460 461 | |
463 #EA 288 459 | |
464 #EA 463 461 | |
465 #EA 280 464 | |
466 #EA 465 286 | |
467 #EC 48 3 3 | |
468 #EA 463 273 | |
469 #EA 467 468 | |
470 #EA 469 286 | |
471 #EC 53 3 | |
472 #EA 262 1 | |
473 #EA 288 472 | |
474 #EA 473 267 | |
475 #EL #BD 17 38 474 | |
476 #EA 471 475 | |
477 #EA 467 459 | |
478 #EA 477 286 | |
479 #EA 318 87 | |
480 #EC 44 3 | |
481 #EA 479 480 | |
482 #EA 478 481 | |
483 #EA 482 480 | |
484 #EA 476 483 | |
485 #EA 262 50 | |
486 #EA 467 485 | |
487 #EA 266 2 | |
488 #EA 289 487 | |
489 #EA 288 488 | |
490 #EA 489 286 | |
491 #EA 486 490 | |
492 #EA 318 50 | |
493 #EA 467 488 | |
494 #EA 493 286 | |
495 #EA 494 1 | |
496 #EA 495 480 | |
497 #EA 492 496 | |
498 #EA 491 497 | |
499 #EA 498 496 | |
500 #EL #BD 54 474 499 | |
501 #EL #BD 17 38 500 | |
502 #EA 484 501 | |
503 #EA 502 87 | |
504 #EA 470 503 | |
505 #EA 504 480 | |
506 #EA 466 505 | |
507 #EA 462 506 | |
508 #EA 507 2 | |
509 #EA 439 508 | |
510 #EA 458 509 | |
511 #EC 46 0 3 | |
512 #EA 439 2 | |
513 #EA 511 512 | |
514 #EA 513 1 | |
515 #EA 288 514 | |
516 #EA 515 286 | |
517 #EL #BD 54 37 516 | |
518 #EL #BD 17 38 517 | |
519 #EA 287 518 | |
520 #EA 519 508 | |
521 #EA 510 520 | |
522 #EA 511 509 | |
523 #EA 522 520 | |
524 #EA 280 523 | |
525 #EA 524 286 | |
526 #EA 525 1 | |
527 #EA 521 526 | |
528 #EA 457 527 | |
529 #EL #BD 63 455 528 | |
530 #EL #BD 17 38 529 | |
531 #EA 454 530 | |
532 #EA 531 1 | |
533 #EL #BD 63 444 532 | |
534 #EL #BD 17 38 533 | |
535 #EA 534 2 | |
536 #EA 535 1 | |
537 #EL #BD 63 444 536 | |
538 #EL #BD 17 38 537 | |
539 #EA 441 538 | |
540 #EL #BD 17 38 539 | |
#DEF 86 437 540 | |
541 #EC 9 0 | |
542 #EA 541 38 | |
543 #EC 18 | |
544 #EA 542 543 | |
545 #EA 544 434 | |
546 #EA 545 235 | |
547 #EP #BD 17 38 546 | |
548 #EC 75 | |
549 #EA 548 434 | |
550 #EA 549 1 | |
551 #EC 86 | |
552 #EA 551 1 | |
553 #EA 550 552 | |
554 #EL #BD 17 38 553 | |
#DEF 74 547 554 | |
555 #EC 31 0 | |
556 #EA 555 38 | |
557 #EC 38 | |
558 #EA 556 557 | |
559 #EC 65 0 | |
560 #EA 559 38 | |
561 #EC 73 | |
562 #EA 560 561 | |
563 #EA 562 557 | |
564 #EC 69 0 | |
565 #EA 564 38 | |
566 #EA 565 561 | |
567 #EA 563 566 | |
568 #EA 558 567 | |
569 #EA 563 568 | |
570 #EA 563 569 | |
571 #EA 558 570 | |
572 #EA 558 571 | |
573 #EA 558 572 | |
574 #EA 558 573 | |
575 #EA 558 574 | |
576 #EA 558 575 | |
577 #EA 558 576 | |
578 #EA 558 577 | |
579 #EA 558 578 | |
580 #EA 558 579 | |
581 #EA 558 580 | |
582 #EA 545 581 | |
583 #EC 74 | |
584 #EA 558 569 | |
585 #EA 507 584 | |
586 #EA 262 585 | |
587 #EA 280 586 | |
588 #EA 295 585 | |
589 #EA 587 588 | |
590 #EA 288 586 | |
591 #EA 590 588 | |
592 #EA 280 591 | |
593 #EA 592 286 | |
594 #EA 266 585 | |
595 #EA 590 594 | |
596 #EA 467 595 | |
597 #EA 596 286 | |
598 #EA 502 585 | |
599 #EA 597 598 | |
600 #EA 599 480 | |
601 #EA 593 600 | |
602 #EA 589 601 | |
603 #EA 602 570 | |
604 #EA 262 603 | |
605 #EA 280 604 | |
606 #EA 295 603 | |
607 #EA 605 606 | |
608 #EA 288 604 | |
609 #EA 608 606 | |
610 #EA 280 609 | |
611 #EA 610 286 | |
612 #EA 266 603 | |
613 #EA 608 612 | |
614 #EA 467 613 | |
615 #EA 614 286 | |
616 #EA 502 603 | |
617 #EA 615 616 | |
618 #EA 617 480 | |
619 #EA 611 618 | |
620 #EA 607 619 | |
621 #EA 620 571 | |
622 #EA 262 621 | |
623 #EA 280 622 | |
624 #EA 295 621 | |
625 #EA 623 624 | |
626 #EA 288 622 | |
627 #EA 626 624 | |
628 #EA 280 627 | |
629 #EA 628 286 | |
630 #EA 266 621 | |
631 #EA 626 630 | |
632 #EA 467 631 | |
633 #EA 632 286 | |
634 #EA 502 621 | |
635 #EA 633 634 | |
636 #EA 635 480 | |
637 #EA 629 636 | |
638 #EA 625 637 | |
639 #EA 638 572 | |
640 #EA 262 639 | |
641 #EA 280 640 | |
642 #EA 295 639 | |
643 #EA 641 642 | |
644 #EA 288 640 | |
645 #EA 644 642 | |
646 #EA 280 645 | |
647 #EA 646 286 | |
648 #EA 266 639 | |
649 #EA 644 648 | |
650 #EA 467 649 | |
651 #EA 650 286 | |
652 #EA 502 639 | |
653 #EA 651 652 | |
654 #EA 653 480 | |
655 #EA 647 654 | |
656 #EA 643 655 | |
657 #EA 656 573 | |
658 #EA 262 657 | |
659 #EA 280 658 | |
660 #EA 295 657 | |
661 #EA 659 660 | |
662 #EA 288 658 | |
663 #EA 662 660 | |
664 #EA 280 663 | |
665 #EA 664 286 | |
666 #EA 266 657 | |
667 #EA 662 666 | |
668 #EA 467 667 | |
669 #EA 668 286 | |
670 #EA 502 657 | |
671 #EA 669 670 | |
672 #EA 671 480 | |
673 #EA 665 672 | |
674 #EA 661 673 | |
675 #EA 674 574 | |
676 #EA 262 675 | |
677 #EA 280 676 | |
678 #EA 295 675 | |
679 #EA 677 678 | |
680 #EA 288 676 | |
681 #EA 680 678 | |
682 #EA 280 681 | |
683 #EA 682 286 | |
684 #EA 266 675 | |
685 #EA 680 684 | |
686 #EA 467 685 | |
687 #EA 686 286 | |
688 #EA 502 675 | |
689 #EA 687 688 | |
690 #EA 689 480 | |
691 #EA 683 690 | |
692 #EA 679 691 | |
693 #EA 692 575 | |
694 #EA 262 693 | |
695 #EA 280 694 | |
696 #EA 295 693 | |
697 #EA 695 696 | |
698 #EA 288 694 | |
699 #EA 698 696 | |
700 #EA 280 699 | |
701 #EA 700 286 | |
702 #EA 266 693 | |
703 #EA 698 702 | |
704 #EA 467 703 | |
705 #EA 704 286 | |
706 #EA 502 693 | |
707 #EA 705 706 | |
708 #EA 707 480 | |
709 #EA 701 708 | |
710 #EA 697 709 | |
711 #EA 710 576 | |
712 #EA 262 711 | |
713 #EA 280 712 | |
714 #EA 295 711 | |
715 #EA 713 714 | |
716 #EA 288 712 | |
717 #EA 716 714 | |
718 #EA 280 717 | |
719 #EA 718 286 | |
720 #EA 266 711 | |
721 #EA 716 720 | |
722 #EA 467 721 | |
723 #EA 722 286 | |
724 #EA 502 711 | |
725 #EA 723 724 | |
726 #EA 725 480 | |
727 #EA 719 726 | |
728 #EA 715 727 | |
729 #EA 728 577 | |
730 #EA 262 729 | |
731 #EA 280 730 | |
732 #EA 295 729 | |
733 #EA 731 732 | |
734 #EA 288 730 | |
735 #EA 734 732 | |
736 #EA 280 735 | |
737 #EA 736 286 | |
738 #EA 266 729 | |
739 #EA 734 738 | |
740 #EA 467 739 | |
741 #EA 740 286 | |
742 #EA 502 729 | |
743 #EA 741 742 | |
744 #EA 743 480 | |
745 #EA 737 744 | |
746 #EA 733 745 | |
747 #EA 746 578 | |
748 #EA 262 747 | |
749 #EA 280 748 | |
750 #EA 295 747 | |
751 #EA 749 750 | |
752 #EA 288 748 | |
753 #EA 752 750 | |
754 #EA 280 753 | |
755 #EA 754 286 | |
756 #EA 266 747 | |
757 #EA 752 756 | |
758 #EA 467 757 | |
759 #EA 758 286 | |
760 #EA 502 747 | |
761 #EA 759 760 | |
762 #EA 761 480 | |
763 #EA 755 762 | |
764 #EA 751 763 | |
765 #EA 764 579 | |
766 #EA 262 765 | |
767 #EA 280 766 | |
768 #EA 295 765 | |
769 #EA 767 768 | |
770 #EA 288 766 | |
771 #EA 770 768 | |
772 #EA 280 771 | |
773 #EA 772 286 | |
774 #EA 266 765 | |
775 #EA 770 774 | |
776 #EA 467 775 | |
777 #EA 776 286 | |
778 #EA 502 765 | |
779 #EA 777 778 | |
780 #EA 779 480 | |
781 #EA 773 780 | |
782 #EA 769 781 | |
783 #EA 782 580 | |
784 #EA 583 783 | |
#DEF 7 582 784 | |
87 #NS 0 has_mem | |
88 #NS 87 mem | |
#INFIX 88 50 ∈ | |
#INFIX 2 50 = | |
#INFIX 9 50 < | |
89 #NS 0 has_mul | |
90 #NS 89 mul | |
#INFIX 90 70 * | |
#INFIX 77 50 ≤ | |
#INFIX 77 50 <= | |
91 #NS 0 unification_constraint | |
92 #NS 91 mk | |
#INFIX 92 50 =?= | |
#INFIX 92 50 ≟ | |
93 #NS 0 prod | |
#INFIX 93 35 × | |
#INFIX 35 65 + | |
94 #NS 0 has_sdiff | |
95 #NS 94 sdiff | |
#INFIX 95 70 \ | |
96 #NS 0 and | |
#INFIX 96 35 ∧ | |
#INFIX 96 35 /\ | |
97 #NS 0 has_dvd | |
98 #NS 97 dvd | |
#INFIX 98 50 ∣ | |
99 #NS 0 not | |
#PREFIX 99 40 ¬ | |
100 #NS 0 has_inter | |
101 #NS 100 inter | |
#INFIX 101 70 ∩ | |
102 #NS 0 has_equiv | |
103 #NS 102 equiv | |
#INFIX 103 50 ≈ | |
104 #NS 0 has_subset | |
105 #NS 104 subset | |
#INFIX 105 50 ⊆ | |
106 #NS 0 ne | |
#INFIX 106 50 ≠ | |
107 #NS 0 iff | |
#INFIX 107 20 ↔ | |
#INFIX 107 20 <-> | |
108 #NS 0 has_mod | |
109 #NS 108 mod | |
#INFIX 109 70 % | |
110 #NS 0 ssuperset | |
#INFIX 110 50 ⊃ | |
111 #NS 0 gt | |
#INFIX 111 50 > | |
112 #NS 2 subst | |
#INFIX 112 75 ▸ | |
113 #NS 0 or | |
#INFIX 113 30 ∨ | |
#INFIX 113 30 \/ | |
114 #NS 0 ge | |
#INFIX 114 50 ≥ | |
#INFIX 114 50 >= | |
115 #NS 0 has_inv | |
116 #NS 115 inv | |
#POSTFIX 116 1034 ⁻¹ | |
117 #NS 0 has_append | |
118 #NS 117 append | |
#INFIX 118 65 ++ | |
119 #NS 0 has_ssubset | |
120 #NS 119 ssubset | |
#INFIX 120 50 ⊂ | |
121 #NS 0 has_sub | |
122 #NS 121 sub | |
#INFIX 122 65 - | |
123 #NS 0 andthen | |
#INFIX 123 1 ; | |
124 #NS 0 has_union | |
125 #NS 124 union | |
#INFIX 125 65 ∪ | |
126 #NS 0 has_neg | |
127 #NS 126 neg | |
#PREFIX 127 65 - | |
128 #NS 0 heq | |
#INFIX 128 50 == | |
129 #NS 0 superset | |
#INFIX 129 50 ⊇ | |
130 #NS 0 has_div | |
131 #NS 130 div | |
#INFIX 131 70 / | |
132 #NS 0 list | |
133 #NS 132 cons | |
#INFIX 133 67 :: |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment