formal_proofs_form_the_book.svg

<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<svg version="1.2" width="241.3mm" height="40.64mm" viewBox="0 0 24130 4064" preserveAspectRatio="xMidYMid" fill-rule="evenodd" stroke-width="28.222" stroke-linejoin="round" xmlns="http://www.w3.org/2000/svg" xmlns:ooo="http://xml.openoffice.org/svg/export" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:presentation="http://sun.com/xmlns/staroffice/presentation" xmlns:smil="http://www.w3.org/2001/SMIL20/" xmlns:anim="urn:oasis:names:tc:opendocument:xmlns:animation:1.0" xml:space="preserve">
 <defs class="ClipPathGroup">
  <clipPath id="presentation_clip_path" clipPathUnits="userSpaceOnUse">
   <rect x="0" y="0" width="24130" height="4064"/>
  </clipPath>
  <clipPath id="presentation_clip_path_shrink" clipPathUnits="userSpaceOnUse">
   <rect x="24" y="4" width="24082" height="4056"/>
  </clipPath>
 </defs>
 <defs>
  <font id="EmbeddedFont_1" horiz-adv-x="2048">
   <font-face font-family="Liberation Sans embedded" units-per-em="2048" font-weight="normal" font-style="normal" ascent="1845" descent="438"/>
   <missing-glyph horiz-adv-x="2048" d="M 0,0 L 2047,0 2047,2047 0,2047 0,0 Z"/>
   <glyph unicode="s" horiz-adv-x="909" d="M 950,299 C 950,197 912,118 835,63 758,8 650,-20 511,-20 376,-20 273,2 200,47 127,91 79,160 57,254 L 216,285 C 231,227 263,185 311,158 359,131 426,117 511,117 602,117 669,131 712,159 754,187 775,229 775,285 775,328 760,362 731,389 702,416 654,438 589,455 L 460,489 C 357,516 283,542 240,568 196,593 162,624 137,661 112,698 100,743 100,796 100,895 135,970 206,1022 276,1073 378,1099 513,1099 632,1099 727,1078 798,1036 868,994 912,927 931,834 L 769,814 C 759,862 732,899 689,925 645,950 586,963 513,963 432,963 372,951 333,926 294,901 275,864 275,814 275,783 283,758 299,738 315,718 339,701 370,687 401,673 467,654 568,629 663,605 732,583 774,563 816,542 849,520 874,495 898,470 917,442 930,410 943,377 950,340 950,299 Z"/>
   <glyph unicode="r" horiz-adv-x="530" d="M 142,0 L 142,830 C 142,906 140,990 136,1082 L 306,1082 C 311,959 314,886 314,861 L 318,861 C 347,954 380,1017 417,1051 454,1085 507,1102 575,1102 599,1102 623,1099 648,1092 L 648,927 C 624,934 592,937 552,937 477,937 420,905 381,841 342,776 322,684 322,564 L 322,0 142,0 Z"/>
   <glyph unicode="o" horiz-adv-x="983" d="M 1053,542 C 1053,353 1011,212 928,119 845,26 724,-20 565,-20 407,-20 288,28 207,125 126,221 86,360 86,542 86,915 248,1102 571,1102 736,1102 858,1057 936,966 1014,875 1053,733 1053,542 Z M 864,542 C 864,691 842,800 798,868 753,935 679,969 574,969 469,969 393,935 346,866 299,797 275,689 275,542 275,399 298,292 345,221 391,149 464,113 563,113 671,113 748,148 795,217 841,286 864,395 864,542 Z"/>
   <glyph unicode="m" horiz-adv-x="1452" d="M 768,0 L 768,686 C 768,791 754,863 725,903 696,943 645,963 570,963 493,963 433,934 388,875 343,816 321,734 321,627 L 321,0 142,0 142,851 C 142,977 140,1054 136,1082 L 306,1082 C 307,1079 307,1070 308,1055 309,1040 310,1024 311,1005 312,986 313,950 314,897 L 317,897 C 356,974 400,1027 450,1057 500,1087 561,1102 633,1102 715,1102 780,1086 828,1053 875,1020 908,968 927,897 L 930,897 C 967,970 1013,1022 1066,1054 1119,1086 1183,1102 1258,1102 1367,1102 1447,1072 1497,1013 1546,954 1571,856 1571,721 L 1571,0 1393,0 1393,686 C 1393,791 1379,863 1350,903 1321,943 1270,963 1195,963 1116,963 1055,934 1012,876 968,817 946,734 946,627 L 946,0 768,0 Z"/>
   <glyph unicode="f" horiz-adv-x="561" d="M 361,951 L 361,0 181,0 181,951 29,951 29,1082 181,1082 181,1204 C 181,1303 203,1374 246,1417 289,1460 356,1482 445,1482 495,1482 537,1478 572,1470 L 572,1333 C 542,1338 515,1341 492,1341 446,1341 413,1329 392,1306 371,1283 361,1240 361,1179 L 361,1082 572,1082 572,951 361,951 Z"/>
   <glyph unicode="T" horiz-adv-x="1166" d="M 720,1253 L 720,0 530,0 530,1253 46,1253 46,1409 1204,1409 1204,1253 720,1253 Z"/>
   <glyph unicode="P" horiz-adv-x="1090" d="M 1258,985 C 1258,852 1215,746 1128,667 1041,588 922,549 773,549 L 359,549 359,0 168,0 168,1409 761,1409 C 919,1409 1041,1372 1128,1298 1215,1224 1258,1120 1258,985 Z M 1066,983 C 1066,1165 957,1256 738,1256 L 359,1256 359,700 746,700 C 959,700 1066,794 1066,983 Z"/>
   <glyph unicode="O" horiz-adv-x="1407" d="M 1495,711 C 1495,564 1467,435 1411,324 1354,213 1273,128 1168,69 1063,10 938,-20 795,-20 650,-20 526,9 421,68 316,127 235,212 180,323 125,434 97,563 97,711 97,936 159,1113 282,1240 405,1367 577,1430 797,1430 940,1430 1065,1402 1170,1345 1275,1288 1356,1205 1412,1096 1467,987 1495,859 1495,711 Z M 1300,711 C 1300,886 1256,1024 1169,1124 1081,1224 957,1274 797,1274 636,1274 511,1225 423,1126 335,1027 291,889 291,711 291,534 336,394 425,291 514,187 637,135 795,135 958,135 1083,185 1170,286 1257,386 1300,528 1300,711 Z"/>
   <glyph unicode="K" horiz-adv-x="1181" d="M 1106,0 L 543,680 359,540 359,0 168,0 168,1409 359,1409 359,703 1038,1409 1263,1409 663,797 1343,0 1106,0 Z"/>
   <glyph unicode="H" horiz-adv-x="1150" d="M 1121,0 L 1121,653 359,653 359,0 168,0 168,1409 359,1409 359,813 1121,813 1121,1409 1312,1409 1312,0 1121,0 Z"/>
   <glyph unicode="E" horiz-adv-x="1120" d="M 168,0 L 168,1409 1237,1409 1237,1253 359,1253 359,801 1177,801 1177,647 359,647 359,156 1278,156 1278,0 168,0 Z"/>
   <glyph unicode="B" horiz-adv-x="1090" d="M 1258,397 C 1258,272 1212,174 1121,105 1030,35 903,0 740,0 L 168,0 168,1409 680,1409 C 1011,1409 1176,1295 1176,1067 1176,984 1153,914 1106,857 1059,800 993,762 908,743 1020,730 1106,692 1167,631 1228,569 1258,491 1258,397 Z M 984,1044 C 984,1120 958,1174 906,1207 854,1240 779,1256 680,1256 L 359,1256 359,810 680,810 C 782,810 858,829 909,868 959,906 984,965 984,1044 Z M 1065,412 C 1065,578 948,661 715,661 L 359,661 359,153 730,153 C 847,153 932,175 985,218 1038,261 1065,326 1065,412 Z"/>
   <glyph unicode=" " horiz-adv-x="575"/>
  </font>
 </defs>
 <defs>
  <font id="EmbeddedFont_2" horiz-adv-x="2048">
   <font-face font-family="Liberation Sans embedded" units-per-em="2048" font-weight="normal" font-style="italic" ascent="1845" descent="438"/>
   <missing-glyph horiz-adv-x="2048" d="M 0,0 L 2047,0 2047,2047 0,2047 0,0 Z"/>
   <glyph unicode="r" horiz-adv-x="727" d="M 718,938 C 689,947 659,951 628,951 558,951 495,914 439,841 382,768 344,675 324,564 L 214,0 34,0 196,830 221,968 239,1082 409,1082 374,861 378,861 C 422,950 465,1012 508,1048 551,1084 600,1102 656,1102 687,1102 718,1097 751,1088 L 718,938 Z"/>
   <glyph unicode="o" horiz-adv-x="1014" d="M 1074,683 C 1074,596 1061,506 1034,413 1007,319 969,240 920,175 870,110 809,61 737,29 665,-4 583,-20 491,-20 360,-20 257,19 181,98 105,177 67,284 67,419 70,555 94,676 141,781 188,886 252,966 335,1020 418,1074 520,1101 642,1101 782,1101 889,1065 963,992 1037,919 1074,816 1074,683 Z M 888,683 C 888,874 805,969 640,969 550,969 478,946 424,900 369,853 327,783 297,689 267,595 252,504 252,416 252,317 273,242 316,191 359,139 421,113 502,113 571,113 626,125 668,148 709,171 746,207 777,256 808,305 834,367 854,443 873,519 885,599 888,683 Z"/>
   <glyph unicode="m" horiz-adv-x="1589" d="M 660,0 L 784,634 C 801,717 809,775 809,808 809,858 796,896 771,923 746,949 704,962 647,962 570,962 502,929 445,863 387,797 349,711 331,604 L 213,0 34,0 200,851 C 213,914 226,991 239,1082 L 409,1082 C 409,1075 406,1049 399,1005 392,960 386,924 381,897 L 384,897 C 433,973 482,1026 531,1056 580,1086 638,1101 706,1101 787,1101 851,1081 898,1042 945,1002 974,944 983,869 1038,956 1093,1016 1147,1050 1200,1084 1262,1101 1331,1101 1421,1101 1490,1077 1539,1028 1587,979 1611,909 1611,817 1611,774 1604,720 1590,653 L 1463,0 1285,0 1409,634 C 1426,717 1434,775 1434,808 1434,858 1421,896 1396,923 1371,949 1329,962 1272,962 1195,962 1127,930 1070,865 1013,800 975,714 956,607 L 838,0 660,0 Z"/>
   <glyph unicode="l" horiz-adv-x="485" d="M 33,0 L 321,1484 501,1484 212,0 33,0 Z"/>
   <glyph unicode="a" horiz-adv-x="1029" d="M 927,-10 C 865,-10 820,3 792,29 763,54 749,92 749,143 L 754,207 748,207 C 693,123 635,64 576,31 517,-3 445,-20 361,-20 268,-20 192,8 134,64 75,120 46,191 46,278 46,401 90,495 179,558 267,621 408,654 601,657 L 833,660 C 846,725 852,768 852,787 852,848 834,893 799,922 764,951 715,965 652,965 573,965 513,951 472,923 431,894 402,851 384,793 L 206,822 C 236,920 288,991 363,1036 437,1080 537,1102 662,1102 776,1102 866,1075 933,1022 999,969 1032,897 1032,807 1032,764 1026,712 1013,650 L 939,272 C 932,240 928,211 928,184 928,135 955,111 1009,111 1027,111 1047,113 1069,118 L 1055,6 C 1011,-5 968,-10 927,-10 Z M 809,536 L 610,532 C 531,530 468,523 423,511 378,498 343,483 318,464 293,445 273,421 259,392 244,363 237,327 237,286 237,236 253,195 286,164 318,133 360,117 411,117 476,117 534,131 586,159 638,186 681,222 715,267 749,312 771,360 782,411 L 809,536 Z"/>
   <glyph unicode="F" horiz-adv-x="1287" d="M 497,1253 L 395,729 1191,729 1160,571 364,571 254,0 63,0 336,1409 1347,1409 1317,1253 497,1253 Z"/>
  </font>
 </defs>
 <defs class="TextShapeIndex">
  <g ooo:slide="id1" ooo:id-list="id3"/>
 </defs>
 <defs class="EmbeddedBulletChars">
  <g id="bullet-char-template-57356" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 580,1141 L 1163,571 580,0 -4,571 580,1141 Z"/>
  </g>
  <g id="bullet-char-template-57354" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 8,1128 L 1137,1128 1137,0 8,0 8,1128 Z"/>
  </g>
  <g id="bullet-char-template-10146" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 174,0 L 602,739 174,1481 1456,739 174,0 Z M 1358,739 L 309,1346 659,739 1358,739 Z"/>
  </g>
  <g id="bullet-char-template-10132" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 2015,739 L 1276,0 717,0 1260,543 174,543 174,936 1260,936 717,1481 1274,1481 2015,739 Z"/>
  </g>
  <g id="bullet-char-template-10007" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 0,-2 C -7,14 -16,27 -25,37 L 356,567 C 262,823 215,952 215,954 215,979 228,992 255,992 264,992 276,990 289,987 310,991 331,999 354,1012 L 381,999 492,748 772,1049 836,1024 860,1049 C 881,1039 901,1025 922,1006 886,937 835,863 770,784 769,783 710,716 594,584 L 774,223 C 774,196 753,168 711,139 L 727,119 C 717,90 699,76 672,76 641,76 570,178 457,381 L 164,-76 C 142,-110 111,-127 72,-127 30,-127 9,-110 8,-76 1,-67 -2,-52 -2,-32 -2,-23 -1,-13 0,-2 Z"/>
  </g>
  <g id="bullet-char-template-10004" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 285,-33 C 182,-33 111,30 74,156 52,228 41,333 41,471 41,549 55,616 82,672 116,743 169,778 240,778 293,778 328,747 346,684 L 369,508 C 377,444 397,411 428,410 L 1163,1116 C 1174,1127 1196,1133 1229,1133 1271,1133 1292,1118 1292,1087 L 1292,965 C 1292,929 1282,901 1262,881 L 442,47 C 390,-6 338,-33 285,-33 Z"/>
  </g>
  <g id="bullet-char-template-9679" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 813,0 C 632,0 489,54 383,161 276,268 223,411 223,592 223,773 276,916 383,1023 489,1130 632,1184 813,1184 992,1184 1136,1130 1245,1023 1353,916 1407,772 1407,592 1407,412 1353,268 1245,161 1136,54 992,0 813,0 Z"/>
  </g>
  <g id="bullet-char-template-8226" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 346,457 C 273,457 209,483 155,535 101,586 74,649 74,723 74,796 101,859 155,911 209,963 273,989 346,989 419,989 480,963 531,910 582,859 608,796 608,723 608,648 583,586 532,535 482,483 420,457 346,457 Z"/>
  </g>
  <g id="bullet-char-template-8211" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M -4,459 L 1135,459 1135,606 -4,606 -4,459 Z"/>
  </g>
  <g id="bullet-char-template-61548" transform="scale(0.00048828125,-0.00048828125)">
   <path d="M 173,740 C 173,903 231,1043 346,1159 462,1274 601,1332 765,1332 928,1332 1067,1274 1183,1159 1299,1043 1357,903 1357,740 1357,577 1299,437 1183,322 1067,206 928,148 765,148 601,148 462,206 346,322 231,437 173,577 173,740 Z"/>
  </g>
 </defs>
 <g>
  <g id="id2" class="Master_Slide">
   <g id="bg-id2" class="Background"/>
   <g id="bo-id2" class="BackgroundObjects"/>
  </g>
 </g>
 <g class="SlideGroup">
  <g>
   <g id="container-id1">
    <g id="id1" class="Slide" clip-path="url(#presentation_clip_path)">
     <g class="Page">
      <defs class="SlideBackground">
       <g id="bg-id1" class="Background">
        <path fill="rgb(156,22,10)" stroke="none" d="M 12057,4055 L -8,4055 -8,-8 24121,-8 24121,4055 12057,4055 Z"/>
       </g>
      </defs>
      <g class="TextShape">
       <g id="id3">
        <rect class="BoundingBox" stroke="none" fill="rgb(156,22,10)" x="635" y="952" width="22707" height="2022"/>
        <text class="SVGTextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="1588px" font-style="italic" font-weight="400"><tspan class="TextPosition" x="885" y="2512"><tspan fill="rgb(255,245,129)" stroke="none" style="white-space: pre">Formal</tspan><tspan font-style="normal" fill="rgb(255,245,129)" stroke="none" style="white-space: pre"> Proofs from THE BOOK</tspan></tspan></tspan></text>
       </g>
      </g>
     </g>
    </g>
   </g>
  </g>
 </g>
</svg>