828 lines
43 KiB
XML
828 lines
43 KiB
XML
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
|
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
|
|
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
|
|
<!-- Generated by graphviz version 2.42.4 (0)
|
|
-->
|
|
<!-- Title: deps Pages: 1 -->
|
|
<svg width="1445pt" height="1800pt"
|
|
viewBox="0.00 0.00 1444.74 1800.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
|
|
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 1796)">
|
|
<title>deps</title>
|
|
<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-1796 1440.74,-1796 1440.74,4 -4,4"/>
|
|
<text text-anchor="start" x="588.87" y="-1779.4" font-family="Inter" font-weight="bold" font-size="12.00" fill="#000000">Theorem dependencies M2, 53 results</text>
|
|
<!-- close_rec_notin -->
|
|
<g id="node1" class="node">
|
|
<title>close_rec_notin</title>
|
|
<g id="a_node1"><a xlink:title="close_rec_notin theory/Binding.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M119.5,-321C119.5,-321 27.5,-321 27.5,-321 21.5,-321 15.5,-315 15.5,-309 15.5,-309 15.5,-297 15.5,-297 15.5,-291 21.5,-285 27.5,-285 27.5,-285 119.5,-285 119.5,-285 125.5,-285 131.5,-291 131.5,-297 131.5,-297 131.5,-309 131.5,-309 131.5,-315 125.5,-321 119.5,-321"/>
|
|
<text text-anchor="middle" x="73.5" y="-300.8" font-family="Inter" font-size="9.00" fill="#000000">close_rec_notin\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- subst_notin -->
|
|
<g id="node58" class="node">
|
|
<title>subst_notin</title>
|
|
<g id="a_node58"><a xlink:title="subst_notin theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-303" rx="39.67" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-300.8" font-family="Inter" font-size="9.00" fill="#000000">subst_notin</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- close_rec_notin->subst_notin -->
|
|
<g id="edge32" class="edge">
|
|
<title>close_rec_notin->subst_notin</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M131.59,-303C164.68,-303 205.74,-303 236.51,-303"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="236.52,-305.1 242.52,-303 236.52,-300.9 236.52,-305.1"/>
|
|
</g>
|
|
<!-- fvs_lift -->
|
|
<g id="node2" class="node">
|
|
<title>fvs_lift</title>
|
|
<g id="a_node2"><a xlink:title="fvs_lift theory/Binding.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M99,-371C99,-371 48,-371 48,-371 42,-371 36,-365 36,-359 36,-359 36,-347 36,-347 36,-341 42,-335 48,-335 48,-335 99,-335 99,-335 105,-335 111,-341 111,-347 111,-347 111,-359 111,-359 111,-365 105,-371 99,-371"/>
|
|
<text text-anchor="middle" x="73.5" y="-350.8" font-family="Inter" font-size="9.00" fill="#000000">fvs_lift\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- fvs_zplug_lift -->
|
|
<g id="node26" class="node">
|
|
<title>fvs_zplug_lift</title>
|
|
<g id="a_node26"><a xlink:title="fvs_zplug_lift theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-353" rx="42.95" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-350.8" font-family="Inter" font-size="9.00" fill="#000000">fvs_zplug_lift</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- fvs_lift->fvs_zplug_lift -->
|
|
<g id="edge18" class="edge">
|
|
<title>fvs_lift->fvs_zplug_lift</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M111.02,-353C145.02,-353 195.93,-353 233.25,-353"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="233.59,-355.1 239.59,-353 233.59,-350.9 233.59,-355.1"/>
|
|
</g>
|
|
<!-- has_red_spec -->
|
|
<g id="node3" class="node">
|
|
<title>has_red_spec</title>
|
|
<g id="a_node3"><a xlink:title="has_red_spec theory/Reduction.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M884.03,-271C884.03,-271 801.03,-271 801.03,-271 795.03,-271 789.03,-265 789.03,-259 789.03,-259 789.03,-247 789.03,-247 789.03,-241 795.03,-235 801.03,-235 801.03,-235 884.03,-235 884.03,-235 890.03,-235 896.03,-241 896.03,-247 896.03,-247 896.03,-259 896.03,-259 896.03,-265 890.03,-271 884.03,-271"/>
|
|
<text text-anchor="middle" x="842.53" y="-250.8" font-family="Inter" font-size="9.00" fill="#000000">has_red_spec\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- check_term_true -->
|
|
<g id="node41" class="node">
|
|
<title>check_term_true</title>
|
|
<g id="a_node41"><a xlink:title="check_term_true theory/Random.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="1036.54" cy="-278" rx="53.89" ry="18"/>
|
|
<text text-anchor="middle" x="1036.54" y="-275.8" font-family="Inter" font-size="9.00" fill="#000000">check_term_true</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- has_red_spec->check_term_true -->
|
|
<g id="edge25" class="edge">
|
|
<title>has_red_spec->check_term_true</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M896.26,-259.86C922.26,-263.25 953.62,-267.33 980,-270.77"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="980.02,-272.89 986.24,-271.58 980.56,-268.72 980.02,-272.89"/>
|
|
</g>
|
|
<!-- corpus_decides -->
|
|
<g id="node61" class="node">
|
|
<title>corpus_decides</title>
|
|
<g id="a_node61"><a xlink:title="corpus_decides theory/Tests.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="1036.54" cy="-228" rx="49.8" ry="18"/>
|
|
<text text-anchor="middle" x="1036.54" y="-225.8" font-family="Inter" font-size="9.00" fill="#000000">corpus_decides</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- has_red_spec->corpus_decides -->
|
|
<g id="edge39" class="edge">
|
|
<title>has_red_spec->corpus_decides</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M896.26,-246.14C923.4,-242.6 956.38,-238.31 983.44,-234.78"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="983.79,-236.86 989.47,-234 983.25,-232.69 983.79,-236.86"/>
|
|
</g>
|
|
<!-- open_rec_occurs_false -->
|
|
<g id="node4" class="node">
|
|
<title>open_rec_occurs_false</title>
|
|
<g id="a_node4"><a xlink:title="open_rec_occurs_false theory/Binding.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M135,-271C135,-271 12,-271 12,-271 6,-271 0,-265 0,-259 0,-259 0,-247 0,-247 0,-241 6,-235 12,-235 12,-235 135,-235 135,-235 141,-235 147,-241 147,-247 147,-247 147,-259 147,-259 147,-265 141,-271 135,-271"/>
|
|
<text text-anchor="middle" x="73.5" y="-250.8" font-family="Inter" font-size="9.00" fill="#000000">open_rec_occurs_false\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- full_comp_aux -->
|
|
<g id="node25" class="node">
|
|
<title>full_comp_aux</title>
|
|
<g id="a_node25"><a xlink:title="full_comp_aux theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="474.45" cy="-143" rx="46.53" ry="18"/>
|
|
<text text-anchor="middle" x="474.45" y="-140.8" font-family="Inter" font-size="9.00" fill="#000000">full_comp_aux</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_occurs_false->full_comp_aux -->
|
|
<g id="edge13" class="edge">
|
|
<title>open_rec_occurs_false->full_comp_aux</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M147.28,-250.39C229.76,-247.42 352.87,-243 352.87,-243 352.87,-243 413.53,-192.7 448.8,-163.44"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="450.53,-164.74 453.81,-159.29 447.85,-161.5 450.53,-164.74"/>
|
|
</g>
|
|
<!-- open_rec_zplug_lift -->
|
|
<g id="node35" class="node">
|
|
<title>open_rec_zplug_lift</title>
|
|
<g id="a_node35"><a xlink:title="open_rec_zplug_lift theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-218" rx="59.43" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-215.8" font-family="Inter" font-size="9.00" fill="#000000">open_rec_zplug_lift</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_occurs_false->open_rec_zplug_lift -->
|
|
<g id="edge10" class="edge">
|
|
<title>open_rec_occurs_false->open_rec_zplug_lift</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M147.17,-240.71C172.4,-236.44 200.31,-231.72 224.13,-227.69"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="224.53,-229.76 230.09,-226.68 223.82,-225.61 224.53,-229.76"/>
|
|
</g>
|
|
<!-- open_rec_occurs_false->subst_notin -->
|
|
<g id="edge33" class="edge">
|
|
<title>open_rec_occurs_false->subst_notin</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M147.17,-270.56C178.67,-278.17 214.37,-286.8 241.04,-293.24"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="240.6,-295.29 246.93,-294.66 241.59,-291.21 240.6,-295.29"/>
|
|
</g>
|
|
<!-- steps_complete -->
|
|
<g id="node5" class="node">
|
|
<title>steps_complete</title>
|
|
<g id="a_node5"><a xlink:title="steps_complete theory/Reduction.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M120,-471C120,-471 27,-471 27,-471 21,-471 15,-465 15,-459 15,-459 15,-447 15,-447 15,-441 21,-435 27,-435 27,-435 120,-435 120,-435 126,-435 132,-441 132,-447 132,-447 132,-459 132,-459 132,-465 126,-471 120,-471"/>
|
|
<text text-anchor="middle" x="73.5" y="-450.8" font-family="Inter" font-size="9.00" fill="#000000">steps_complete\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- enumerate_complete -->
|
|
<g id="node17" class="node">
|
|
<title>enumerate_complete</title>
|
|
<g id="a_node17"><a xlink:title="enumerate_complete theory/Enumerate.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-503" rx="65.48" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-500.8" font-family="Inter" font-size="9.00" fill="#000000">enumerate_complete</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_complete->enumerate_complete -->
|
|
<g id="edge5" class="edge">
|
|
<title>steps_complete->enumerate_complete</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M132.14,-466.93C161.73,-474.08 197.58,-482.74 226.74,-489.78"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="226.53,-491.89 232.85,-491.26 227.51,-487.81 226.53,-491.89"/>
|
|
</g>
|
|
<!-- gen_complete -->
|
|
<g id="node42" class="node">
|
|
<title>gen_complete</title>
|
|
<g id="a_node42"><a xlink:title="gen_complete theory/Random.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-453" rx="46.38" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-450.8" font-family="Inter" font-size="9.00" fill="#000000">gen_complete</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_complete->gen_complete -->
|
|
<g id="edge29" class="edge">
|
|
<title>steps_complete->gen_complete</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M132.14,-453C162.85,-453 200.3,-453 230.01,-453"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="230.23,-455.1 236.23,-453 230.23,-450.9 230.23,-455.1"/>
|
|
</g>
|
|
<!-- corpus_complete -->
|
|
<g id="node60" class="node">
|
|
<title>corpus_complete</title>
|
|
<g id="a_node60"><a xlink:title="corpus_complete theory/Tests.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-403" rx="54.04" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-400.8" font-family="Inter" font-size="9.00" fill="#000000">corpus_complete</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_complete->corpus_complete -->
|
|
<g id="edge38" class="edge">
|
|
<title>steps_complete->corpus_complete</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M132.14,-439.07C163.65,-431.46 202.26,-422.13 232.32,-414.87"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="232.87,-416.89 238.21,-413.44 231.89,-412.81 232.87,-416.89"/>
|
|
</g>
|
|
<!-- steps_sound -->
|
|
<g id="node6" class="node">
|
|
<title>steps_sound</title>
|
|
<g id="a_node6"><a xlink:title="steps_sound theory/Reduction.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M113,-621C113,-621 34,-621 34,-621 28,-621 22,-615 22,-609 22,-609 22,-597 22,-597 22,-591 28,-585 34,-585 34,-585 113,-585 113,-585 119,-585 125,-591 125,-597 125,-597 125,-609 125,-609 125,-615 119,-621 113,-621"/>
|
|
<text text-anchor="middle" x="73.5" y="-600.8" font-family="Inter" font-size="9.00" fill="#000000">steps_sound\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- enumerate_sound -->
|
|
<g id="node18" class="node">
|
|
<title>enumerate_sound</title>
|
|
<g id="a_node18"><a xlink:title="enumerate_sound theory/Enumerate.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-653" rx="56.66" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-650.8" font-family="Inter" font-size="9.00" fill="#000000">enumerate_sound</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_sound->enumerate_sound -->
|
|
<g id="edge4" class="edge">
|
|
<title>steps_sound->enumerate_sound</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M125.12,-615.23C157.34,-623.02 198.9,-633.06 231.07,-640.83"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="230.63,-642.89 236.96,-642.25 231.62,-638.8 230.63,-642.89"/>
|
|
</g>
|
|
<!-- gen_sound -->
|
|
<g id="node45" class="node">
|
|
<title>gen_sound</title>
|
|
<g id="a_node45"><a xlink:title="gen_sound theory/Random.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-603" rx="38.21" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-600.8" font-family="Inter" font-size="9.00" fill="#000000">gen_sound</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_sound->gen_sound -->
|
|
<g id="edge28" class="edge">
|
|
<title>steps_sound->gen_sound</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M125.12,-603C159.82,-603 205.35,-603 238.31,-603"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="238.32,-605.1 244.32,-603 238.32,-600.9 238.32,-605.1"/>
|
|
</g>
|
|
<!-- corpus_sound -->
|
|
<g id="node63" class="node">
|
|
<title>corpus_sound</title>
|
|
<g id="a_node63"><a xlink:title="corpus_sound theory/Tests.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-553" rx="46.38" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-550.8" font-family="Inter" font-size="9.00" fill="#000000">corpus_sound</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_sound->corpus_sound -->
|
|
<g id="edge37" class="edge">
|
|
<title>steps_sound->corpus_sound</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M125.12,-590.77C159.25,-582.52 203.87,-571.74 236.7,-563.81"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="237.35,-565.81 242.69,-562.36 236.36,-561.73 237.35,-565.81"/>
|
|
</g>
|
|
<!-- steps_sound_red1 -->
|
|
<g id="node7" class="node">
|
|
<title>steps_sound_red1</title>
|
|
<g id="a_node7"><a xlink:title="steps_sound_red1 theory/Reduction.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M894.53,-346C894.53,-346 790.53,-346 790.53,-346 784.53,-346 778.53,-340 778.53,-334 778.53,-334 778.53,-322 778.53,-322 778.53,-316 784.53,-310 790.53,-310 790.53,-310 894.53,-310 894.53,-310 900.53,-310 906.53,-316 906.53,-322 906.53,-322 906.53,-334 906.53,-334 906.53,-340 900.53,-346 894.53,-346"/>
|
|
<text text-anchor="middle" x="842.53" y="-325.8" font-family="Inter" font-size="9.00" fill="#000000">steps_sound_red1\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_sound_red1->check_term_true -->
|
|
<g id="edge26" class="edge">
|
|
<title>steps_sound_red1->check_term_true</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M906.67,-311.56C932.97,-304.71 963.01,-296.89 987.47,-290.52"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="988.29,-292.48 993.56,-288.93 987.23,-288.41 988.29,-292.48"/>
|
|
</g>
|
|
<!-- gen_fv_preserved -->
|
|
<g id="node43" class="node">
|
|
<title>gen_fv_preserved</title>
|
|
<g id="a_node43"><a xlink:title="gen_fv_preserved theory/Random.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="1036.54" cy="-378" rx="55.35" ry="18"/>
|
|
<text text-anchor="middle" x="1036.54" y="-375.8" font-family="Inter" font-size="9.00" fill="#000000">gen_fv_preserved</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_sound_red1->gen_fv_preserved -->
|
|
<g id="edge31" class="edge">
|
|
<title>steps_sound_red1->gen_fv_preserved</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M906.67,-344.44C932.67,-351.21 962.32,-358.93 986.62,-365.26"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="986.35,-367.36 992.68,-366.84 987.41,-363.29 986.35,-367.36"/>
|
|
</g>
|
|
<!-- corpus_fv_preserved -->
|
|
<g id="node62" class="node">
|
|
<title>corpus_fv_preserved</title>
|
|
<g id="a_node62"><a xlink:title="corpus_fv_preserved theory/Tests.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="1036.54" cy="-328" rx="63.52" ry="18"/>
|
|
<text text-anchor="middle" x="1036.54" y="-325.8" font-family="Inter" font-size="9.00" fill="#000000">corpus_fv_preserved</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- steps_sound_red1->corpus_fv_preserved -->
|
|
<g id="edge41" class="edge">
|
|
<title>steps_sound_red1->corpus_fv_preserved</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M906.67,-328C925.99,-328 947.32,-328 966.98,-328"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="967.02,-330.1 973.02,-328 967.02,-325.9 967.02,-330.1"/>
|
|
</g>
|
|
<!-- subst_fvar_other -->
|
|
<g id="node8" class="node">
|
|
<title>subst_fvar_other</title>
|
|
<g id="a_node8"><a xlink:title="subst_fvar_other theory/Binding.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M122.5,-721C122.5,-721 24.5,-721 24.5,-721 18.5,-721 12.5,-715 12.5,-709 12.5,-709 12.5,-697 12.5,-697 12.5,-691 18.5,-685 24.5,-685 24.5,-685 122.5,-685 122.5,-685 128.5,-685 134.5,-691 134.5,-697 134.5,-697 134.5,-709 134.5,-709 134.5,-715 128.5,-721 122.5,-721"/>
|
|
<text text-anchor="middle" x="73.5" y="-700.8" font-family="Inter" font-size="9.00" fill="#000000">subst_fvar_other\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- subst_other -->
|
|
<g id="node59" class="node">
|
|
<title>subst_other</title>
|
|
<g id="a_node59"><a xlink:title="subst_other theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-703" rx="40.33" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-700.8" font-family="Inter" font-size="9.00" fill="#000000">subst_other</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- subst_fvar_other->subst_other -->
|
|
<g id="edge35" class="edge">
|
|
<title>subst_fvar_other->subst_other</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M134.63,-703C166.83,-703 205.86,-703 235.58,-703"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="235.78,-705.1 241.78,-703 235.78,-700.9 235.78,-705.1"/>
|
|
</g>
|
|
<!-- subst_fvar_self -->
|
|
<g id="node9" class="node">
|
|
<title>subst_fvar_self</title>
|
|
<g id="a_node9"><a xlink:title="subst_fvar_self theory/Binding.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M118,-771C118,-771 29,-771 29,-771 23,-771 17,-765 17,-759 17,-759 17,-747 17,-747 17,-741 23,-735 29,-735 29,-735 118,-735 118,-735 124,-735 130,-741 130,-747 130,-747 130,-759 130,-759 130,-765 124,-771 118,-771"/>
|
|
<text text-anchor="middle" x="73.5" y="-750.8" font-family="Inter" font-size="9.00" fill="#000000">subst_fvar_self\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- subst_lc_self -->
|
|
<g id="node57" class="node">
|
|
<title>subst_lc_self</title>
|
|
<g id="a_node57"><a xlink:title="subst_lc_self theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-753" rx="42.29" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-750.8" font-family="Inter" font-size="9.00" fill="#000000">subst_lc_self</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- subst_fvar_self->subst_lc_self -->
|
|
<g id="edge34" class="edge">
|
|
<title>subst_fvar_self->subst_lc_self</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M130.23,-753C162.66,-753 203.11,-753 234.01,-753"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="234.06,-755.1 240.06,-753 234.06,-750.9 234.06,-755.1"/>
|
|
</g>
|
|
<!-- zdecs_sound -->
|
|
<g id="node10" class="node">
|
|
<title>zdecs_sound</title>
|
|
<g id="a_node10"><a xlink:title="zdecs_sound theory/Reduction.v proved">
|
|
<path fill="#ffffff" stroke="#000000" stroke-width="0.9" stroke-dasharray="5,2" d="M322.44,-186C322.44,-186 242.44,-186 242.44,-186 236.44,-186 230.44,-180 230.44,-174 230.44,-174 230.44,-162 230.44,-162 230.44,-156 236.44,-150 242.44,-150 242.44,-150 322.44,-150 322.44,-150 328.44,-150 334.44,-156 334.44,-162 334.44,-162 334.44,-174 334.44,-174 334.44,-180 328.44,-186 322.44,-186"/>
|
|
<text text-anchor="middle" x="282.44" y="-165.8" font-family="Inter" font-size="9.00" fill="#000000">zdecs_sound\n(M1)</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- zdecs_sound->full_comp_aux -->
|
|
<g id="edge16" class="edge">
|
|
<title>zdecs_sound->full_comp_aux</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M334.61,-161.27C362.3,-157.62 396.36,-153.14 423.82,-149.53"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="424.25,-151.59 429.93,-148.73 423.7,-147.43 424.25,-151.59"/>
|
|
</g>
|
|
<!-- Plus_to_Star -->
|
|
<g id="node11" class="node">
|
|
<title>Plus_to_Star</title>
|
|
<g id="a_node11"><a xlink:title="Plus_to_Star theory/Closure.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-803" rx="40.98" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-800.8" font-family="Inter" font-size="9.00" fill="#000000">Plus_to_Star</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- Star_red1_context -->
|
|
<g id="node12" class="node">
|
|
<title>Star_red1_context</title>
|
|
<g id="a_node12"><a xlink:title="Star_red1_context theory/Closure.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-853" rx="57.97" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-850.8" font-family="Inter" font-size="9.00" fill="#000000">Star_red1_context</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- Star_trans -->
|
|
<g id="node13" class="node">
|
|
<title>Star_trans</title>
|
|
<g id="a_node13"><a xlink:title="Star_trans theory/Closure.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-903" rx="36.25" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-900.8" font-family="Inter" font-size="9.00" fill="#000000">Star_trans</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- red1_star -->
|
|
<g id="node14" class="node">
|
|
<title>red1_star</title>
|
|
<g id="a_node14"><a xlink:title="red1_star theory/Closure.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-953" rx="34.13" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-950.8" font-family="Inter" font-size="9.00" fill="#000000">red1_star</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- star_one_trans -->
|
|
<g id="node15" class="node">
|
|
<title>star_one_trans</title>
|
|
<g id="a_node15"><a xlink:title="star_one_trans theory/Closure.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1003" rx="47.84" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1000.8" font-family="Inter" font-size="9.00" fill="#000000">star_one_trans</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- enumerate_check -->
|
|
<g id="node16" class="node">
|
|
<title>enumerate_check</title>
|
|
<g id="a_node16"><a xlink:title="enumerate_check theory/Enumerate.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="1380.16" cy="-278" rx="56.66" ry="18"/>
|
|
<text text-anchor="middle" x="1380.16" y="-275.8" font-family="Inter" font-size="9.00" fill="#000000">enumerate_check</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- in_comb -->
|
|
<g id="node19" class="node">
|
|
<title>in_comb</title>
|
|
<g id="a_node19"><a xlink:title="in_comb theory/Enumerate.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1103" rx="31.51" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1100.8" font-family="Inter" font-size="9.00" fill="#000000">in_comb</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- size_all_terms -->
|
|
<g id="node21" class="node">
|
|
<title>size_all_terms</title>
|
|
<g id="a_node21"><a xlink:title="size_all_terms theory/Enumerate.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-1078" rx="45.07" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-1075.8" font-family="Inter" font-size="9.00" fill="#000000">size_all_terms</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- in_comb->size_all_terms -->
|
|
<g id="edge1" class="edge">
|
|
<title>in_comb->size_all_terms</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M105.03,-1099.31C138.65,-1095.25 193.17,-1088.66 232.7,-1083.89"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="233.21,-1085.94 238.92,-1083.14 232.71,-1081.77 233.21,-1085.94"/>
|
|
</g>
|
|
<!-- pow2_pos -->
|
|
<g id="node20" class="node">
|
|
<title>pow2_pos</title>
|
|
<g id="a_node20"><a xlink:title="pow2_pos theory/Enumerate.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1053" rx="35.59" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1050.8" font-family="Inter" font-size="9.00" fill="#000000">pow2_pos</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- pow2_pos->size_all_terms -->
|
|
<g id="edge2" class="edge">
|
|
<title>pow2_pos->size_all_terms</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M108.67,-1057.13C142.56,-1061.22 194.8,-1067.53 232.97,-1072.14"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="232.76,-1074.23 238.97,-1072.87 233.27,-1070.07 232.76,-1074.23"/>
|
|
</g>
|
|
<!-- Plus_red1_context -->
|
|
<g id="node22" class="node">
|
|
<title>Plus_red1_context</title>
|
|
<g id="a_node22"><a xlink:title="Plus_red1_context theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="654.03" cy="-93" rx="57.32" ry="18"/>
|
|
<text text-anchor="middle" x="654.03" y="-90.8" font-family="Inter" font-size="9.00" fill="#000000">Plus_red1_context</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- lemma_2_3_beta_sim -->
|
|
<g id="node29" class="node">
|
|
<title>lemma_2_3_beta_sim</title>
|
|
<g id="a_node29"><a xlink:title="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v proved">
|
|
<path fill="#ffffff" stroke="#000000" d="M887.03,-136C887.03,-136 798.03,-136 798.03,-136 792.03,-136 786.03,-130 786.03,-124 786.03,-124 786.03,-112 786.03,-112 786.03,-106 792.03,-100 798.03,-100 798.03,-100 887.03,-100 887.03,-100 893.03,-100 899.03,-106 899.03,-112 899.03,-112 899.03,-124 899.03,-124 899.03,-130 893.03,-136 887.03,-136"/>
|
|
<text text-anchor="middle" x="842.53" y="-115.8" font-family="Inter" font-size="9.00" fill="#000000">lemma_2_3_beta_sim</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- Plus_red1_context->lemma_2_3_beta_sim -->
|
|
<g id="edge23" class="edge">
|
|
<title>Plus_red1_context->lemma_2_3_beta_sim</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M706.98,-99.96C729.54,-102.99 756.14,-106.55 779.71,-109.71"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="779.72,-111.83 785.95,-110.55 780.28,-107.67 779.72,-111.83"/>
|
|
</g>
|
|
<!-- Plus_step_trans -->
|
|
<g id="node23" class="node">
|
|
<title>Plus_step_trans</title>
|
|
<g id="a_node23"><a xlink:title="Plus_step_trans theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1153" rx="49.8" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1150.8" font-family="Inter" font-size="9.00" fill="#000000">Plus_step_trans</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- Plus_trans -->
|
|
<g id="node24" class="node">
|
|
<title>Plus_trans</title>
|
|
<g id="a_node24"><a xlink:title="Plus_trans theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1203" rx="35.59" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1200.8" font-family="Inter" font-size="9.00" fill="#000000">Plus_trans</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- lemma_2_2_full_comp -->
|
|
<g id="node28" class="node">
|
|
<title>lemma_2_2_full_comp</title>
|
|
<g id="a_node28"><a xlink:title="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v proved">
|
|
<path fill="#ffffff" stroke="#000000" d="M700.03,-161C700.03,-161 608.03,-161 608.03,-161 602.03,-161 596.03,-155 596.03,-149 596.03,-149 596.03,-137 596.03,-137 596.03,-131 602.03,-125 608.03,-125 608.03,-125 700.03,-125 700.03,-125 706.03,-125 712.03,-131 712.03,-137 712.03,-137 712.03,-149 712.03,-149 712.03,-155 706.03,-161 700.03,-161"/>
|
|
<text text-anchor="middle" x="654.03" y="-140.8" font-family="Inter" font-size="9.00" fill="#000000">lemma_2_2_full_comp</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- full_comp_aux->lemma_2_2_full_comp -->
|
|
<g id="edge17" class="edge">
|
|
<title>full_comp_aux->lemma_2_2_full_comp</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M521.65,-143C542.41,-143 567.24,-143 589.7,-143"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="589.96,-145.1 595.96,-143 589.96,-140.9 589.96,-145.1"/>
|
|
</g>
|
|
<!-- red1_root_fv -->
|
|
<g id="node37" class="node">
|
|
<title>red1_root_fv</title>
|
|
<g id="a_node37"><a xlink:title="red1_root_fv theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="474.45" cy="-353" rx="42.29" ry="18"/>
|
|
<text text-anchor="middle" x="474.45" y="-350.8" font-family="Inter" font-size="9.00" fill="#000000">red1_root_fv</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- fvs_zplug_lift->red1_root_fv -->
|
|
<g id="edge19" class="edge">
|
|
<title>fvs_zplug_lift->red1_root_fv</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M325.61,-353C355.33,-353 395.18,-353 426.01,-353"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="426.05,-355.1 432.05,-353 426.05,-350.9 426.05,-355.1"/>
|
|
</g>
|
|
<!-- lemma_2_1_fv_preserved -->
|
|
<g id="node27" class="node">
|
|
<title>lemma_2_1_fv_preserved</title>
|
|
<g id="a_node27"><a xlink:title="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v proved">
|
|
<path fill="#ffffff" stroke="#000000" d="M896.03,-396C896.03,-396 789.03,-396 789.03,-396 783.03,-396 777.03,-390 777.03,-384 777.03,-384 777.03,-372 777.03,-372 777.03,-366 783.03,-360 789.03,-360 789.03,-360 896.03,-360 896.03,-360 902.03,-360 908.03,-366 908.03,-372 908.03,-372 908.03,-384 908.03,-384 908.03,-390 902.03,-396 896.03,-396"/>
|
|
<text text-anchor="middle" x="842.53" y="-375.8" font-family="Inter" font-size="9.00" fill="#000000">lemma_2_1_fv_preserved</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- lemma_2_1_fv_preserved->gen_fv_preserved -->
|
|
<g id="edge30" class="edge">
|
|
<title>lemma_2_1_fv_preserved->gen_fv_preserved</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M908.27,-378C929.77,-378 953.63,-378 974.81,-378"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="975.01,-380.1 981.01,-378 975.01,-375.9 975.01,-380.1"/>
|
|
</g>
|
|
<!-- lemma_2_1_fv_preserved->corpus_fv_preserved -->
|
|
<g id="edge40" class="edge">
|
|
<title>lemma_2_1_fv_preserved->corpus_fv_preserved</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M908.27,-361.14C932.66,-354.79 960.06,-347.66 983.18,-341.64"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="983.99,-343.59 989.27,-340.05 982.94,-339.53 983.99,-343.59"/>
|
|
</g>
|
|
<!-- lemma_2_2_full_comp->lemma_2_3_beta_sim -->
|
|
<g id="edge24" class="edge">
|
|
<title>lemma_2_2_full_comp->lemma_2_3_beta_sim</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M712.26,-135.33C733.69,-132.46 758.13,-129.18 779.94,-126.26"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="780.35,-128.32 786.02,-125.44 779.79,-124.16 780.35,-128.32"/>
|
|
</g>
|
|
<!-- occurs_count_false -->
|
|
<g id="node30" class="node">
|
|
<title>occurs_count_false</title>
|
|
<g id="a_node30"><a xlink:title="occurs_count_false theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-118" rx="58.78" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-115.8" font-family="Inter" font-size="9.00" fill="#000000">occurs_count_false</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- occurs_count_zfill_plug -->
|
|
<g id="node33" class="node">
|
|
<title>occurs_count_zfill_plug</title>
|
|
<g id="a_node33"><a xlink:title="occurs_count_zfill_plug theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-118" rx="70.37" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-115.8" font-family="Inter" font-size="9.00" fill="#000000">occurs_count_zfill_plug</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- occurs_count_false->occurs_count_zfill_plug -->
|
|
<g id="edge7" class="edge">
|
|
<title>occurs_count_false->occurs_count_zfill_plug</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M132.42,-118C155.13,-118 181.49,-118 205.67,-118"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="205.77,-120.1 211.77,-118 205.77,-115.9 205.77,-120.1"/>
|
|
</g>
|
|
<!-- occurs_count_pos -->
|
|
<g id="node31" class="node">
|
|
<title>occurs_count_pos</title>
|
|
<g id="a_node31"><a xlink:title="occurs_count_pos theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="474.45" cy="-18" rx="56.66" ry="18"/>
|
|
<text text-anchor="middle" x="474.45" y="-15.8" font-family="Inter" font-size="9.00" fill="#000000">occurs_count_pos</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- occurs_count_zero -->
|
|
<g id="node32" class="node">
|
|
<title>occurs_count_zero</title>
|
|
<g id="a_node32"><a xlink:title="occurs_count_zero theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-18" rx="58.13" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-15.8" font-family="Inter" font-size="9.00" fill="#000000">occurs_count_zero</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- occurs_count_zero->full_comp_aux -->
|
|
<g id="edge11" class="edge">
|
|
<title>occurs_count_zero->full_comp_aux</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M321,-31.52C337.36,-37.41 352.87,-43 352.87,-43 352.87,-43 413.53,-93.3 448.8,-122.56"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="447.85,-124.5 453.81,-126.71 450.53,-121.26 447.85,-124.5"/>
|
|
</g>
|
|
<!-- occurs_count_zero->occurs_count_pos -->
|
|
<g id="edge6" class="edge">
|
|
<title>occurs_count_zero->occurs_count_pos</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M340.96,-18C363.32,-18 388.98,-18 411.73,-18"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="411.75,-20.1 417.75,-18 411.75,-15.9 411.75,-20.1"/>
|
|
</g>
|
|
<!-- occurs_count_zfill_plug->full_comp_aux -->
|
|
<g id="edge12" class="edge">
|
|
<title>occurs_count_zfill_plug->full_comp_aux</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M345.39,-126.15C370.85,-129.5 399.93,-133.33 423.93,-136.48"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="423.7,-138.57 429.92,-137.27 424.25,-134.41 423.7,-138.57"/>
|
|
</g>
|
|
<!-- occurs_lift_self -->
|
|
<g id="node34" class="node">
|
|
<title>occurs_lift_self</title>
|
|
<g id="a_node34"><a xlink:title="occurs_lift_self theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-185" rx="47.19" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-182.8" font-family="Inter" font-size="9.00" fill="#000000">occurs_lift_self</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- occurs_lift_self->occurs_count_zfill_plug -->
|
|
<g id="edge8" class="edge">
|
|
<title>occurs_lift_self->occurs_count_zfill_plug</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M110.07,-173.48C143.75,-162.58 194.6,-146.11 232.17,-133.95"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="233.02,-135.88 238.08,-132.04 231.73,-131.89 233.02,-135.88"/>
|
|
</g>
|
|
<!-- occurs_lift_self->open_rec_zplug_lift -->
|
|
<g id="edge9" class="edge">
|
|
<title>occurs_lift_self->open_rec_zplug_lift</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M117.38,-191.84C148.03,-196.73 189.63,-203.36 223.27,-208.72"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="223.19,-210.84 229.45,-209.71 223.86,-206.69 223.19,-210.84"/>
|
|
</g>
|
|
<!-- open_rec_zplug_lift->full_comp_aux -->
|
|
<g id="edge14" class="edge">
|
|
<title>open_rec_zplug_lift->full_comp_aux</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M321.41,-204.33C337.62,-198.49 352.87,-193 352.87,-193 352.87,-193 401.07,-173.02 436.52,-158.32"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="437.35,-160.24 442.09,-156.01 435.74,-156.36 437.35,-160.24"/>
|
|
</g>
|
|
<!-- plug_fv_mono -->
|
|
<g id="node36" class="node">
|
|
<title>plug_fv_mono</title>
|
|
<g id="a_node36"><a xlink:title="plug_fv_mono theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="474.45" cy="-403" rx="46.38" ry="18"/>
|
|
<text text-anchor="middle" x="474.45" y="-400.8" font-family="Inter" font-size="9.00" fill="#000000">plug_fv_mono</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- red1r_fv -->
|
|
<g id="node38" class="node">
|
|
<title>red1r_fv</title>
|
|
<g id="a_node38"><a xlink:title="red1r_fv theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="654.03" cy="-378" rx="31.35" ry="18"/>
|
|
<text text-anchor="middle" x="654.03" y="-375.8" font-family="Inter" font-size="9.00" fill="#000000">red1r_fv</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- plug_fv_mono->red1r_fv -->
|
|
<g id="edge20" class="edge">
|
|
<title>plug_fv_mono->red1r_fv</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M518.44,-396.95C548.69,-392.69 588.71,-387.06 617.23,-383.04"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="617.85,-385.07 623.5,-382.16 617.26,-380.92 617.85,-385.07"/>
|
|
</g>
|
|
<!-- red1_root_fv->red1r_fv -->
|
|
<g id="edge21" class="edge">
|
|
<title>red1_root_fv->red1r_fv</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M514.86,-358.55C545.58,-362.87 587.86,-368.82 617.53,-373"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="617.43,-375.11 623.67,-373.87 618.02,-370.95 617.43,-375.11"/>
|
|
</g>
|
|
<!-- red1r_fv->lemma_2_1_fv_preserved -->
|
|
<g id="edge22" class="edge">
|
|
<title>red1r_fv->lemma_2_1_fv_preserved</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M685.41,-378C708.44,-378 741.05,-378 770.52,-378"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="770.75,-380.1 776.75,-378 770.75,-375.9 770.75,-380.1"/>
|
|
</g>
|
|
<!-- zdecs_nonempty -->
|
|
<g id="node39" class="node">
|
|
<title>zdecs_nonempty</title>
|
|
<g id="a_node39"><a xlink:title="zdecs_nonempty theory/Metatheory.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-68" rx="53.89" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-65.8" font-family="Inter" font-size="9.00" fill="#000000">zdecs_nonempty</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- zdecs_nonempty->full_comp_aux -->
|
|
<g id="edge15" class="edge">
|
|
<title>zdecs_nonempty->full_comp_aux</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M319.78,-81.09C336.58,-87.13 352.87,-93 352.87,-93 352.87,-93 401.07,-112.98 436.52,-127.68"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="435.74,-129.64 442.09,-129.99 437.35,-125.76 435.74,-129.64"/>
|
|
</g>
|
|
<!-- check_all_true -->
|
|
<g id="node40" class="node">
|
|
<title>check_all_true</title>
|
|
<g id="a_node40"><a xlink:title="check_all_true theory/Random.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="1211.82" cy="-278" rx="46.53" ry="18"/>
|
|
<text text-anchor="middle" x="1211.82" y="-275.8" font-family="Inter" font-size="9.00" fill="#000000">check_all_true</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- check_all_true->enumerate_check -->
|
|
<g id="edge3" class="edge">
|
|
<title>check_all_true->enumerate_check</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M1258.71,-278C1276.76,-278 1297.76,-278 1317.13,-278"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="1317.35,-280.1 1323.35,-278 1317.35,-275.9 1317.35,-280.1"/>
|
|
</g>
|
|
<!-- check_term_true->check_all_true -->
|
|
<g id="edge27" class="edge">
|
|
<title>check_term_true->check_all_true</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M1090.47,-278C1112.21,-278 1137.31,-278 1158.94,-278"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="1158.95,-280.1 1164.95,-278 1158.95,-275.9 1158.95,-280.1"/>
|
|
</g>
|
|
<!-- gen_list_length -->
|
|
<g id="node44" class="node">
|
|
<title>gen_list_length</title>
|
|
<g id="a_node44"><a xlink:title="gen_list_length theory/Random.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1253" rx="49.15" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1250.8" font-family="Inter" font-size="9.00" fill="#000000">gen_list_length</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- close_rec_app -->
|
|
<g id="node46" class="node">
|
|
<title>close_rec_app</title>
|
|
<g id="a_node46"><a xlink:title="close_rec_app theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1303" rx="46.38" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1300.8" font-family="Inter" font-size="9.00" fill="#000000">close_rec_app</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- close_rec_esub -->
|
|
<g id="node47" class="node">
|
|
<title>close_rec_esub</title>
|
|
<g id="a_node47"><a xlink:title="close_rec_esub theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1353" rx="48.49" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1350.8" font-family="Inter" font-size="9.00" fill="#000000">close_rec_esub</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- close_rec_lam -->
|
|
<g id="node48" class="node">
|
|
<title>close_rec_lam</title>
|
|
<g id="a_node48"><a xlink:title="close_rec_lam theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1403" rx="45.72" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1400.8" font-family="Inter" font-size="9.00" fill="#000000">close_rec_lam</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_app -->
|
|
<g id="node49" class="node">
|
|
<title>open_rec_app</title>
|
|
<g id="a_node49"><a xlink:title="open_rec_app theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1453" rx="46.38" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1450.8" font-family="Inter" font-size="9.00" fill="#000000">open_rec_app</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_esub -->
|
|
<g id="node50" class="node">
|
|
<title>open_rec_esub</title>
|
|
<g id="a_node50"><a xlink:title="open_rec_esub theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1503" rx="48.49" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1500.8" font-family="Inter" font-size="9.00" fill="#000000">open_rec_esub</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_lam -->
|
|
<g id="node51" class="node">
|
|
<title>open_rec_lam</title>
|
|
<g id="a_node51"><a xlink:title="open_rec_lam theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1553" rx="45.72" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1550.8" font-family="Inter" font-size="9.00" fill="#000000">open_rec_lam</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_lc -->
|
|
<g id="node52" class="node">
|
|
<title>open_rec_lc</title>
|
|
<g id="a_node52"><a xlink:title="open_rec_lc theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="282.44" cy="-1603" rx="40.33" ry="18"/>
|
|
<text text-anchor="middle" x="282.44" y="-1600.8" font-family="Inter" font-size="9.00" fill="#000000">open_rec_lc</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_lc_atom -->
|
|
<g id="node53" class="node">
|
|
<title>open_rec_lc_atom</title>
|
|
<g id="a_node53"><a xlink:title="open_rec_lc_atom theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1603" rx="56.66" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1600.8" font-family="Inter" font-size="9.00" fill="#000000">open_rec_lc_atom</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- open_rec_lc_atom->open_rec_lc -->
|
|
<g id="edge36" class="edge">
|
|
<title>open_rec_lc_atom->open_rec_lc</title>
|
|
<path fill="none" stroke="#000000" stroke-width="0.8" d="M130.23,-1603C163.33,-1603 204.79,-1603 235.92,-1603"/>
|
|
<polygon fill="#000000" stroke="#000000" stroke-width="0.8" points="236.01,-1605.1 242.01,-1603 236.01,-1600.9 236.01,-1605.1"/>
|
|
</g>
|
|
<!-- subst_app -->
|
|
<g id="node54" class="node">
|
|
<title>subst_app</title>
|
|
<g id="a_node54"><a xlink:title="subst_app theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1653" rx="36.25" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1650.8" font-family="Inter" font-size="9.00" fill="#000000">subst_app</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- subst_esub -->
|
|
<g id="node55" class="node">
|
|
<title>subst_esub</title>
|
|
<g id="a_node55"><a xlink:title="subst_esub theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1703" rx="39.02" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1700.8" font-family="Inter" font-size="9.00" fill="#000000">subst_esub</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
<!-- subst_lam -->
|
|
<g id="node56" class="node">
|
|
<title>subst_lam</title>
|
|
<g id="a_node56"><a xlink:title="subst_lam theory/Substitution.v proved">
|
|
<ellipse fill="#ffffff" stroke="#000000" cx="73.5" cy="-1753" rx="35.59" ry="18"/>
|
|
<text text-anchor="middle" x="73.5" y="-1750.8" font-family="Inter" font-size="9.00" fill="#000000">subst_lam</text>
|
|
</a>
|
|
</g>
|
|
</g>
|
|
</g>
|
|
</svg>
|
