char_zero_lt_d800.txt

char_zero_lt_d800.txt

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  ::