gistfile1.txt

1431773 #EP #BI 3 45 1431772
1431774 #EA 419493 54
1431775 #EA 1431774 810246
1431776 #EA 1431775 810985
1431777 #EA 1431776 902781
1431778 #EC 17566 1
1431779 #EA 1431778 54
1431780 #EA 1431779 31
1431781 #EA 1431780 2
1431782 #EA 1431781 1
1431783 #EA 1431777 1431782
1431784 #EA 902835 54
1431785 #EA 1431784 31
1431786 #EA 1431785 2
1431787 #EA 1431786 1
1431788 #EA 1431783 1431787
1431789 #EL #BI 19 31 1431788
1431790 #EL #BI 4 2 1431789
1431791 #EL #BC 162 24812 1431790
1431792 #EL #BI 3 45 1431791
#DEF 17565 1431773 1431792 1
1431793 #EA 902812 810389
1431794 #EP #BD 1325 810382 1431793
1431795 #EP #BI 24 645 1431794
1431796 #EP #BI 19 61 1431795
1431797 #EP #BI 4 54 1431796
1431798 #EP #BC 1725 783173 1431797
1431799 #EP #BC 163 36441 1431798
1431800 #EP #BC 162 453944 1431799
1431801 #EP #BI 3 45 1431800
1431802 #EA 810940 902811
1431803 #EA 1431802 810950
1431804 #EC 17565 1
1431805 #EA 1431804 845
1431806 #EA 1431805 644552
1431807 #EA 1431806 54
1431808 #EA 1431807 2
1431809 #EA 1431803 1431808
1431810 #EL #BD 1325 810382 1431809
1431811 #EL #BI 24 645 1431810
1431812 #EL #BI 19 61 1431811
1431813 #EL #BI 4 54 1431812
1431814 #EL #BC 1725 783173 1431813
1431815 #EL #BC 163 36441 1431814
1431816 #EL #BC 162 453944 1431815
1431817 #EL #BI 3 45 1431816
#DEF 17564 1431801 1431817 1
17568 #NS 0 has_deriv_within_at_iff_tendsto_slope'
17569 #NS 2727 diff_singleton_eq_self
17570 #NS 2727 diff_eq_self
17571 #NS 0 sdiff_eq_self_iff_disjoint
17572 #NS 0 sdiff_eq_sdiff_iff_inf_eq_inf
17573 #NS 0 sdiff_inf_self_right
17574 #NS 0 sdiff_inf
17575 #NS 0 sup_sdiff_right
1431818 #EA 908191 31
1431819 #EA 591 1431818
1431820 #EA 1431819 31
1431821 #EP #BC 162 210176 1431820
1431822 #EP #BI 317 2 1431821
1431823 #EP #BI 258 1 1431822
1431824 #EP #BI 3 45 1431823
1431825 #EA 8595 1431820
1431826 #EA 1431825 1153179
1431827 #EA 8390 1431820
1431828 #EA 1431827 1153179
1431829 #EA 8434 1431828
1431830 #EA 12645 1431818
1431831 #EA 908229 54
1431832 #EA 607 1431831
1431833 #EA 1431832 54
1431834 #EA 8390 1431833
1431835 #EA 1431834 733216
1431836 #EL #BD 208 54 1431835
1431837 #EA 1431830 1431836
1431838 #EA 9178 1431820
1431839 #EA 1431837 1431838
1431840 #EA 1431839 1153177
1431841 #EA 908313 873619
1431842 #EA 1431841 31
1431843 #EA 1431840 1431842
1431844 #EA 1431829 1431843
1431845 #EA 1431826 1431844
1431846 #EA 105051 31
1431847 #EA 1153184 1431846
1431848 #EA 1153188 1431846
1431849 #EA 8434 1431848
1431850 #EA 12645 1153177
1431851 #EA 1153195 733216
1431852 #EL #BD 208 54 1431851
1431853 #EA 1431850 1431852
1431854 #EA 1431853 1153199
1431855 #EA 1431854 31
1431856 #EA 1153724 54
1431857 #EA 1431856 31
1431858 #EA 1431857 2
1431859 #EA 1431858 1
1431860 #EA 1431855 1431859
1431861 #EA 1431849 1431860
1431862 #EA 1431847 1431861
1431863 #EA 1431862 106915
--
12782723 #EA 12782720 12782722
12782724 #EA 12782723 31
12782725 #EA 9896716 2
12782726 #EA 12782724 12782725
12782727 #EP #BD 16 6823483 12782726
12782728 #EP #BI 85 845760 12782727
12782729 #EP #BC 1725 687311 12782728
12782730 #EP #BC 163 687310 12782729
12782731 #EP #BC 162 653530 12782730
12782732 #EP #BI 2034 8891 12782731
12782733 #EP #BI 74 8509 12782732
12782734 #EP #BI 3 8860 12782733
12782735 #EL #BD 16 6823483 1
12782736 #EL #BI 85 845760 12782735
12782737 #EL #BC 1725 687311 12782736
12782738 #EL #BC 163 687310 12782737
12782739 #EL #BC 162 653530 12782738
12782740 #EL #BI 2034 8891 12782739
12782741 #EL #BI 74 8509 12782740
12782742 #EL #BI 3 8860 12782741
#DEF 93979 12782734 12782742 452 446 453
93980 #NS 30495 of
12782743 #EA 1844947 31
12782744 #EA 12782743 3266763
12782745 #EA 12782744 571405
12782746 #EA 12782745 1840336
12782747 #EA 93436 3266763
12782748 #EA 12782747 7656674
12782749 #EA 12782746 12782748
12782750 #EA 12782749 1
12782751 #EA 12782750 7656681
12782752 #EP #BC 1725 3266681 12782751
12782753 #EP #BC 163 1840329 12782752
12782754 #EP #BD 127 8509 12782753
12782755 #EP #BD 605 3266678 12782754
12782756 #EP #BC 162 568189 12782755
12782757 #EP #BI 1022 8860 12782756
12782758 #EA 1840433 645
12782759 #EA 12782758 31
12782760 #EA 12782759 568207
12782761 #EA 12782760 2
12782762 #EA 12782761 1
12782763 #EA 12782762 3266749
12782764 #EL #BC 1725 3266681 12782763
12782765 #EL #BC 163 1840329 12782764
12782766 #EL #BD 127 8509 12782765
12782767 #EL #BD 605 3266678 12782766
12782768 #EL #BC 162 568189 12782767
12782769 #EL #BI 1022 8860 12782768
#DEF 93980 12782757 12782769 452 446
93981 #NS 2353 sdiff_eq_self_iff_disjoint
93982 #NS 2353 sdiff_eq_self
93983 #NS 3636 antisymm_iff
12782770 #EA 190868 190870
12782771 #EA 180112 12782770
12782772 #EP #BI 94 116254 12782771
12782773 #EP #BI 93 116250 12782772
12782774 #EP #BI 3 8860 12782773
12782775 #EC 3884 25
12782776 #EA 12782775 116917
12782777 #EA 12782776 191076
12782778 #EA 12782777 2
12782779 #EA 12782778 1
12782780 #EL #BI 94 116254 12782779
12782781 #EL #BI 93 116250 12782780
12782782 #EL #BI 3 8860 12782781
#DEF 93983 12782774 12782782 452
93984 #NS 2353 inter_subset_inter
12782783 #EA 1359638 54
12782784 #EA 213690 12782783
12782785 #EA 193864 31
12782786 #EA 12782784 12782785
12782787 #EP #BD 719 8300436 12782786
12782788 #EP #BD 16 3026122 12782787
12782789 #EP #BI 157 139079 12782788
12782790 #EP #BI 64 117221 12782789
12782791 #EP #BI 317 116917 12782790
12782792 #EP #BI 258 116254 12782791
12782793 #EP #BC 162 17347 12782792
12782794 #EP #BI 3 8860 12782793
12782795 #EA 8434 12782786
12782796 #EA 1360963 61
12782797 #EA 181378 12782796
12782798 #EA 193614 180194
12782799 #EA 193616 850
12782800 #EA 12782799 121348
12782801 #EA 12782798 12782800
12782802 #EA 12782801 766
12782803 #EA 12782802 61
12782804 #EA 180760 12782803
12782805 #EA 8595 12782804
12782806 #EA 416 841972
12782807 #EA 12782806 3551936
12782808 #EA 12782805 12782807
12782809 #EA 8390 12782804
12782810 #EA 12782809 12782807
12782811 #EA 8434 12782810
12782812 #EA 8715 12782804
12782813 #EA 206456 121505
12782814 #EA 206455 12782813
12782815 #EA 12782814 845
--
#DEF 94276 12843332 12843336
94277 #NS 13992 decidable_int
94278 #NS 94277 equations
94279 #NS 94278 _eqn_1
94280 #NS 94277 _proof_1
12843337 #EA 8356 2401297
12843338 #EA 12843337 2399692
12843339 #EP #BD 19 224888 12843338
12843340 #EP #BD 4 224888 12843339
12843341 #EA 91429 2399692
12843342 #EA 12843341 2401297
12843343 #EA 2401669 2
12843344 #EA 12843343 1
12843345 #EA 12843342 12843344
12843346 #EL #BD 19 224888 12843345
12843347 #EL #BD 4 224888 12843346
#DEF 94280 12843340 12843347
12843348 #EA 2401807 2
12843349 #EA 12843348 1
12843350 #EA 1045067 12843349
12843351 #EL #BD 19 224888 12843350
12843352 #EL #BD 4 224888 12843351
12843353 #EA 2399167 12843352
12843354 #EA 12843352 2
12843355 #EA 12843354 1
12843356 #EA 155567 12843355
12843357 #EA 12843356 2401297
12843358 #EC 94280
12843359 #EA 12843358 2
12843360 #EA 12843359 1
12843361 #EA 12843357 12843360
12843362 #EA 2291 2401295
12843363 #EA 12843362 252216
12843364 #EA 1810768 260049
12843365 #EA 12843364 440
12843366 #EA 12843363 12843365
12843367 #EA 2089036 1
12843368 #EA 12843367 228305
12843369 #EA 12843366 12843368
12843370 #EA 12843361 12843369
12843371 #EL #BD 19 224888 12843370
12843372 #EL #BD 4 224888 12843371
#DEF 94277 12843353 12843372
12843373 #EA 1283 12843353
12843374 #EC 94277
12843375 #EA 12843373 12843374
12843376 #EA 12843375 12843372
12843377 #EA 1328 12843353
12843378 #EA 12843377 12843374
#DEF 94279 12843376 12843378
94281 #NS 0 sdiff_eq_self_iff_disjoint'
12843379 #EA 1433169 898052
12843380 #EP #BC 162 210176 12843379
12843381 #EP #BI 317 2 12843380
12843382 #EP #BI 258 1 12843381
12843383 #EP #BI 3 45 12843382
12843384 #EA 8595 12843379
12843385 #EA 8356 1433171
12843386 #EA 12843385 898052
12843387 #EA 12843384 12843386
12843388 #EA 8390 12843379
12843389 #EA 12843388 12843386
12843390 #EA 8434 12843389
12843391 #EA 8715 1433168
12843392 #EA 1433238 54
12843393 #EA 12843392 31
12843394 #EA 1433194 12843393
12843395 #EA 8390 12843394
12843396 #EA 8380 12843393
12843397 #EA 12843395 12843396
12843398 #EL #BD 208 3 12843397
12843399 #EA 12843391 12843398
12843400 #EA 9178 12843379
12843401 #EA 12843399 12843400
12843402 #EA 12843401 1433171
12843403 #EA 8764 1433168
12843404 #EA 12843403 1433171
12843405 #EA 1433344 54
12843406 #EA 12843405 31
12843407 #EA 12843406 2
12843408 #EA 12843407 1
12843409 #EA 12843404 12843408
12843410 #EA 12843402 12843409
12843411 #EA 12843390 12843410
12843412 #EA 12843387 12843411
12843413 #EA 8595 12843386
12843414 #EA 8356 898052
12843415 #EA 12843414 898052
12843416 #EA 12843413 12843415
12843417 #EA 8390 12843386
12843418 #EA 12843417 12843415
12843419 #EA 8434 12843418
12843420 #EA 8356 1433240
12843421 #EA 12843420 12843393
12843422 #EA 8390 12843421
12843423 #EA 12843422 12843396
12843424 #EL #BD 208 3 12843423
12843425 #EA 1433287 12843424
12843426 #EA 9178 12843386
12843427 #EA 12843425 12843426
12843428 #EA 12843427 898052