X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2FlibrariesCluster.ps;h=94b0666878cc431f2a05c84c04632e55f448921f;hb=114ee592d3da9b49abfd4c1b186cba1e170075dc;hp=03d3665d834a0c338473f57bb544be3fdcf3f69d;hpb=ffbef6329458347da5805b12c98819cc0ce4ab73;p=helm.git diff --git a/helm/papers/matita/librariesCluster.ps b/helm/papers/matita/librariesCluster.ps index 03d3665d8..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 1332 937 +%%BoundingBox: 35 35 1108 1263 %%EndComments save %%BeginProlog @@ -230,10 +230,10 @@ def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 1332 937 +%%PageBoundingBox: 36 36 1108 1263 %%PageOrientation: Portrait gsave -35 35 1297 902 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 772 488 moveto -1201 488 lineto -1201 856 lineto -772 856 lineto +newpath 634 778 moveto +1063 778 lineto +1063 1162 lineto +634 1162 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 772 488 moveto -1201 488 lineto -1201 856 lineto -772 856 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 -780 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 330 612 moveto -580 612 lineto -580 892 lineto -330 892 lineto +newpath 68 814 moveto +454 814 lineto +454 1094 lineto +68 1094 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 330 612 moveto -580 612 lineto -580 892 lineto -330 892 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 -338 866 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 232 208 moveto -606 208 lineto -606 592 lineto -232 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 232 208 moveto -606 208 lineto -606 592 lineto -232 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 -239 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 614 16 moveto -902 16 lineto -902 400 lineto -614 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 614 16 moveto -902 16 lineto -902 400 lineto -614 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 -816 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 -915 646 75 25 ellipse_path +752 848 75 25 ellipse_path stroke gsave 10 dict begin -854 638 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 -876 558 54 25 ellipse_path +352 636 54 25 ellipse_path stroke gsave 10 dict begin -836 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 904 621 moveto -900 612 895 602 891 592 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 894 591 moveto -887 583 lineto -888 594 lineto +newpath 399 657 moveto +389 655 lineto +396 663 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 894 591 moveto -887 583 lineto -888 594 lineto -closepath -stroke -end grestore - -% cic_proof_checking -gsave 10 dict begin -487 454 110 25 ellipse_path -stroke -gsave 10 dict begin -391 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 863 533 moveto -854 517 840 498 821 488 curveto -803 477 693 468 604 462 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 604 459 moveto -594 461 lineto -604 465 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 604 459 moveto -594 461 lineto -604 465 lineto +newpath 399 657 moveto +389 655 lineto +396 663 lineto closepath stroke end grestore % cic_disambiguation gsave 10 dict begin -890 734 109 25 ellipse_path +752 936 109 25 ellipse_path stroke gsave 10 dict begin -795 726 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 897 709 moveto -900 700 903 691 905 682 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 908 683 moveto -908 672 lineto -902 681 lineto +newpath 756 884 moveto +752 874 lineto +749 884 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 908 683 moveto -908 672 lineto -902 681 lineto +newpath 756 884 moveto +752 874 lineto +749 884 lineto closepath stroke end grestore % cic_unification gsave 10 dict begin -485 646 86 25 ellipse_path +359 848 86 25 ellipse_path stroke gsave 10 dict begin -413 638 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 810 717 moveto -738 702 636 679 565 663 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 565 660 moveto -555 661 lineto -564 666 lineto +newpath 439 862 moveto +429 863 lineto +438 868 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 565 660 moveto -555 661 lineto -564 666 lineto +newpath 439 862 moveto +429 863 lineto +438 868 lineto closepath stroke end grestore % whelp gsave 10 dict begin -336 558 44 25 ellipse_path +474 736 44 25 ellipse_path stroke gsave 10 dict begin -306 550 moveto +444 728 moveto (whelp) [17.28 12 10.56 6.72 12] xshow @@ -502,34 +472,32 @@ end grestore end grestore % cic_disambiguation -> whelp -newpath 845 711 moveto -786 682 680 634 584 612 curveto -535 600 397 620 354 592 curveto -354 592 353 592 353 591 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 356 589 moveto -347 583 lineto -350 593 lineto +newpath 512 759 moveto +502 756 lineto +508 765 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 356 589 moveto -347 583 lineto -350 593 lineto +newpath 512 759 moveto +502 756 lineto +508 765 lineto closepath stroke end grestore % content_pres gsave 10 dict begin -1095 734 76 25 ellipse_path +957 936 76 25 ellipse_path stroke gsave 10 dict begin -1033 726 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 @@ -537,32 +505,32 @@ end grestore end grestore % content_pres -> acic_content -newpath 1051 713 moveto -1026 700 994 685 967 672 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 968 669 moveto -958 667 lineto -965 675 lineto +newpath 810 869 moveto +799 868 lineto +807 875 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 968 669 moveto -958 667 lineto -965 675 lineto +newpath 810 869 moveto +799 868 lineto +807 875 lineto closepath stroke end grestore % utf8_macros gsave 10 dict begin -818 366 75 25 ellipse_path +873 366 75 25 ellipse_path stroke gsave 10 dict begin -757 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 @@ -570,87 +538,191 @@ end grestore end grestore % content_pres -> utf8_macros -newpath 1082 709 moveto -1057 662 1000 562 940 488 curveto -914 454 879 421 854 397 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 856 394 moveto -846 390 lineto -851 399 lineto +newpath 746 1059 moveto +745 1049 lineto +740 1058 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 856 394 moveto -846 390 lineto -851 399 lineto +newpath 746 1059 moveto +745 1049 lineto +740 1058 lineto closepath stroke end grestore % grafite gsave 10 dict begin -1095 822 46 25 ellipse_path +161 936 46 25 ellipse_path stroke gsave 10 dict begin -1063 814 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 1095 796 moveto -1095 788 1095 779 1095 770 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 214 948 moveto +203 948 lineto +212 954 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 214 948 moveto +203 948 lineto +212 954 lineto +closepath +stroke +end grestore + +% 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 756 972 moveto +752 962 lineto +749 972 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +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 1099 770 moveto -1095 760 lineto -1092 770 lineto +newpath 902 963 moveto +910 956 lineto +899 957 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 1099 770 moveto -1095 760 lineto -1092 770 lineto +newpath 902 963 moveto +910 956 lineto +899 957 lineto closepath stroke end grestore -% cic_unification -> cic_proof_checking -newpath 485 620 moveto -486 586 486 528 487 490 curveto +% 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 491 490 moveto -487 480 lineto -484 490 lineto +newpath 363 772 moveto +359 762 lineto +356 772 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 491 490 moveto -487 480 lineto -484 490 lineto +newpath 363 772 moveto +359 762 lineto +356 772 lineto closepath stroke end grestore % tactics gsave 10 dict begin -482 734 45 25 ellipse_path +313 936 45 25 ellipse_path stroke gsave 10 dict begin -451 726 moveto +282 928 moveto (tactics) [6.72 10.56 10.56 6.72 6.72 10.56 9.36] xshow @@ -658,54 +730,56 @@ end grestore end grestore % tactics -> cic_unification -newpath 483 708 moveto -483 700 484 691 484 682 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 488 682 moveto -484 672 lineto -481 682 lineto +newpath 343 883 moveto +345 873 lineto +337 880 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 488 682 moveto -484 672 lineto -481 682 lineto +newpath 343 883 moveto +345 873 lineto +337 880 lineto closepath stroke end grestore % tactics -> whelp -newpath 451 715 moveto -428 701 399 682 389 672 curveto -370 648 356 617 347 593 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 350 591 moveto -343 583 lineto -343 594 lineto +newpath 439 764 moveto +446 756 lineto +436 758 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 350 591 moveto -343 583 lineto -343 594 lineto +newpath 439 764 moveto +446 756 lineto +436 758 lineto closepath stroke end grestore % paramodulation gsave 10 dict begin -479 822 90 25 ellipse_path +355 1024 90 25 ellipse_path stroke gsave 10 dict begin -403 814 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 480 796 moveto -480 788 481 779 481 770 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 485 770 moveto -481 760 lineto -478 770 lineto +newpath 332 969 moveto +325 961 lineto +326 972 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 485 770 moveto -481 760 lineto -478 770 lineto +newpath 332 969 moveto +325 961 lineto +326 972 lineto closepath stroke end grestore % cic gsave 10 dict begin -462 366 28 25 ellipse_path +408 454 28 25 ellipse_path stroke gsave 10 dict begin -448 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 -494 278 70 25 ellipse_path +424 366 70 25 ellipse_path stroke gsave 10 dict begin -438 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 471 341 moveto -474 332 478 322 481 312 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 314 moveto -485 303 lineto -478 311 lineto +newpath 420 402 moveto +419 392 lineto +414 401 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 484 314 moveto -485 303 lineto -478 311 lineto +newpath 420 402 moveto +419 392 lineto +414 401 lineto closepath stroke end grestore % xml gsave 10 dict begin -675 174 33 25 ellipse_path +622 174 33 25 ellipse_path stroke gsave 10 dict begin -656 166 moveto +603 166 moveto (xml) [12 18.72 6.72] xshow @@ -791,55 +944,67 @@ end grestore end grestore % cic -> xml -newpath 442 347 moveto -432 336 420 320 414 304 curveto -401 263 386 240 414 208 curveto -428 192 560 181 631 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 631 180 moveto -641 176 lineto -631 174 lineto +newpath 578 181 moveto +588 177 lineto +578 175 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 631 180 moveto -641 176 lineto -631 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 480 429 moveto -477 420 474 410 472 401 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 475 400 moveto -469 391 lineto -469 402 lineto +newpath 412 490 moveto +408 480 lineto +405 490 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 475 400 moveto -469 391 lineto -469 402 lineto +newpath 412 490 moveto +408 480 lineto +405 490 lineto closepath stroke end grestore % getter gsave 10 dict begin -323 366 42 25 ellipse_path +500 454 42 25 ellipse_path stroke gsave 10 dict begin -295 358 moveto +472 446 moveto (getter) [12 10.56 6.72 6.72 10.56 7.92] xshow @@ -847,53 +1012,53 @@ end grestore end grestore % cic_proof_checking -> getter -newpath 443 430 moveto -418 417 388 400 364 388 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 365 385 moveto -355 383 lineto -362 391 lineto +newpath 462 480 moveto +469 472 lineto +459 474 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 365 385 moveto -355 383 lineto -362 391 lineto +newpath 462 480 moveto +469 472 lineto +459 474 lineto closepath stroke end grestore % getter -> urimanager -newpath 356 349 moveto -380 336 416 318 444 304 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 446 307 moveto -453 299 lineto -443 301 lineto +newpath 455 396 moveto +445 391 lineto +450 401 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 446 307 moveto -453 299 lineto -443 301 lineto +newpath 455 396 moveto +445 391 lineto +450 401 lineto closepath stroke end grestore % registry gsave 10 dict begin -675 278 52 25 ellipse_path +748 262 52 25 ellipse_path stroke gsave 10 dict begin -637 270 moveto +710 254 moveto (registry) [7.92 10.56 12 6.72 9.36 6.72 7.92 12] xshow @@ -901,88 +1066,102 @@ end grestore end grestore % getter -> registry -newpath 362 355 moveto -381 350 404 345 424 340 curveto -507 321 530 327 610 304 curveto -615 302 621 300 626 298 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 627 301 moveto -636 295 lineto -625 295 lineto +newpath 702 287 moveto +710 280 lineto +699 280 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 627 301 moveto -636 295 lineto -625 295 lineto +newpath 702 287 moveto +710 280 lineto +699 280 lineto closepath stroke end grestore -% metadata +% logger gsave 10 dict begin -299 454 58 25 ellipse_path +613 366 45 25 ellipse_path stroke gsave 10 dict begin -255 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 336 434 moveto -364 419 401 399 428 385 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 430 388 moveto -437 380 lineto -427 382 lineto +newpath 580 396 moveto +586 387 lineto +576 390 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 430 388 moveto -437 380 lineto -427 382 lineto +newpath 580 396 moveto +586 387 lineto +576 390 lineto closepath stroke end grestore -% metadata -> getter -newpath 306 429 moveto -308 420 311 410 313 401 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 316 402 moveto -316 391 lineto -310 400 lineto +newpath 441 472 moveto +431 469 lineto +437 477 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 316 402 moveto -316 391 lineto -310 400 lineto +newpath 441 472 moveto +431 469 lineto +437 477 lineto closepath stroke end grestore % hmysql gsave 10 dict begin -673 366 50 25 ellipse_path +728 366 50 25 ellipse_path stroke gsave 10 dict begin -637 358 moveto +692 358 moveto (hmysql) [12 18.72 12 9.36 12 6.72] xshow @@ -990,55 +1169,117 @@ end grestore end grestore % metadata -> hmysql -newpath 341 436 moveto -349 433 358 430 367 428 curveto -473 402 507 432 610 400 curveto -618 398 625 394 632 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 634 394 moveto -641 386 lineto -631 388 lineto +newpath 734 402 moveto +730 392 lineto +727 402 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 634 394 moveto -641 386 lineto -631 388 lineto +newpath 734 402 moveto +730 392 lineto +727 402 lineto closepath stroke end grestore % whelp -> metadata -newpath 327 533 moveto -322 520 316 503 311 488 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 314 487 moveto -308 479 lineto -308 490 lineto +newpath 450 667 moveto +456 658 lineto +446 661 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 314 487 moveto -308 479 lineto -308 490 lineto +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 391 577 moveto +393 567 lineto +385 574 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 391 577 moveto +393 567 lineto +385 574 lineto closepath stroke end grestore % extlib gsave 10 dict begin -675 86 42 25 ellipse_path +622 86 42 25 ellipse_path stroke gsave 10 dict begin -647 78 moveto +594 78 moveto (extlib) [10.56 12 6.72 6.72 6.72 12] xshow @@ -1047,10 +1288,10 @@ end grestore % hgdome gsave 10 dict begin -801 278 54 25 ellipse_path +622 262 54 25 ellipse_path stroke gsave 10 dict begin -761 270 moveto +582 254 moveto (hgdome) [12 12 12 12 18.72 10.56] xshow @@ -1058,135 +1299,137 @@ end grestore end grestore % hgdome -> xml -newpath 783 254 moveto -771 239 754 221 737 208 curveto -730 202 721 197 713 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 714 189 moveto -704 187 lineto -711 195 lineto +newpath 626 210 moveto +622 200 lineto +619 210 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 714 189 moveto -704 187 lineto -711 195 lineto +newpath 626 210 moveto +622 200 lineto +619 210 lineto closepath stroke end grestore % hmysql -> registry -newpath 674 340 moveto -674 332 674 323 674 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 678 314 moveto -674 304 lineto -671 314 lineto +newpath 744 298 moveto +743 288 lineto +738 297 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 678 314 moveto -674 304 lineto -671 314 lineto +newpath 744 298 moveto +743 288 lineto +738 297 lineto closepath stroke end grestore % registry -> xml -newpath 675 252 moveto -675 239 675 224 675 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 679 210 moveto -675 200 lineto -672 210 lineto +newpath 657 194 moveto +647 191 lineto +653 200 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 679 210 moveto -675 200 lineto -672 210 lineto +newpath 657 194 moveto +647 191 lineto +653 200 lineto closepath stroke end grestore % xml -> extlib -newpath 675 148 moveto -675 140 675 131 675 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 679 122 moveto -675 112 lineto -672 122 lineto +newpath 626 122 moveto +622 112 lineto +619 122 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 679 122 moveto -675 112 lineto -672 122 lineto +newpath 626 122 moveto +622 112 lineto +619 122 lineto closepath stroke end grestore -% DrawGraph +% DependencyAnalyzer gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 128 472 moveto -0 472 lineto -0 436 lineto -128 436 lineto +newpath 711 768 moveto +575 768 lineto +575 704 lineto +711 704 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 128 472 moveto -0 472 lineto -0 436 lineto -128 436 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 -7 446 moveto -(DrawGraph) -[17.28 7.92 10.56 17.28 17.28 7.92 10.56 12 12] +583 742 moveto +(Dependency) +[17.28 10.56 12 10.56 12 12 10.56 12 10.56 12] +xshow +599 714 moveto +(Analyzer) +[17.28 12 10.56 6.72 12 10.56 10.56 7.92] xshow end grestore end grestore -% DrawGraph -> getter -newpath 114 436 moveto -122 433 130 430 137 428 curveto -184 411 237 394 275 381 curveto +% DependencyAnalyzer -> metadata +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 276 384 moveto -285 378 lineto -274 378 lineto +newpath 527 659 moveto +517 657 lineto +524 665 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 276 384 moveto -285 378 lineto -274 378 lineto +newpath 527 659 moveto +517 657 lineto +524 665 lineto closepath stroke end grestore @@ -1196,22 +1439,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 222 472 moveto -146 472 lineto -146 436 lineto -222 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 222 472 moveto -146 472 lineto -146 436 lineto -222 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 -154 446 moveto +567 534 moveto (Getter) [17.28 10.56 6.72 6.72 10.56 7.92] xshow @@ -1219,22 +1462,22 @@ end grestore end grestore % Getter -> getter -newpath 212 436 moveto -233 423 262 405 285 390 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 286 393 moveto -293 385 lineto -283 387 lineto +newpath 534 480 moveto +524 476 lineto +529 485 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 286 393 moveto -293 385 lineto -283 387 lineto +newpath 534 480 moveto +524 476 lineto +529 485 lineto closepath stroke end grestore @@ -1244,22 +1487,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 764 840 moveto -686 840 lineto -686 804 lineto -764 804 lineto +newpath 394 1226 moveto +316 1226 lineto +316 1190 lineto +394 1190 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 764 840 moveto -686 840 lineto -686 804 lineto -764 804 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 -693 814 moveto +323 1200 moveto (Matita) [21.36 10.56 6.72 6.72 6.72 10.56] xshow @@ -1267,165 +1510,216 @@ end grestore end grestore % Matita -> cic_disambiguation -newpath 754 804 moveto -759 801 764 798 768 796 curveto -789 784 813 772 833 762 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 835 765 moveto -842 757 lineto -832 759 lineto +newpath 647 954 moveto +656 949 lineto +646 948 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 835 765 moveto -842 757 lineto -832 759 lineto +newpath 647 954 moveto +656 949 lineto +646 948 lineto closepath stroke end grestore -% Matita -> tactics -newpath 694 804 moveto -689 801 683 798 677 796 curveto -630 776 574 759 534 748 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 535 745 moveto -524 745 lineto -533 751 lineto +newpath 670 1156 moveto +678 1149 lineto +667 1150 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 535 745 moveto -524 745 lineto -533 751 lineto +newpath 670 1156 moveto +678 1149 lineto +667 1150 lineto closepath stroke end grestore -% ProofChecker +% Matita -> paramodulation +newpath 355 1190 moveto +355 1160 355 1099 355 1060 curveto +stroke gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 764 576 moveto -614 576 lineto -614 540 lineto -764 540 lineto +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 359 1060 moveto +355 1050 lineto +352 1060 lineto closepath fill -0.584 0.220 0.933 nodecolor -newpath 764 576 moveto -614 576 lineto -614 540 lineto -764 540 lineto +0.000 0.000 0.000 edgecolor +newpath 359 1060 moveto +355 1050 lineto +352 1060 lineto closepath stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -622 550 moveto -(ProofChecker) -[13.44 7.92 12 12 7.92 16.08 12 10.56 10.56 12 10.56 7.92] -xshow 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 -% ProofChecker -> cic_proof_checking -newpath 673 540 moveto -659 524 635 501 610 488 curveto -601 483 590 478 580 474 curveto +% 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 581 471 moveto -570 471 lineto -579 477 lineto +newpath 557 268 moveto +567 264 lineto +557 262 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 581 471 moveto -570 471 lineto -579 477 lineto +newpath 557 268 moveto +567 264 lineto +557 262 lineto closepath stroke end grestore -% Uwobo +% ProofChecker gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 1295 840 moveto -1209 840 lineto -1209 804 lineto -1295 804 lineto +newpath 279 668 moveto +183 668 lineto +183 604 lineto +279 604 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 1295 840 moveto -1209 840 lineto -1209 804 lineto -1295 804 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 -1216 814 moveto -(Uwobo) -[17.28 17.28 12 12 12] +204 642 moveto +(Proof) +[13.44 7.92 12 12 7.92] +xshow +191 614 moveto +(Checker) +[16.08 12 10.56 10.56 12 10.56 7.92] xshow end grestore end grestore -% Uwobo -> acic_content -newpath 1246 804 moveto -1235 778 1214 732 1181 708 curveto -1111 655 1074 662 999 653 curveto +% ProofChecker -> cic_proof_checking +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 999 650 moveto -989 652 lineto -999 656 lineto +newpath 352 572 moveto +360 565 lineto +349 566 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 999 650 moveto -989 652 lineto -999 656 lineto +newpath 352 572 moveto +360 565 lineto +349 566 lineto closepath stroke end grestore +% Uwobo +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 626 1042 moveto +540 1042 lineto +540 1006 lineto +626 1006 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +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 +547 1016 moveto +(Uwobo) +[17.28 17.28 12 12 12] +xshow +end grestore +end grestore + % Uwobo -> content_pres -newpath 1221 804 moveto -1216 801 1210 798 1205 796 curveto -1165 778 1143 791 1113 767 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 1115 764 moveto -1105 760 lineto -1110 769 lineto +newpath 892 960 moveto +901 954 lineto +890 954 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 1115 764 moveto -1105 760 lineto -1110 769 lineto +newpath 892 960 moveto +901 954 lineto +890 954 lineto closepath stroke end grestore @@ -1435,69 +1729,45 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 668 840 moveto -588 840 lineto -588 804 lineto -668 804 lineto +newpath 764 1226 moveto +684 1226 lineto +684 1190 lineto +764 1190 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 668 840 moveto -588 840 lineto -588 804 lineto -668 804 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 -595 814 moveto +691 1200 moveto (Whelp) [22.56 12 10.56 6.72 12] xshow end grestore end grestore -% Whelp -> cic_disambiguation -newpath 660 804 moveto -666 801 671 798 677 796 curveto -718 779 764 765 803 755 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 804 758 moveto -813 752 lineto -802 752 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 804 758 moveto -813 752 lineto -802 752 lineto -closepath -stroke -end grestore - -% Whelp -> whelp -newpath 602 804 moveto -596 801 590 798 584 796 curveto -530 776 365 803 326 760 curveto -286 714 305 637 321 592 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 324 594 moveto -325 583 lineto -318 591 lineto +newpath 728 1164 moveto +724 1154 lineto +721 1164 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 324 594 moveto -325 583 lineto -318 591 lineto +newpath 728 1164 moveto +724 1154 lineto +721 1164 lineto closepath stroke end grestore