X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2FlibrariesCluster.ps;h=94b0666878cc431f2a05c84c04632e55f448921f;hb=18c6848695fbfa97508e0981f6875a6459429a58;hp=eb52d37d17749b92da41650c58de9c5cbb1c7a4d;hpb=fceef5d991d78de6e162efcdd94600dc0d903368;p=helm.git diff --git a/helm/papers/matita/librariesCluster.ps b/helm/papers/matita/librariesCluster.ps index eb52d37d1..94b066687 100644 --- a/helm/papers/matita/librariesCluster.ps +++ b/helm/papers/matita/librariesCluster.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) -%%For: (zacchiro) Stefano Zacchiroli,,, +%%For: (sacerdot) Claudio Sacerdoti Coen,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 1114 979 +%%BoundingBox: 35 35 1108 1263 %%EndComments save %%BeginProlog @@ -230,10 +230,10 @@ def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 1114 979 +%%PageBoundingBox: 36 36 1108 1263 %%PageOrientation: Portrait gsave -35 35 1079 944 boxprim clip newpath +35 35 1073 1228 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0 0 translate 0 rotate @@ -244,22 +244,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 640 488 moveto -1069 488 lineto -1069 862 lineto -640 862 lineto +newpath 634 778 moveto +1063 778 lineto +1063 1162 lineto +634 1162 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 640 488 moveto -1069 488 lineto -1069 862 lineto -640 862 lineto +newpath 634 778 moveto +1063 778 lineto +1063 1162 lineto +634 1162 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -648 498 moveto +642 788 moveto (Terms at the content and presentation level) [14.64 10.56 7.92 18.72 9.36 6 10.56 6.72 6 6.72 12 10.56 6 10.56 12 12 6.72 10.56 12 6.72 6 10.56 12 12 6 12 7.92 10.56 9.36 10.56 12 6.72 10.56 6.72 6.72 12 12 6 6.72 10.56 12 10.56 6.72] xshow @@ -270,22 +270,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 152 618 moveto -402 618 lineto -402 898 lineto -152 898 lineto +newpath 68 814 moveto +454 814 lineto +454 1094 lineto +68 1094 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 152 618 moveto -402 618 lineto -402 898 lineto -152 898 lineto +newpath 68 814 moveto +454 814 lineto +454 1094 lineto +68 1094 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -160 872 moveto +76 1068 moveto (Partially specified terms) [13.44 10.56 7.92 6.72 6.72 10.56 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] xshow @@ -296,22 +296,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 258 208 moveto -632 208 lineto -632 592 lineto -258 592 lineto +newpath 289 296 moveto +551 296 lineto +551 770 lineto +289 770 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 258 208 moveto -632 208 lineto -632 592 lineto -258 592 lineto +newpath 289 296 moveto +551 296 lineto +551 770 lineto +289 770 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -265 218 moveto +296 306 moveto (Fully specified terms) [13.44 12 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] xshow @@ -322,22 +322,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 640 16 moveto -928 16 lineto -928 400 lineto -640 400 lineto +newpath 559 16 moveto +957 16 lineto +957 400 lineto +559 400 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 640 16 moveto -928 16 lineto -928 400 lineto -640 400 lineto +newpath 559 16 moveto +957 16 lineto +957 400 lineto +559 400 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -842 26 moveto +871 26 moveto (Utilities) [17.28 6.72 6.72 6.72 6.72 6.72 6.72 10.56 9.36] xshow @@ -346,10 +346,10 @@ end grestore % acic_content gsave 10 dict begin -758 652 75 25 ellipse_path +752 848 75 25 ellipse_path stroke gsave 10 dict begin -697 644 moveto +691 840 moveto (acic_content) [10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] xshow @@ -358,10 +358,10 @@ end grestore % cic_acic gsave 10 dict begin -731 558 54 25 ellipse_path +352 636 54 25 ellipse_path stroke gsave 10 dict begin -691 550 moveto +312 628 moveto (cic_acic) [10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] xshow @@ -369,66 +369,36 @@ end grestore end grestore % acic_content -> cic_acic -newpath 751 626 moveto -748 616 744 604 741 593 curveto +newpath 717 825 moveto +691 809 653 789 617 778 curveto +592 769 579 786 557 770 curveto +532 750 552 725 528 704 curveto +490 668 465 687 416 668 curveto +410 665 404 663 398 660 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 744 592 moveto -739 583 lineto -738 593 lineto +newpath 399 657 moveto +389 655 lineto +396 663 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 744 592 moveto -739 583 lineto -738 593 lineto -closepath -stroke -end grestore - -% cic_proof_checking -gsave 10 dict begin -513 454 110 25 ellipse_path -stroke -gsave 10 dict begin -417 446 moveto -(cic_proof_checking) -[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] -xshow -end grestore -end grestore - -% cic_acic -> cic_proof_checking -newpath 706 535 moveto -688 520 662 500 636 488 curveto -626 483 615 479 604 475 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 605 472 moveto -594 472 lineto -603 478 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 605 472 moveto -594 472 lineto -603 478 lineto +newpath 399 657 moveto +389 655 lineto +396 663 lineto closepath stroke end grestore % cic_disambiguation gsave 10 dict begin -758 740 109 25 ellipse_path +752 936 109 25 ellipse_path stroke gsave 10 dict begin -663 732 moveto +657 928 moveto (cic_disambiguation) [10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] xshow @@ -436,32 +406,32 @@ end grestore end grestore % cic_disambiguation -> acic_content -newpath 758 714 moveto -758 706 758 697 758 688 curveto +newpath 752 910 moveto +752 902 752 893 752 884 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 762 688 moveto -758 678 lineto -755 688 lineto +newpath 756 884 moveto +752 874 lineto +749 884 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 762 688 moveto -758 678 lineto -755 688 lineto +newpath 756 884 moveto +752 874 lineto +749 884 lineto closepath stroke end grestore % cic_unification gsave 10 dict begin -307 652 86 25 ellipse_path +359 848 86 25 ellipse_path stroke gsave 10 dict begin -235 644 moveto +287 840 moveto (cic_unification) [10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] xshow @@ -469,32 +439,32 @@ end grestore end grestore % cic_disambiguation -> cic_unification -newpath 674 724 moveto -592 708 471 684 390 668 curveto +newpath 672 918 moveto +604 903 507 881 439 865 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 390 665 moveto -380 666 lineto -389 671 lineto +newpath 439 862 moveto +429 863 lineto +438 868 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 390 665 moveto -380 666 lineto -389 671 lineto +newpath 439 862 moveto +429 863 lineto +438 868 lineto closepath stroke end grestore % whelp gsave 10 dict begin -325 558 44 25 ellipse_path +474 736 44 25 ellipse_path stroke gsave 10 dict begin -295 550 moveto +444 728 moveto (whelp) [17.28 12 10.56 6.72 12] xshow @@ -502,32 +472,32 @@ end grestore end grestore % cic_disambiguation -> whelp -newpath 704 718 moveto -618 681 451 611 370 577 curveto +newpath 718 912 moveto +666 874 565 801 510 762 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 372 574 moveto -361 573 lineto -369 580 lineto +newpath 512 759 moveto +502 756 lineto +508 765 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 372 574 moveto -361 573 lineto -369 580 lineto +newpath 512 759 moveto +502 756 lineto +508 765 lineto closepath stroke end grestore % content_pres gsave 10 dict begin -963 740 76 25 ellipse_path +957 936 76 25 ellipse_path stroke gsave 10 dict begin -901 732 moveto +895 928 moveto (content_pres) [10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] xshow @@ -535,32 +505,32 @@ end grestore end grestore % content_pres -> acic_content -newpath 916 720 moveto -885 707 846 690 814 676 curveto +newpath 910 916 moveto +879 903 840 886 808 872 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 816 673 moveto -805 672 lineto -813 679 lineto +newpath 810 869 moveto +799 868 lineto +807 875 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 816 673 moveto -805 672 lineto -813 679 lineto +newpath 810 869 moveto +799 868 lineto +807 875 lineto closepath stroke end grestore % utf8_macros gsave 10 dict begin -844 366 75 25 ellipse_path +873 366 75 25 ellipse_path stroke gsave 10 dict begin -783 358 moveto +812 358 moveto (utf8_macros) [12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] xshow @@ -568,87 +538,191 @@ end grestore end grestore % content_pres -> utf8_macros -newpath 955 715 moveto -934 649 879 476 855 401 curveto +newpath 949 911 moveto +937 873 917 799 917 736 curveto +917 736 917 736 917 542 curveto +917 492 900 436 888 401 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 891 399 moveto +884 391 lineto +884 402 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 891 399 moveto +884 391 lineto +884 402 lineto +closepath +stroke +end grestore + +% grafite_parser +gsave 10 dict begin +724 1128 81 25 ellipse_path +stroke +gsave 10 dict begin +657 1120 moveto +(grafite_parser) +[12 7.92 10.56 7.92 6.72 6.72 10.56 12 12 10.56 7.92 9.36 10.56 7.92] +xshow +end grestore +end grestore + +% sheath +gsave 10 dict begin +752 1024 45 25 ellipse_path +stroke +gsave 10 dict begin +721 1016 moveto +(sheath) +[9.36 12 10.56 10.56 6.72 12] +xshow +end grestore +end grestore + +% grafite_parser -> sheath +newpath 731 1103 moveto +734 1090 739 1074 743 1059 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 858 400 moveto -852 391 lineto -852 402 lineto +newpath 746 1059 moveto +745 1049 lineto +740 1058 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 858 400 moveto -852 391 lineto -852 402 lineto +newpath 746 1059 moveto +745 1049 lineto +740 1058 lineto closepath stroke end grestore % grafite gsave 10 dict begin -830 828 46 25 ellipse_path +161 936 46 25 ellipse_path stroke gsave 10 dict begin -798 820 moveto +129 928 moveto (grafite) [12 7.92 10.56 7.92 6.72 6.72 10.56] xshow end grestore end grestore -% grafite -> content_pres -newpath 860 808 moveto -877 797 900 782 920 769 curveto +% grafite_parser -> grafite +newpath 670 1108 moveto +661 1106 651 1103 642 1102 curveto +625 1098 498 1104 484 1094 curveto +449 1066 489 1027 455 998 curveto +389 938 345 981 258 962 curveto +243 959 227 955 213 951 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 922 772 moveto -928 763 lineto -918 766 lineto +newpath 214 948 moveto +203 948 lineto +212 954 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 922 772 moveto -928 763 lineto -918 766 lineto +newpath 214 948 moveto +203 948 lineto +212 954 lineto closepath stroke end grestore -% cic_unification -> cic_proof_checking -newpath 337 628 moveto -350 617 366 604 379 592 curveto -416 557 456 515 483 487 curveto +% sheath -> cic_disambiguation +newpath 752 998 moveto +752 990 752 981 752 972 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 486 489 moveto -490 479 lineto -481 484 lineto +newpath 756 972 moveto +752 962 lineto +749 972 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 486 489 moveto -490 479 lineto -481 484 lineto +newpath 756 972 moveto +752 962 lineto +749 972 lineto +closepath +stroke +end grestore + +% sheath -> content_pres +newpath 789 1008 moveto +820 995 865 976 901 960 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 902 963 moveto +910 956 lineto +899 957 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 902 963 moveto +910 956 lineto +899 957 lineto +closepath +stroke +end grestore + +% library +gsave 10 dict begin +359 736 46 25 ellipse_path +stroke +gsave 10 dict begin +327 728 moveto +(library) +[6.72 6.72 12 7.92 10.56 7.92 12] +xshow +end grestore +end grestore + +% cic_unification -> library +newpath 359 822 moveto +359 807 359 788 359 772 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 363 772 moveto +359 762 lineto +356 772 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 363 772 moveto +359 762 lineto +356 772 lineto closepath stroke end grestore % tactics gsave 10 dict begin -301 740 45 25 ellipse_path +313 936 45 25 ellipse_path stroke gsave 10 dict begin -270 732 moveto +282 928 moveto (tactics) [6.72 10.56 10.56 6.72 6.72 10.56 9.36] xshow @@ -656,56 +730,56 @@ end grestore end grestore % tactics -> cic_unification -newpath 303 714 moveto -304 706 304 697 305 688 curveto +newpath 326 911 moveto +331 902 336 892 340 882 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 309 688 moveto -305 678 lineto -302 688 lineto +newpath 343 883 moveto +345 873 lineto +337 880 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 309 688 moveto -305 678 lineto -302 688 lineto +newpath 343 883 moveto +345 873 lineto +337 880 lineto closepath stroke end grestore % tactics -> whelp -newpath 264 725 moveto -245 714 222 699 211 678 curveto -199 654 196 639 211 618 curveto -230 591 252 607 280 592 curveto -284 590 288 588 291 585 curveto +newpath 289 914 moveto +279 903 268 889 263 874 curveto +249 833 234 808 263 778 curveto +275 765 399 774 415 770 curveto +423 768 430 764 437 761 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 293 588 moveto -299 579 lineto -289 582 lineto +newpath 439 764 moveto +446 756 lineto +436 758 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 293 588 moveto -299 579 lineto -289 582 lineto +newpath 439 764 moveto +446 756 lineto +436 758 lineto closepath stroke end grestore % paramodulation gsave 10 dict begin -301 828 90 25 ellipse_path +355 1024 90 25 ellipse_path stroke gsave 10 dict begin -225 820 moveto +279 1016 moveto (paramodulation) [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12] xshow @@ -713,44 +787,123 @@ end grestore end grestore % paramodulation -> tactics -newpath 301 802 moveto -301 794 301 785 301 776 curveto +newpath 343 999 moveto +338 990 333 980 329 970 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 305 776 moveto -301 766 lineto -298 776 lineto +newpath 332 969 moveto +325 961 lineto +326 972 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 305 776 moveto -301 766 lineto -298 776 lineto +newpath 332 969 moveto +325 961 lineto +326 972 lineto closepath stroke end grestore % cic gsave 10 dict begin -420 366 28 25 ellipse_path +408 454 28 25 ellipse_path stroke gsave 10 dict begin -406 358 moveto +394 446 moveto (cic) [10.56 6.72 10.56] xshow end grestore end grestore +% grafite -> cic +newpath 160 910 moveto +158 872 155 798 155 736 curveto +155 736 155 736 155 636 curveto +155 556 219 554 288 516 curveto +327 495 343 502 379 480 curveto +379 480 380 480 380 479 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 382 482 moveto +388 473 lineto +378 476 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 382 482 moveto +388 473 lineto +378 476 lineto +closepath +stroke +end grestore + +% grafite_engine +gsave 10 dict begin +161 1024 84 25 ellipse_path +stroke +gsave 10 dict begin +91 1016 moveto +(grafite_engine) +[12 7.92 10.56 7.92 6.72 6.72 10.56 12 10.56 12 12 6.72 12 10.56] +xshow +end grestore +end grestore + +% grafite_engine -> tactics +newpath 200 1001 moveto +222 989 249 973 272 960 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 274 963 moveto +281 955 lineto +271 957 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 274 963 moveto +281 955 lineto +271 957 lineto +closepath +stroke +end grestore + +% grafite_engine -> grafite +newpath 161 998 moveto +161 990 161 981 161 972 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 165 972 moveto +161 962 lineto +158 972 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 165 972 moveto +161 962 lineto +158 972 lineto +closepath +stroke +end grestore + % urimanager gsave 10 dict begin -515 278 70 25 ellipse_path +424 366 70 25 ellipse_path stroke gsave 10 dict begin -459 270 moveto +368 358 moveto (urimanager) [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] xshow @@ -758,32 +911,32 @@ end grestore end grestore % cic -> urimanager -newpath 440 347 moveto -452 336 468 322 482 309 curveto +newpath 413 429 moveto +414 420 416 411 417 402 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 484 312 moveto -489 302 lineto -479 307 lineto +newpath 420 402 moveto +419 392 lineto +414 401 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 484 312 moveto -489 302 lineto -479 307 lineto +newpath 420 402 moveto +419 392 lineto +414 401 lineto closepath stroke end grestore % xml gsave 10 dict begin -701 174 33 25 ellipse_path +622 174 33 25 ellipse_path stroke gsave 10 dict begin -682 166 moveto +603 166 moveto (xml) [12 18.72 6.72] xshow @@ -791,54 +944,67 @@ end grestore end grestore % cic -> xml -newpath 414 341 moveto -407 306 401 243 435 208 curveto -450 192 585 181 657 177 curveto +newpath 383 440 moveto +369 431 352 417 344 400 curveto +325 358 319 334 344 296 curveto +396 216 514 188 578 178 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 657 180 moveto -667 176 lineto -657 174 lineto +newpath 578 181 moveto +588 177 lineto +578 175 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 657 180 moveto -667 176 lineto -657 174 lineto +newpath 578 181 moveto +588 177 lineto +578 175 lineto closepath stroke end grestore +% cic_proof_checking +gsave 10 dict begin +408 542 110 25 ellipse_path +stroke +gsave 10 dict begin +312 534 moveto +(cic_proof_checking) +[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] +xshow +end grestore +end grestore + % cic_proof_checking -> cic -newpath 487 429 moveto -475 417 460 404 448 392 curveto +newpath 408 516 moveto +408 508 408 499 408 490 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 450 389 moveto -440 385 lineto -445 394 lineto +newpath 412 490 moveto +408 480 lineto +405 490 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 450 389 moveto -440 385 lineto -445 394 lineto +newpath 412 490 moveto +408 480 lineto +405 490 lineto closepath stroke end grestore % getter gsave 10 dict begin -513 366 42 25 ellipse_path +500 454 42 25 ellipse_path stroke gsave 10 dict begin -485 358 moveto +472 446 moveto (getter) [12 10.56 6.72 6.72 10.56 7.92] xshow @@ -846,53 +1012,53 @@ end grestore end grestore % cic_proof_checking -> getter -newpath 513 428 moveto -513 420 513 411 513 402 curveto +newpath 418 516 moveto +430 501 446 487 460 477 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 517 402 moveto -513 392 lineto -510 402 lineto +newpath 462 480 moveto +469 472 lineto +459 474 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 517 402 moveto -513 392 lineto -510 402 lineto +newpath 462 480 moveto +469 472 lineto +459 474 lineto closepath stroke end grestore % getter -> urimanager -newpath 514 340 moveto -514 332 514 323 514 314 curveto +newpath 480 431 moveto +472 421 461 409 452 398 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 518 314 moveto -514 304 lineto -511 314 lineto +newpath 455 396 moveto +445 391 lineto +450 401 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 518 314 moveto -514 304 lineto -511 314 lineto +newpath 455 396 moveto +445 391 lineto +450 401 lineto closepath stroke end grestore % registry gsave 10 dict begin -701 278 52 25 ellipse_path +748 262 52 25 ellipse_path stroke gsave 10 dict begin -663 270 moveto +710 254 moveto (registry) [7.92 10.56 12 6.72 9.36 6.72 7.92 12] xshow @@ -900,87 +1066,102 @@ end grestore end grestore % getter -> registry -newpath 547 350 moveto -577 336 621 316 654 300 curveto +newpath 501 428 moveto +505 392 517 327 558 296 curveto +570 287 673 291 686 288 curveto +691 287 696 285 700 284 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 655 303 moveto -663 296 lineto -652 297 lineto +newpath 702 287 moveto +710 280 lineto +699 280 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 655 303 moveto -663 296 lineto -652 297 lineto +newpath 702 287 moveto +710 280 lineto +699 280 lineto closepath stroke end grestore -% metadata +% logger gsave 10 dict begin -325 454 58 25 ellipse_path +613 366 45 25 ellipse_path stroke gsave 10 dict begin -281 446 moveto -(metadata) -[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +582 358 moveto +(logger) +[6.72 12 12 12 10.56 7.92] xshow end grestore end grestore -% metadata -> cic -newpath 350 431 moveto -363 419 379 404 392 392 curveto +% getter -> logger +newpath 526 434 moveto +541 422 561 406 578 393 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 395 394 moveto -400 385 lineto -390 389 lineto +newpath 580 396 moveto +586 387 lineto +576 390 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 395 394 moveto -400 385 lineto -390 389 lineto +newpath 580 396 moveto +586 387 lineto +576 390 lineto closepath stroke end grestore -% metadata -> getter -newpath 369 437 moveto -401 424 442 408 458 400 curveto -464 397 470 394 475 390 curveto +% metadata +gsave 10 dict begin +484 636 58 25 ellipse_path +stroke +gsave 10 dict begin +440 628 moveto +(metadata) +[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +xshow +end grestore +end grestore + +% metadata -> cic +newpath 505 612 moveto +525 586 548 546 528 516 curveto +507 483 483 498 448 480 curveto +445 478 443 477 440 475 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 477 393 moveto -484 385 lineto -474 387 lineto +newpath 441 472 moveto +431 469 lineto +437 477 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 477 393 moveto -484 385 lineto -474 387 lineto +newpath 441 472 moveto +431 469 lineto +437 477 lineto closepath stroke end grestore % hmysql gsave 10 dict begin -699 366 50 25 ellipse_path +728 366 50 25 ellipse_path stroke gsave 10 dict begin -663 358 moveto +692 358 moveto (hmysql) [12 18.72 12 9.36 12 6.72] xshow @@ -988,55 +1169,117 @@ end grestore end grestore % metadata -> hmysql -newpath 367 436 moveto -375 433 384 430 393 428 curveto -499 402 533 432 636 400 curveto -644 398 651 394 658 391 curveto +newpath 539 626 moveto +600 616 638 623 686 568 curveto +727 521 731 446 730 402 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 660 394 moveto -667 386 lineto -657 388 lineto +newpath 734 402 moveto +730 392 lineto +727 402 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 660 394 moveto -667 386 lineto -657 388 lineto +newpath 734 402 moveto +730 392 lineto +727 402 lineto closepath stroke end grestore % whelp -> metadata -newpath 325 532 moveto -325 519 325 504 325 490 curveto +newpath 477 711 moveto +479 699 480 685 481 672 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 484 672 moveto +482 662 lineto +478 672 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 484 672 moveto +482 662 lineto +478 672 lineto +closepath +stroke +end grestore + +% library -> metadata +newpath 386 715 moveto +404 700 428 680 448 664 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 450 667 moveto +456 658 lineto +446 661 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 450 667 moveto +456 658 lineto +446 661 lineto +closepath +stroke +end grestore + +% library -> cic_acic +newpath 357 711 moveto +356 699 355 685 355 672 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 358 672 moveto +354 662 lineto +352 672 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 358 672 moveto +354 662 lineto +352 672 lineto +closepath +stroke +end grestore + +% cic_acic -> cic_proof_checking +newpath 367 611 moveto +373 600 381 587 388 576 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 329 490 moveto -325 480 lineto -322 490 lineto +newpath 391 577 moveto +393 567 lineto +385 574 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 329 490 moveto -325 480 lineto -322 490 lineto +newpath 391 577 moveto +393 567 lineto +385 574 lineto closepath stroke end grestore % extlib gsave 10 dict begin -701 86 42 25 ellipse_path +622 86 42 25 ellipse_path stroke gsave 10 dict begin -673 78 moveto +594 78 moveto (extlib) [10.56 12 6.72 6.72 6.72 12] xshow @@ -1045,10 +1288,10 @@ end grestore % hgdome gsave 10 dict begin -827 278 54 25 ellipse_path +622 262 54 25 ellipse_path stroke gsave 10 dict begin -787 270 moveto +582 254 moveto (hgdome) [12 12 12 12 18.72 10.56] xshow @@ -1056,86 +1299,85 @@ end grestore end grestore % hgdome -> xml -newpath 809 254 moveto -797 239 780 221 763 208 curveto -756 202 747 197 739 192 curveto +newpath 622 236 moveto +622 228 622 219 622 210 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 740 189 moveto -730 187 lineto -737 195 lineto +newpath 626 210 moveto +622 200 lineto +619 210 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 740 189 moveto -730 187 lineto -737 195 lineto +newpath 626 210 moveto +622 200 lineto +619 210 lineto closepath stroke end grestore % hmysql -> registry -newpath 700 340 moveto -700 332 700 323 700 314 curveto +newpath 733 341 moveto +735 328 738 312 741 298 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 704 314 moveto -700 304 lineto -697 314 lineto +newpath 744 298 moveto +743 288 lineto +738 297 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 704 314 moveto -700 304 lineto -697 314 lineto +newpath 744 298 moveto +743 288 lineto +738 297 lineto closepath stroke end grestore % registry -> xml -newpath 701 252 moveto -701 239 701 224 701 210 curveto +newpath 718 241 moveto +699 228 674 211 655 197 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 705 210 moveto -701 200 lineto -698 210 lineto +newpath 657 194 moveto +647 191 lineto +653 200 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 705 210 moveto -701 200 lineto -698 210 lineto +newpath 657 194 moveto +647 191 lineto +653 200 lineto closepath stroke end grestore % xml -> extlib -newpath 701 148 moveto -701 140 701 131 701 122 curveto +newpath 622 148 moveto +622 140 622 131 622 122 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 705 122 moveto -701 112 lineto -698 122 lineto +newpath 626 122 moveto +622 112 lineto +619 122 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 705 122 moveto -701 112 lineto -698 122 lineto +newpath 626 122 moveto +622 112 lineto +619 122 lineto closepath stroke end grestore @@ -1145,26 +1387,26 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 136 590 moveto -0 590 lineto -0 526 lineto -136 526 lineto +newpath 711 768 moveto +575 768 lineto +575 704 lineto +711 704 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 136 590 moveto -0 590 lineto -0 526 lineto -136 526 lineto +newpath 711 768 moveto +575 768 lineto +575 704 lineto +711 704 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -8 564 moveto +583 742 moveto (Dependency) [17.28 10.56 12 10.56 12 12 10.56 12 10.56 12] xshow -24 536 moveto +599 714 moveto (Analyzer) [17.28 12 10.56 6.72 12 10.56 10.56 7.92] xshow @@ -1172,24 +1414,22 @@ end grestore end grestore % DependencyAnalyzer -> metadata -newpath 94 526 moveto -108 512 126 496 145 488 curveto -170 477 240 486 266 480 curveto -270 479 273 478 277 477 curveto +newpath 592 704 moveto +570 691 546 675 526 662 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 278 480 moveto -286 473 lineto -275 474 lineto +newpath 527 659 moveto +517 657 lineto +524 665 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 278 480 moveto -286 473 lineto -275 474 lineto +newpath 527 659 moveto +517 657 lineto +524 665 lineto closepath stroke end grestore @@ -1199,22 +1439,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 248 472 moveto -172 472 lineto -172 436 lineto -248 436 lineto +newpath 635 560 moveto +559 560 lineto +559 524 lineto +635 524 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 248 472 moveto -172 472 lineto -172 436 lineto -248 436 lineto +newpath 635 560 moveto +559 560 lineto +559 524 lineto +635 524 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -180 446 moveto +567 534 moveto (Getter) [17.28 10.56 6.72 6.72 10.56 7.92] xshow @@ -1222,24 +1462,22 @@ end grestore end grestore % Getter -> getter -newpath 237 436 moveto -242 433 248 430 254 428 curveto -341 397 372 430 458 400 curveto -465 397 471 394 477 391 curveto +newpath 577 524 moveto +563 512 546 496 532 483 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 479 394 moveto -486 386 lineto -476 388 lineto +newpath 534 480 moveto +524 476 lineto +529 485 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 479 394 moveto -486 386 lineto -476 388 lineto +newpath 534 480 moveto +524 476 lineto +529 485 lineto closepath stroke end grestore @@ -1249,22 +1487,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 459 942 moveto -381 942 lineto -381 906 lineto -459 906 lineto +newpath 394 1226 moveto +316 1226 lineto +316 1190 lineto +394 1190 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 459 942 moveto -381 942 lineto -381 906 lineto -459 906 lineto +newpath 394 1226 moveto +316 1226 lineto +316 1190 lineto +394 1190 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -388 916 moveto +323 1200 moveto (Matita) [21.36 10.56 6.72 6.72 6.72 10.56] xshow @@ -1272,67 +1510,113 @@ end grestore end grestore % Matita -> cic_disambiguation -newpath 417 906 moveto -415 879 414 830 439 802 curveto -504 731 554 751 640 746 curveto +newpath 372 1190 moveto +393 1167 429 1129 458 1094 curveto +493 1052 487 1028 531 998 curveto +565 975 607 961 646 951 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 640 749 moveto -650 745 lineto -640 743 lineto +newpath 647 954 moveto +656 949 lineto +646 948 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 640 749 moveto -650 745 lineto -640 743 lineto +newpath 647 954 moveto +656 949 lineto +646 948 lineto closepath stroke end grestore -% Matita -> grafite -newpath 459 923 moveto -547 921 756 914 783 898 curveto -798 890 808 876 816 862 curveto +% Matita -> grafite_parser +newpath 394 1205 moveto +450 1199 556 1186 642 1162 curveto +651 1160 660 1156 669 1153 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 819 864 moveto -820 853 lineto -813 861 lineto +newpath 670 1156 moveto +678 1149 lineto +667 1150 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 819 864 moveto -820 853 lineto -813 861 lineto +newpath 670 1156 moveto +678 1149 lineto +667 1150 lineto closepath stroke end grestore % Matita -> paramodulation -newpath 381 919 moveto -354 915 321 908 311 898 curveto -302 889 299 876 298 864 curveto +newpath 355 1190 moveto +355 1160 355 1099 355 1060 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 302 864 moveto -298 854 lineto -295 864 lineto +newpath 359 1060 moveto +355 1050 lineto +352 1060 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 302 864 moveto -298 854 lineto -295 864 lineto +newpath 359 1060 moveto +355 1050 lineto +352 1060 lineto +closepath +stroke +end grestore + +% Matita -> grafite_engine +newpath 336 1190 moveto +303 1158 236 1094 194 1056 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 197 1054 moveto +187 1049 lineto +192 1059 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 197 1054 moveto +187 1049 lineto +192 1059 lineto +closepath +stroke +end grestore + +% Matita -> hgdome +newpath 316 1204 moveto +253 1196 129 1171 64 1094 curveto +44 1069 48 1055 48 1024 curveto +48 1024 48 1024 48 454 curveto +48 327 166 338 285 296 curveto +334 278 473 269 557 265 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 557 268 moveto +567 264 lineto +557 262 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 557 268 moveto +567 264 lineto +557 262 lineto closepath stroke end grestore @@ -1342,26 +1626,26 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 250 590 moveto -154 590 lineto -154 526 lineto -250 526 lineto +newpath 279 668 moveto +183 668 lineto +183 604 lineto +279 604 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 250 590 moveto -154 590 lineto -154 526 lineto -250 526 lineto +newpath 279 668 moveto +183 668 lineto +183 604 lineto +279 604 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -175 564 moveto +204 642 moveto (Proof) [13.44 7.92 12 12 7.92] xshow -162 536 moveto +191 614 moveto (Checker) [16.08 12 10.56 10.56 12 10.56 7.92] xshow @@ -1369,24 +1653,23 @@ end grestore end grestore % ProofChecker -> cic_proof_checking -newpath 218 526 moveto -226 512 238 496 254 488 curveto -268 480 378 482 393 480 curveto -404 478 415 476 426 474 curveto +newpath 279 607 moveto +281 606 283 605 285 604 curveto +306 592 330 580 351 569 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 427 477 moveto -436 472 lineto -426 471 lineto +newpath 352 572 moveto +360 565 lineto +349 566 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 427 477 moveto -436 472 lineto -426 471 lineto +newpath 352 572 moveto +360 565 lineto +349 566 lineto closepath stroke end grestore @@ -1396,22 +1679,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 632 846 moveto -546 846 lineto -546 810 lineto -632 810 lineto +newpath 626 1042 moveto +540 1042 lineto +540 1006 lineto +626 1006 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 632 846 moveto -546 846 lineto -546 810 lineto -632 810 lineto +newpath 626 1042 moveto +540 1042 lineto +540 1006 lineto +626 1006 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -553 820 moveto +547 1016 moveto (Uwobo) [17.28 17.28 12 12 12] xshow @@ -1419,24 +1702,24 @@ end grestore end grestore % Uwobo -> content_pres -newpath 618 810 moveto -624 807 630 804 636 802 curveto -739 767 772 789 877 766 curveto -884 765 890 763 897 761 curveto +newpath 612 1006 moveto +618 1003 624 1000 630 998 curveto +733 963 766 985 871 962 curveto +878 961 884 959 891 957 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 898 764 moveto -907 758 lineto -896 758 lineto +newpath 892 960 moveto +901 954 lineto +890 954 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 898 764 moveto -907 758 lineto -896 758 lineto +newpath 892 960 moveto +901 954 lineto +890 954 lineto closepath stroke end grestore @@ -1446,69 +1729,45 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 528 846 moveto -448 846 lineto -448 810 lineto -528 810 lineto +newpath 764 1226 moveto +684 1226 lineto +684 1190 lineto +764 1190 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 528 846 moveto -448 846 lineto -448 810 lineto -528 810 lineto +newpath 764 1226 moveto +684 1226 lineto +684 1190 lineto +764 1190 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -455 820 moveto +691 1200 moveto (Whelp) [22.56 12 10.56 6.72 12] xshow end grestore end grestore -% Whelp -> cic_disambiguation -newpath 520 810 moveto -526 807 531 804 537 802 curveto -580 785 628 770 669 760 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 670 763 moveto -679 758 lineto -669 757 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 670 763 moveto -679 758 lineto -669 757 lineto -closepath -stroke -end grestore - -% Whelp -> content_pres -newpath 518 810 moveto -524 807 531 804 537 802 curveto -683 757 729 796 877 766 curveto -884 765 891 763 898 761 curveto +% Whelp -> grafite_parser +newpath 724 1190 moveto +724 1182 724 1173 724 1164 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 899 764 moveto -908 758 lineto -897 758 lineto +newpath 728 1164 moveto +724 1154 lineto +721 1164 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 899 764 moveto -908 758 lineto -897 758 lineto +newpath 728 1164 moveto +724 1154 lineto +721 1164 lineto closepath stroke end grestore