doc-src/IsarRef/document/isar-vm.svg
changeset 48958 12afbf6eb7f9
parent 29738 05d5615e12d3
equal deleted inserted replaced
48957:c04001b3a753 48958:12afbf6eb7f9
       
     1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
       
     2 <!-- Created with Inkscape (http://www.inkscape.org/) -->
       
     3 <svg
       
     4    xmlns:dc="http://purl.org/dc/elements/1.1/"
       
     5    xmlns:cc="http://creativecommons.org/ns#"
       
     6    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
       
     7    xmlns:svg="http://www.w3.org/2000/svg"
       
     8    xmlns="http://www.w3.org/2000/svg"
       
     9    xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
       
    10    xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
       
    11    width="543.02673"
       
    12    height="215.66071"
       
    13    id="svg2"
       
    14    sodipodi:version="0.32"
       
    15    inkscape:version="0.46"
       
    16    version="1.0"
       
    17    sodipodi:docname="isar-vm.svg"
       
    18    inkscape:output_extension="org.inkscape.output.svg.inkscape">
       
    19   <defs
       
    20      id="defs4">
       
    21     <marker
       
    22        inkscape:stockid="TriangleOutM"
       
    23        orient="auto"
       
    24        refY="0"
       
    25        refX="0"
       
    26        id="TriangleOutM"
       
    27        style="overflow:visible">
       
    28       <path
       
    29          id="path4130"
       
    30          d="M 5.77,0 L -2.88,5 L -2.88,-5 L 5.77,0 z"
       
    31          style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;marker-start:none"
       
    32          transform="scale(0.4,0.4)" />
       
    33     </marker>
       
    34     <marker
       
    35        inkscape:stockid="Arrow1Mend"
       
    36        orient="auto"
       
    37        refY="0"
       
    38        refX="0"
       
    39        id="Arrow1Mend"
       
    40        style="overflow:visible">
       
    41       <path
       
    42          id="path3993"
       
    43          d="M 0,0 L 5,-5 L -12.5,0 L 5,5 L 0,0 z"
       
    44          style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;marker-start:none"
       
    45          transform="matrix(-0.4,0,0,-0.4,-4,0)" />
       
    46     </marker>
       
    47     <marker
       
    48        inkscape:stockid="Arrow1Lend"
       
    49        orient="auto"
       
    50        refY="0"
       
    51        refX="0"
       
    52        id="Arrow1Lend"
       
    53        style="overflow:visible">
       
    54       <path
       
    55          id="path3207"
       
    56          d="M 0,0 L 5,-5 L -12.5,0 L 5,5 L 0,0 z"
       
    57          style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;marker-start:none"
       
    58          transform="matrix(-0.8,0,0,-0.8,-10,0)" />
       
    59     </marker>
       
    60     <marker
       
    61        inkscape:stockid="Arrow1Lstart"
       
    62        orient="auto"
       
    63        refY="0"
       
    64        refX="0"
       
    65        id="Arrow1Lstart"
       
    66        style="overflow:visible">
       
    67       <path
       
    68          id="path3204"
       
    69          d="M 0,0 L 5,-5 L -12.5,0 L 5,5 L 0,0 z"
       
    70          style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;marker-start:none"
       
    71          transform="matrix(0.8,0,0,0.8,10,0)" />
       
    72     </marker>
       
    73     <inkscape:perspective
       
    74        sodipodi:type="inkscape:persp3d"
       
    75        inkscape:vp_x="0 : 526.18109 : 1"
       
    76        inkscape:vp_y="0 : 1000 : 0"
       
    77        inkscape:vp_z="744.09448 : 526.18109 : 1"
       
    78        inkscape:persp3d-origin="372.04724 : 350.78739 : 1"
       
    79        id="perspective10" />
       
    80   </defs>
       
    81   <sodipodi:namedview
       
    82      id="base"
       
    83      pagecolor="#ffffff"
       
    84      bordercolor="#666666"
       
    85      borderopacity="1.0"
       
    86      gridtolerance="10"
       
    87      guidetolerance="10"
       
    88      objecttolerance="10"
       
    89      inkscape:pageopacity="0.0"
       
    90      inkscape:pageshadow="2"
       
    91      inkscape:zoom="1.4142136"
       
    92      inkscape:cx="305.44602"
       
    93      inkscape:cy="38.897723"
       
    94      inkscape:document-units="mm"
       
    95      inkscape:current-layer="layer1"
       
    96      showgrid="true"
       
    97      inkscape:snap-global="true"
       
    98      units="mm"
       
    99      inkscape:window-width="1226"
       
   100      inkscape:window-height="951"
       
   101      inkscape:window-x="28"
       
   102      inkscape:window-y="47">
       
   103     <inkscape:grid
       
   104        type="xygrid"
       
   105        id="grid2383"
       
   106        visible="true"
       
   107        enabled="true"
       
   108        units="mm"
       
   109        spacingx="2.5mm"
       
   110        spacingy="2.5mm"
       
   111        empspacing="2" />
       
   112   </sodipodi:namedview>
       
   113   <metadata
       
   114      id="metadata7">
       
   115     <rdf:RDF>
       
   116       <cc:Work
       
   117          rdf:about="">
       
   118         <dc:format>image/svg+xml</dc:format>
       
   119         <dc:type
       
   120            rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
       
   121       </cc:Work>
       
   122     </rdf:RDF>
       
   123   </metadata>
       
   124   <g
       
   125      inkscape:label="Layer 1"
       
   126      inkscape:groupmode="layer"
       
   127      id="layer1"
       
   128      transform="translate(-44.641342,-76.87234)">
       
   129     <g
       
   130        id="g3448"
       
   131        transform="translate(70.838012,79.725562)">
       
   132       <rect
       
   133          ry="17.67767"
       
   134          y="131.52507"
       
   135          x="212.09882"
       
   136          height="53.149605"
       
   137          width="70.866142"
       
   138          id="rect3407"
       
   139          style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.99921262;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
       
   140       <text
       
   141          sodipodi:linespacing="100%"
       
   142          id="text3409"
       
   143          y="164.06471"
       
   144          x="223.50845"
       
   145          style="font-size:18px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   146          xml:space="preserve"><tspan
       
   147            style="font-size:16px;font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans Bold"
       
   148            y="164.06471"
       
   149            x="223.50845"
       
   150            id="tspan3411"
       
   151            sodipodi:role="line">chain</tspan></text>
       
   152     </g>
       
   153     <path
       
   154        style="fill:none;fill-opacity:0.75;fill-rule:evenodd;stroke:#000000;stroke-width:0.99921262;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#TriangleOutM);stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
       
   155        d="M 424.72469,236.82544 L 356.83209,236.82544 L 356.83209,236.82544"
       
   156        id="path3458" />
       
   157     <path
       
   158        style="fill:none;fill-opacity:0.75;fill-rule:evenodd;stroke:#000000;stroke-width:0.99921268;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#TriangleOutM);stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
       
   159        d="M 282.35183,236.82544 L 215.11403,236.82544 L 215.11403,236.82544"
       
   160        id="path4771" />
       
   161     <path
       
   162        style="fill:none;fill-opacity:0.75;fill-rule:evenodd;stroke:#000000;stroke-width:0.99999994px;stroke-linecap:butt;stroke-linejoin:miter;marker-start:none;marker-mid:none;marker-end:url(#TriangleOutM);stroke-opacity:1"
       
   163        d="M 424.69726,192.5341 L 215.13005,192.5341"
       
   164        id="path4773" />
       
   165     <path
       
   166        style="fill:none;fill-opacity:0.75;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#TriangleOutM);stroke-opacity:1"
       
   167        d="M 211.98429,148.24276 L 422.13162,148.24276"
       
   168        id="path6883" />
       
   169     <g
       
   170        id="g3443"
       
   171        transform="translate(70.866146,78.725567)">
       
   172       <rect
       
   173          ry="17.67767"
       
   174          y="42.942394"
       
   175          x="70.366531"
       
   176          height="141.73228"
       
   177          width="70.866142"
       
   178          id="rect2586"
       
   179          style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.99921262;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
       
   180       <text
       
   181          sodipodi:linespacing="100%"
       
   182          id="text3370"
       
   183          y="116.62494"
       
   184          x="79.682419"
       
   185          style="font-size:18px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   186          xml:space="preserve"><tspan
       
   187            style="font-size:16px;font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans Bold"
       
   188            y="116.62494"
       
   189            x="79.682419"
       
   190            id="tspan3372"
       
   191            sodipodi:role="line">prove</tspan></text>
       
   192     </g>
       
   193     <path
       
   194        style="fill:none;fill-opacity:0.75;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#TriangleOutM);stroke-opacity:1"
       
   195        d="M 176.66575,92.035445 L 176.66575,118.61025"
       
   196        id="path7412" />
       
   197     <path
       
   198        sodipodi:type="arc"
       
   199        style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:4.30137062;stroke-linecap:round;stroke-linejoin:round;marker-end:url(#TriangleOutM);stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
       
   200        id="path9011"
       
   201        sodipodi:cx="119.58662"
       
   202        sodipodi:cy="266.74686"
       
   203        sodipodi:rx="93.01181"
       
   204        sodipodi:ry="53.149605"
       
   205        d="M 208.65508,282.05865 A 93.01181,53.149605 0 1 1 208.68579,251.49353"
       
   206        transform="matrix(0.2378166,0,0,-0.2269133,90.621413,253.06251)"
       
   207        sodipodi:start="0.29223018"
       
   208        sodipodi:end="5.9921036"
       
   209        sodipodi:open="true" />
       
   210     <g
       
   211        id="g3453"
       
   212        transform="translate(70.866151,78.725565)">
       
   213       <rect
       
   214          ry="17.67767"
       
   215          y="42.942394"
       
   216          x="353.83112"
       
   217          height="141.73228"
       
   218          width="70.866142"
       
   219          id="rect3381"
       
   220          style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.99921262;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
       
   221       <text
       
   222          sodipodi:linespacing="100%"
       
   223          id="text3383"
       
   224          y="119.31244"
       
   225          x="365.98294"
       
   226          style="font-size:18px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   227          xml:space="preserve"><tspan
       
   228            style="font-size:16px;font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans Bold"
       
   229            y="119.31244"
       
   230            x="365.98294"
       
   231            sodipodi:role="line"
       
   232            id="tspan3387">state</tspan></text>
       
   233     </g>
       
   234     <path
       
   235        style="fill:none;fill-opacity:0.75;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#TriangleOutM);stroke-opacity:1"
       
   236        d="M 460.13031,263.40024 L 460.13031,289.97505"
       
   237        id="path7941" />
       
   238     <path
       
   239        sodipodi:type="arc"
       
   240        style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:4.30137062;stroke-linecap:round;stroke-linejoin:round;marker-end:url(#TriangleOutM);stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
       
   241        id="path10594"
       
   242        sodipodi:cx="119.58662"
       
   243        sodipodi:cy="266.74686"
       
   244        sodipodi:rx="93.01181"
       
   245        sodipodi:ry="53.149605"
       
   246        d="M 208.65508,282.05865 A 93.01181,53.149605 0 1 1 208.68579,251.49353"
       
   247        transform="matrix(-0.2378166,0,0,0.2269133,546.17466,132.00569)"
       
   248        sodipodi:start="0.29223018"
       
   249        sodipodi:end="5.9921036"
       
   250        sodipodi:open="true" />
       
   251     <path
       
   252        sodipodi:type="arc"
       
   253        style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:4.30137062;stroke-linecap:round;stroke-linejoin:bevel;marker-end:url(#TriangleOutM);stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
       
   254        id="path12210"
       
   255        sodipodi:cx="119.58662"
       
   256        sodipodi:cy="266.74686"
       
   257        sodipodi:rx="93.01181"
       
   258        sodipodi:ry="53.149605"
       
   259        d="M 208.65508,282.05865 A 93.01181,53.149605 0 1 1 208.68579,251.49353"
       
   260        transform="matrix(-0.2378166,0,0,0.2269133,546.17465,87.714359)"
       
   261        sodipodi:start="0.29223018"
       
   262        sodipodi:end="5.9921036"
       
   263        sodipodi:open="true" />
       
   264     <path
       
   265        sodipodi:type="arc"
       
   266        style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:4.30137062;stroke-linecap:round;stroke-linejoin:round;marker-start:none;marker-end:url(#TriangleOutM);stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
       
   267        id="path12212"
       
   268        sodipodi:cx="119.58662"
       
   269        sodipodi:cy="266.74686"
       
   270        sodipodi:rx="93.01181"
       
   271        sodipodi:ry="53.149605"
       
   272        d="M 208.65508,282.05865 A 93.01181,53.149605 0 1 1 208.68579,251.49353"
       
   273        transform="matrix(-0.2378166,0,0,0.2269133,546.17465,176.29703)"
       
   274        sodipodi:start="0.29223018"
       
   275        sodipodi:end="5.9921036"
       
   276        sodipodi:open="true" />
       
   277     <path
       
   278        sodipodi:type="arc"
       
   279        style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:4.30137062;stroke-linecap:round;stroke-linejoin:round;marker-end:url(#TriangleOutM);stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
       
   280        id="path12214"
       
   281        sodipodi:cx="119.58662"
       
   282        sodipodi:cy="266.74686"
       
   283        sodipodi:rx="93.01181"
       
   284        sodipodi:ry="53.149605"
       
   285        d="M 208.65508,282.05865 A 93.01181,53.149605 0 1 1 208.68579,251.49353"
       
   286        transform="matrix(0,0.2378166,0.2269133,0,399.60191,71.056696)"
       
   287        sodipodi:start="0.29223018"
       
   288        sodipodi:end="5.9921036"
       
   289        sodipodi:open="true" />
       
   290     <text
       
   291        xml:space="preserve"
       
   292        style="font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   293        x="173.49998"
       
   294        y="97.094513"
       
   295        id="text19307"
       
   296        sodipodi:linespacing="100%"
       
   297        transform="translate(17.216929,6.5104864)"><tspan
       
   298          sodipodi:role="line"
       
   299          id="tspan19309"
       
   300          x="173.49998"
       
   301          y="97.094513" /></text>
       
   302     <text
       
   303        xml:space="preserve"
       
   304        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   305        x="185.52402"
       
   306        y="110.07987"
       
   307        id="text19311"
       
   308        sodipodi:linespacing="100%"><tspan
       
   309          sodipodi:role="line"
       
   310          id="tspan19313"
       
   311          x="185.52402"
       
   312          y="110.07987">theorem</tspan></text>
       
   313     <text
       
   314        xml:space="preserve"
       
   315        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   316        x="389.99997"
       
   317        y="11.594519"
       
   318        id="text19315"
       
   319        sodipodi:linespacing="100%"
       
   320        transform="translate(17.216929,6.5104864)"><tspan
       
   321          sodipodi:role="line"
       
   322          id="tspan19317"
       
   323          x="389.99997"
       
   324          y="11.594519" /></text>
       
   325     <text
       
   326        xml:space="preserve"
       
   327        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   328        x="468.98859"
       
   329        y="280.47543"
       
   330        id="text19319"
       
   331        sodipodi:linespacing="100%"><tspan
       
   332          sodipodi:role="line"
       
   333          id="tspan19321"
       
   334          x="468.98859"
       
   335          y="280.47543">qed</tspan></text>
       
   336     <text
       
   337        xml:space="preserve"
       
   338        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   339        x="549.06946"
       
   340        y="239.58423"
       
   341        id="text19323"
       
   342        sodipodi:linespacing="100%"><tspan
       
   343          sodipodi:role="line"
       
   344          id="tspan19325"
       
   345          x="549.06946"
       
   346          y="239.58423">qed</tspan></text>
       
   347     <text
       
   348        xml:space="preserve"
       
   349        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   350        x="549.39172"
       
   351        y="191.26213"
       
   352        id="text19327"
       
   353        sodipodi:linespacing="100%"><tspan
       
   354          sodipodi:role="line"
       
   355          id="tspan19329"
       
   356          x="549.39172"
       
   357          y="191.26213">fix</tspan><tspan
       
   358          sodipodi:role="line"
       
   359          x="549.39172"
       
   360          y="201.26213"
       
   361          id="tspan19331">assume</tspan></text>
       
   362     <text
       
   363        xml:space="preserve"
       
   364        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   365        x="548.71301"
       
   366        y="146.97079"
       
   367        id="text19333"
       
   368        sodipodi:linespacing="100%"><tspan
       
   369          sodipodi:role="line"
       
   370          id="tspan19335"
       
   371          x="548.71301"
       
   372          y="146.97079">{ }</tspan><tspan
       
   373          sodipodi:role="line"
       
   374          x="548.71301"
       
   375          y="156.97079"
       
   376          id="tspan19337">next</tspan></text>
       
   377     <text
       
   378        xml:space="preserve"
       
   379        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   380        x="477.84686"
       
   381        y="98.264297"
       
   382        id="text19339"
       
   383        sodipodi:linespacing="100%"><tspan
       
   384          sodipodi:role="line"
       
   385          x="477.84686"
       
   386          y="98.264297"
       
   387          id="tspan19343">note</tspan><tspan
       
   388          sodipodi:role="line"
       
   389          x="477.84686"
       
   390          y="108.2643"
       
   391          id="tspan19358">let</tspan></text>
       
   392     <text
       
   393        xml:space="preserve"
       
   394        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   395        x="43.791733"
       
   396        y="190.29289"
       
   397        id="text19345"
       
   398        sodipodi:linespacing="100%"><tspan
       
   399          sodipodi:role="line"
       
   400          id="tspan19347"
       
   401          x="43.791733"
       
   402          y="190.29289">using</tspan><tspan
       
   403          sodipodi:role="line"
       
   404          x="43.791733"
       
   405          y="200.29289"
       
   406          id="tspan19349">unfolding</tspan></text>
       
   407     <text
       
   408        xml:space="preserve"
       
   409        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   410        x="378.65891"
       
   411        y="230.52518"
       
   412        id="text19360"
       
   413        sodipodi:linespacing="100%"><tspan
       
   414          sodipodi:role="line"
       
   415          id="tspan19362"
       
   416          x="378.65891"
       
   417          y="230.52518">then</tspan></text>
       
   418     <text
       
   419        xml:space="preserve"
       
   420        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:150%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   421        x="233.98795"
       
   422        y="233.05347"
       
   423        id="text19364"
       
   424        sodipodi:linespacing="150%"><tspan
       
   425          sodipodi:role="line"
       
   426          x="233.98795"
       
   427          y="233.05347"
       
   428          id="tspan19368">have</tspan><tspan
       
   429          sodipodi:role="line"
       
   430          x="233.98795"
       
   431          y="248.05347"
       
   432          id="tspan19370">show</tspan></text>
       
   433     <text
       
   434        xml:space="preserve"
       
   435        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:150%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   436        x="305.89636"
       
   437        y="188.76213"
       
   438        id="text19374"
       
   439        sodipodi:linespacing="150%"><tspan
       
   440          sodipodi:role="line"
       
   441          x="305.89636"
       
   442          y="188.76213"
       
   443          id="tspan19376">have</tspan><tspan
       
   444          sodipodi:role="line"
       
   445          x="305.89636"
       
   446          y="203.76213"
       
   447          id="tspan19378">show</tspan></text>
       
   448     <text
       
   449        xml:space="preserve"
       
   450        style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:100%;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans;-inkscape-font-specification:Bitstream Vera Sans"
       
   451        x="303.82324"
       
   452        y="141.07895"
       
   453        id="text19380"
       
   454        sodipodi:linespacing="100%"><tspan
       
   455          sodipodi:role="line"
       
   456          id="tspan19382"
       
   457          x="303.82324"
       
   458          y="141.07895">proof</tspan></text>
       
   459   </g>
       
   460 </svg>