lambda-sub/graphs/dependency.svg

<?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: theorem_deps Pages: 1 -->
<svg width="1085pt" height="1875pt"
 viewBox="0.00 0.00 1085.21 1875.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 1871)">
<title>theorem_deps</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-1871 1081.21,-1871 1081.21,4 -4,4"/>
<text text-anchor="start" x="302.6" y="-1854.4" font-family="Inter" font-weight="bold" font-size="12.00">Milner&#39;s Lambda&#45;Calculus with Partial Substitutions &#45; theorem dependency (M2)</text>
<text text-anchor="start" x="465.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#38761d">proved</text>
<text text-anchor="start" x="495.6" y="-1844.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
<text text-anchor="start" x="502.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#b45f06">stated</text>
<text text-anchor="start" x="529.6" y="-1844.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
<text text-anchor="start" x="536.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#777777">planned</text>
<text text-anchor="start" x="570.6" y="-1844.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
<text text-anchor="start" x="577.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#cc0000">blocked</text>
<!-- fvs_lift -->
<g id="node1" class="node">
<title>fvs_lift</title>
<g id="a_node1"><a xlink:title="fvs_lift theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-650" rx="27" ry="18"/>
<text text-anchor="middle" x="65.24" y="-647.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_lift</text>
</a>
</g>
</g>
<!-- open_rec_fvs -->
<g id="node10" class="node">
<title>open_rec_fvs</title>
<g id="a_node10"><a xlink:title="open_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-572" rx="41.64" ry="18"/>
<text text-anchor="middle" x="239.88" y="-569.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_fvs</text>
</a>
</g>
</g>
<!-- fvs_lift&#45;&gt;open_rec_fvs -->
<g id="edge2" class="edge">
<title>fvs_lift&#45;&gt;open_rec_fvs</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M87.39,-639.18C108.87,-628.32 143.18,-611.35 173.48,-598 182.74,-593.92 192.85,-589.76 202.3,-586"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="203.27,-587.87 208.08,-583.71 201.72,-583.97 203.27,-587.87"/>
</g>
<!-- fvs_zplug_lift -->
<g id="node25" class="node">
<title>fvs_zplug_lift</title>
<g id="a_node25"><a xlink:title="fvs_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-676" rx="40.98" ry="18"/>
<text text-anchor="middle" x="239.88" y="-673.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_zplug_lift</text>
</a>
</g>
</g>
<!-- fvs_lift&#45;&gt;fvs_zplug_lift -->
<g id="edge21" class="edge">
<title>fvs_lift&#45;&gt;fvs_zplug_lift</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M91.71,-653.84C118.82,-657.92 162.22,-664.45 194.87,-669.37"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.59,-671.45 200.84,-670.27 195.22,-667.3 194.59,-671.45"/>
</g>
<!-- lift_lc -->
<g id="node2" class="node">
<title>lift_lc</title>
<g id="a_node2"><a xlink:title="lift_lc theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-728" rx="27" ry="18"/>
<text text-anchor="middle" x="65.24" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">lift_lc</text>
</a>
</g>
</g>
<!-- lift_0_lc -->
<g id="node3" class="node">
<title>lift_0_lc</title>
<g id="a_node3"><a xlink:title="lift_0_lc theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-728" rx="27.93" ry="18"/>
<text text-anchor="middle" x="239.88" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">lift_0_lc</text>
</a>
</g>
</g>
<!-- lift_lc&#45;&gt;lift_0_lc -->
<g id="edge1" class="edge">
<title>lift_lc&#45;&gt;lift_0_lc</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-728C122.79,-728 172.78,-728 205.77,-728"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="206.13,-730.1 212.13,-728 206.13,-725.9 206.13,-730.1"/>
</g>
<!-- subst_fvar_self -->
<g id="node12" class="node">
<title>subst_fvar_self</title>
<g id="a_node12"><a xlink:title="subst_fvar_self theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-728" rx="45.72" ry="18"/>
<text text-anchor="middle" x="408.74" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_self</text>
</a>
</g>
</g>
<!-- lift_0_lc&#45;&gt;subst_fvar_self -->
<g id="edge6" class="edge">
<title>lift_0_lc&#45;&gt;subst_fvar_self</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M267.69,-728C291.68,-728 327.51,-728 356.92,-728"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="357.09,-730.1 363.09,-728 357.09,-725.9 357.09,-730.1"/>
</g>
<!-- open_rec_bvar -->
<g id="node4" class="node">
<title>open_rec_bvar</title>
<g id="a_node4"><a xlink:title="open_rec_bvar theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-520" rx="46.38" ry="18"/>
<text text-anchor="middle" x="65.24" y="-517.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar</text>
</a>
</g>
</g>
<!-- open_rec_bvar&#45;&gt;open_rec_fvs -->
<g id="edge3" class="edge">
<title>open_rec_bvar&#45;&gt;open_rec_fvs</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.43,-530.9C130.77,-539.44 170.14,-551.29 199.31,-560.08"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="199.02,-562.19 205.37,-561.91 200.23,-558.17 199.02,-562.19"/>
</g>
<!-- open_close -->
<g id="node11" class="node">
<title>open_close</title>
<g id="a_node11"><a xlink:title="open_close theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-520" rx="36.9" ry="18"/>
<text text-anchor="middle" x="239.88" y="-517.8" font-family="Inter" font-size="9.00" fill="#222222">open_close</text>
</a>
</g>
</g>
<!-- open_rec_bvar&#45;&gt;open_close -->
<g id="edge5" class="edge">
<title>open_rec_bvar&#45;&gt;open_close</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M111.6,-520C137.96,-520 170.95,-520 196.74,-520"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.79,-522.1 202.79,-520 196.79,-517.9 196.79,-522.1"/>
</g>
<!-- close_rec_fvar -->
<g id="node5" class="node">
<title>close_rec_fvar</title>
<g id="a_node5"><a xlink:title="close_rec_fvar theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-780" rx="45.07" ry="18"/>
<text text-anchor="middle" x="65.24" y="-777.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvar</text>
</a>
</g>
</g>
<!-- open_rec_occurs_false -->
<g id="node6" class="node">
<title>open_rec_occurs_false</title>
<g id="a_node6"><a xlink:title="open_rec_occurs_false theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-109" rx="65.48" ry="18"/>
<text text-anchor="middle" x="65.24" y="-106.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_occurs_false</text>
</a>
</g>
</g>
<!-- open_rec_zplug_lift -->
<g id="node22" class="node">
<title>open_rec_zplug_lift</title>
<g id="a_node22"><a xlink:title="open_rec_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-156" rx="56.66" ry="18"/>
<text text-anchor="middle" x="239.88" y="-153.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_zplug_lift</text>
</a>
</g>
</g>
<!-- open_rec_occurs_false&#45;&gt;open_rec_zplug_lift -->
<g id="edge13" class="edge">
<title>open_rec_occurs_false&#45;&gt;open_rec_zplug_lift</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M112.5,-121.6C136.54,-128.14 165.89,-136.13 190.25,-142.76"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="189.99,-144.87 196.34,-144.42 191.1,-140.82 189.99,-144.87"/>
</g>
<!-- full_comp_aux -->
<g id="node23" class="node">
<title>full_comp_aux</title>
<g id="a_node23"><a xlink:title="full_comp_aux theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-156" rx="44.41" ry="18"/>
<text text-anchor="middle" x="408.74" y="-153.8" font-family="Inter" font-size="9.00" fill="#222222">full_comp_aux</text>
</a>
</g>
</g>
<!-- open_rec_occurs_false&#45;&gt;full_comp_aux -->
<g id="edge16" class="edge">
<title>open_rec_occurs_false&#45;&gt;full_comp_aux</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M129.77,-111.72C178.37,-114.49 246.89,-119.87 306.27,-130 326.24,-133.41 348.05,-138.77 366.31,-143.75"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="366.01,-145.85 372.36,-145.42 367.13,-141.8 366.01,-145.85"/>
</g>
<!-- subst_notin -->
<g id="node68" class="node">
<title>subst_notin</title>
<g id="a_node68"><a xlink:title="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-18" rx="37.56" ry="18"/>
<text text-anchor="middle" x="239.88" y="-15.8" font-family="Inter" font-size="9.00" fill="#222222">subst_notin</text>
</a>
</g>
</g>
<!-- open_rec_occurs_false&#45;&gt;subst_notin -->
<g id="edge53" class="edge">
<title>open_rec_occurs_false&#45;&gt;subst_notin</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M91.13,-92.28C112.45,-78.36 144.24,-58.55 173.48,-44 182.99,-39.27 193.58,-34.75 203.43,-30.85"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="204.3,-32.77 209.12,-28.63 202.77,-28.85 204.3,-32.77"/>
</g>
<!-- close_rec_notin -->
<g id="node7" class="node">
<title>close_rec_notin</title>
<g id="a_node7"><a xlink:title="close_rec_notin theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-18" rx="47.84" ry="18"/>
<text text-anchor="middle" x="65.24" y="-15.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_notin</text>
</a>
</g>
</g>
<!-- close_rec_notin&#45;&gt;subst_notin -->
<g id="edge52" class="edge">
<title>close_rec_notin&#45;&gt;subst_notin</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M113.41,-18C139.18,-18 170.86,-18 195.93,-18"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.16,-20.1 202.16,-18 196.16,-15.9 196.16,-20.1"/>
</g>
<!-- close_rec_fvs -->
<g id="node8" class="node">
<title>close_rec_fvs</title>
<g id="a_node8"><a xlink:title="close_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-624" rx="42.95" ry="18"/>
<text text-anchor="middle" x="239.88" y="-621.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvs</text>
</a>
</g>
</g>
<!-- subst_fvs -->
<g id="node14" class="node">
<title>subst_fvs</title>
<g id="a_node14"><a xlink:title="subst_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-572" rx="32.16" ry="18"/>
<text text-anchor="middle" x="408.74" y="-569.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvs</text>
</a>
</g>
</g>
<!-- close_rec_fvs&#45;&gt;subst_fvs -->
<g id="edge7" class="edge">
<title>close_rec_fvs&#45;&gt;subst_fvs</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M274.64,-613.48C303.63,-604.44 345.18,-591.49 374.12,-582.48"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="374.99,-584.4 380.1,-580.61 373.74,-580.39 374.99,-584.4"/>
</g>
<!-- open_rec_bvar_neq -->
<g id="node9" class="node">
<title>open_rec_bvar_neq</title>
<g id="a_node9"><a xlink:title="open_rec_bvar_neq theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-572" rx="57.97" ry="18"/>
<text text-anchor="middle" x="65.24" y="-569.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar_neq</text>
</a>
</g>
</g>
<!-- open_rec_bvar_neq&#45;&gt;open_rec_fvs -->
<g id="edge4" class="edge">
<title>open_rec_bvar_neq&#45;&gt;open_rec_fvs</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M123.25,-572C145.5,-572 170.71,-572 191.9,-572"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.05,-574.1 198.05,-572 192.05,-569.9 192.05,-574.1"/>
</g>
<!-- open_rec_fvs&#45;&gt;subst_fvs -->
<g id="edge8" class="edge">
<title>open_rec_fvs&#45;&gt;subst_fvs</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.7,-572C308.67,-572 343.77,-572 370.08,-572"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="370.23,-574.1 376.23,-572 370.23,-569.9 370.23,-574.1"/>
</g>
<!-- subst_lc_self -->
<g id="node69" class="node">
<title>subst_lc_self</title>
<g id="a_node69"><a xlink:title="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-728" rx="40.33" ry="18"/>
<text text-anchor="middle" x="565.21" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lc_self</text>
</a>
</g>
</g>
<!-- subst_fvar_self&#45;&gt;subst_lc_self -->
<g id="edge54" class="edge">
<title>subst_fvar_self&#45;&gt;subst_lc_self</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M454.42,-728C474.52,-728 498.23,-728 518.46,-728"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="518.62,-730.1 524.62,-728 518.62,-725.9 518.62,-730.1"/>
</g>
<!-- subst_fvar_other -->
<g id="node13" class="node">
<title>subst_fvar_other</title>
<g id="a_node13"><a xlink:title="subst_fvar_other theory/Binding.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-832" rx="49.8" ry="18"/>
<text text-anchor="middle" x="65.24" y="-829.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_other</text>
</a>
</g>
</g>
<!-- subst_other -->
<g id="node70" class="node">
<title>subst_other</title>
<g id="a_node70"><a xlink:title="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-832" rx="37.56" ry="18"/>
<text text-anchor="middle" x="239.88" y="-829.8" font-family="Inter" font-size="9.00" fill="#222222">subst_other</text>
</a>
</g>
</g>
<!-- subst_fvar_other&#45;&gt;subst_other -->
<g id="edge55" class="edge">
<title>subst_fvar_other&#45;&gt;subst_other</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M115.25,-832C140.7,-832 171.52,-832 196.02,-832"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.1,-834.1 202.1,-832 196.1,-829.9 196.1,-834.1"/>
</g>
<!-- Plus_red1_context -->
<g id="node15" class="node">
<title>Plus_red1_context</title>
<g id="a_node15"><a xlink:title="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-208" rx="53.23" ry="18"/>
<text text-anchor="middle" x="565.21" y="-205.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_red1_context</text>
</a>
</g>
</g>
<!-- lemma_2_3_beta_sim -->
<g id="node30" class="node">
<title>lemma_2_3_beta_sim</title>
<g id="a_node30"><a xlink:title="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<path fill="#d9ead3" stroke="#38761d" d="M763.21,-200C763.21,-200 681.21,-200 681.21,-200 675.21,-200 669.21,-194 669.21,-188 669.21,-188 669.21,-176 669.21,-176 669.21,-170 675.21,-164 681.21,-164 681.21,-164 763.21,-164 763.21,-164 769.21,-164 775.21,-170 775.21,-176 775.21,-176 775.21,-188 775.21,-188 775.21,-194 769.21,-200 763.21,-200"/>
<text text-anchor="middle" x="722.21" y="-179.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_3_beta_sim</text>
</a>
</g>
</g>
<!-- Plus_red1_context&#45;&gt;lemma_2_3_beta_sim -->
<g id="edge26" class="edge">
<title>Plus_red1_context&#45;&gt;lemma_2_3_beta_sim</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M613.13,-200.13C628.84,-197.49 646.55,-194.52 663.02,-191.76"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="663.46,-193.82 669.03,-190.75 662.76,-189.67 663.46,-193.82"/>
</g>
<!-- occurs_count_zero -->
<g id="node16" class="node">
<title>occurs_count_zero</title>
<g id="a_node16"><a xlink:title="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-70" rx="54.7" ry="18"/>
<text text-anchor="middle" x="239.88" y="-67.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zero</text>
</a>
</g>
</g>
<!-- occurs_count_pos -->
<g id="node18" class="node">
<title>occurs_count_pos</title>
<g id="a_node18"><a xlink:title="occurs_count_pos theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-70" rx="53.89" ry="18"/>
<text text-anchor="middle" x="408.74" y="-67.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_pos</text>
</a>
</g>
</g>
<!-- occurs_count_zero&#45;&gt;occurs_count_pos -->
<g id="edge9" class="edge">
<title>occurs_count_zero&#45;&gt;occurs_count_pos</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M295.05,-70C312.17,-70 331.17,-70 348.62,-70"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.97,-72.1 354.97,-70 348.97,-67.9 348.97,-72.1"/>
</g>
<!-- occurs_count_zero&#45;&gt;full_comp_aux -->
<g id="edge14" class="edge">
<title>occurs_count_zero&#45;&gt;full_comp_aux</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M273.37,-84.33C283.94,-89.15 295.68,-94.66 306.27,-100 330.41,-112.18 357.16,-127 377.13,-138.33"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="376.33,-140.29 382.58,-141.43 378.41,-136.64 376.33,-140.29"/>
</g>
<!-- occurs_count_false -->
<g id="node17" class="node">
<title>occurs_count_false</title>
<g id="a_node17"><a xlink:title="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-213" rx="56.66" ry="18"/>
<text text-anchor="middle" x="65.24" y="-210.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_false</text>
</a>
</g>
</g>
<!-- occurs_count_zfill_plug -->
<g id="node21" class="node">
<title>occurs_count_zfill_plug</title>
<g id="a_node21"><a xlink:title="occurs_count_zfill_plug theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-208" rx="66.29" ry="18"/>
<text text-anchor="middle" x="239.88" y="-205.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zfill_plug</text>
</a>
</g>
</g>
<!-- occurs_count_false&#45;&gt;occurs_count_zfill_plug -->
<g id="edge10" class="edge">
<title>occurs_count_false&#45;&gt;occurs_count_zfill_plug</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M121.81,-211.39C136.43,-210.97 152.41,-210.5 167.72,-210.06"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="167.84,-212.16 173.78,-209.89 167.72,-207.96 167.84,-212.16"/>
</g>
<!-- occurs_lift_self -->
<g id="node19" class="node">
<title>occurs_lift_self</title>
<g id="a_node19"><a xlink:title="occurs_lift_self theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-161" rx="46.38" ry="18"/>
<text text-anchor="middle" x="65.24" y="-158.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_lift_self</text>
</a>
</g>
</g>
<!-- occurs_lift_self&#45;&gt;occurs_count_zfill_plug -->
<g id="edge11" class="edge">
<title>occurs_lift_self&#45;&gt;occurs_count_zfill_plug</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M103.7,-171.2C127.85,-177.77 159.62,-186.42 186.29,-193.68"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.91,-195.76 192.25,-195.31 187.01,-191.7 185.91,-195.76"/>
</g>
<!-- occurs_lift_self&#45;&gt;open_rec_zplug_lift -->
<g id="edge12" class="edge">
<title>occurs_lift_self&#45;&gt;open_rec_zplug_lift</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M111.6,-159.69C131.69,-159.1 155.63,-158.41 177.3,-157.78"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="177.41,-159.88 183.35,-157.61 177.29,-155.68 177.41,-159.88"/>
</g>
<!-- zdecs_nonempty -->
<g id="node20" class="node">
<title>zdecs_nonempty</title>
<g id="a_node20"><a xlink:title="zdecs_nonempty theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-260" rx="51.27" ry="18"/>
<text text-anchor="middle" x="239.88" y="-257.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_nonempty</text>
</a>
</g>
</g>
<!-- zdecs_nonempty&#45;&gt;full_comp_aux -->
<g id="edge18" class="edge">
<title>zdecs_nonempty&#45;&gt;full_comp_aux</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M279.56,-248.33C288.79,-244.56 298.27,-239.82 306.27,-234 330.52,-216.35 325.38,-200.13 349.27,-182 355.15,-177.54 361.91,-173.65 368.7,-170.32"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="369.85,-172.1 374.4,-167.66 368.07,-168.3 369.85,-172.1"/>
</g>
<!-- occurs_count_zfill_plug&#45;&gt;full_comp_aux -->
<g id="edge15" class="edge">
<title>occurs_count_zfill_plug&#45;&gt;full_comp_aux</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.28,-194.47C309.85,-186.51 341.99,-176.49 367.07,-168.67"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="367.85,-170.63 372.95,-166.84 366.6,-166.62 367.85,-170.63"/>
</g>
<!-- open_rec_zplug_lift&#45;&gt;full_comp_aux -->
<g id="edge17" class="edge">
<title>open_rec_zplug_lift&#45;&gt;full_comp_aux</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M296.9,-156C316.72,-156 338.87,-156 358.12,-156"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="358.26,-158.1 364.26,-156 358.26,-153.9 358.26,-158.1"/>
</g>
<!-- lemma_2_2_full_comp -->
<g id="node24" class="node">
<title>lemma_2_2_full_comp</title>
<g id="a_node24"><a xlink:title="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<path fill="#d9ead3" stroke="#38761d" d="M607.21,-174C607.21,-174 523.21,-174 523.21,-174 517.21,-174 511.21,-168 511.21,-162 511.21,-162 511.21,-150 511.21,-150 511.21,-144 517.21,-138 523.21,-138 523.21,-138 607.21,-138 607.21,-138 613.21,-138 619.21,-144 619.21,-150 619.21,-150 619.21,-162 619.21,-162 619.21,-168 613.21,-174 607.21,-174"/>
<text text-anchor="middle" x="565.21" y="-153.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_2_full_comp</text>
</a>
</g>
</g>
<!-- full_comp_aux&#45;&gt;lemma_2_2_full_comp -->
<g id="edge20" class="edge">
<title>full_comp_aux&#45;&gt;lemma_2_2_full_comp</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M453.59,-156C469.56,-156 487.88,-156 504.96,-156"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="505.19,-158.1 511.19,-156 505.19,-153.9 505.19,-158.1"/>
</g>
<!-- lemma_2_2_full_comp&#45;&gt;lemma_2_3_beta_sim -->
<g id="edge27" class="edge">
<title>lemma_2_2_full_comp&#45;&gt;lemma_2_3_beta_sim</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M619.55,-164.95C633.57,-167.3 648.76,-169.85 663.03,-172.24"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="662.81,-174.33 669.08,-173.26 663.51,-170.19 662.81,-174.33"/>
</g>
<!-- red1_root_fv -->
<g id="node27" class="node">
<title>red1_root_fv</title>
<g id="a_node27"><a xlink:title="red1_root_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-676" rx="38.87" ry="18"/>
<text text-anchor="middle" x="408.74" y="-673.8" font-family="Inter" font-size="9.00" fill="#222222">red1_root_fv</text>
</a>
</g>
</g>
<!-- fvs_zplug_lift&#45;&gt;red1_root_fv -->
<g id="edge22" class="edge">
<title>fvs_zplug_lift&#45;&gt;red1_root_fv</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-676C306.27,-676 338.37,-676 363.98,-676"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="364.01,-678.1 370.01,-676 364.01,-673.9 364.01,-678.1"/>
</g>
<!-- plug_fv_mono -->
<g id="node26" class="node">
<title>plug_fv_mono</title>
<g id="a_node26"><a xlink:title="plug_fv_mono theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-624" rx="42.95" ry="18"/>
<text text-anchor="middle" x="408.74" y="-621.8" font-family="Inter" font-size="9.00" fill="#222222">plug_fv_mono</text>
</a>
</g>
</g>
<!-- red1r_fv -->
<g id="node28" class="node">
<title>red1r_fv</title>
<g id="a_node28"><a xlink:title="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-624" rx="28.74" ry="18"/>
<text text-anchor="middle" x="565.21" y="-621.8" font-family="Inter" font-size="9.00" fill="#222222">red1r_fv</text>
</a>
</g>
</g>
<!-- plug_fv_mono&#45;&gt;red1r_fv -->
<g id="edge23" class="edge">
<title>plug_fv_mono&#45;&gt;red1r_fv</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M451.54,-624C476.15,-624 506.88,-624 530.03,-624"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="530.04,-626.1 536.04,-624 530.04,-621.9 530.04,-626.1"/>
</g>
<!-- red1_root_fv&#45;&gt;red1r_fv -->
<g id="edge24" class="edge">
<title>red1_root_fv&#45;&gt;red1r_fv</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M440.63,-665.6C467.64,-656.51 506.65,-643.38 533.58,-634.31"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="534.46,-636.23 539.48,-632.33 533.12,-632.25 534.46,-636.23"/>
</g>
<!-- lemma_2_1_fv_preserved -->
<g id="node29" class="node">
<title>lemma_2_1_fv_preserved</title>
<g id="a_node29"><a xlink:title="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
<path fill="#d9ead3" stroke="#38761d" d="M770.21,-629C770.21,-629 674.21,-629 674.21,-629 668.21,-629 662.21,-623 662.21,-617 662.21,-617 662.21,-605 662.21,-605 662.21,-599 668.21,-593 674.21,-593 674.21,-593 770.21,-593 770.21,-593 776.21,-593 782.21,-599 782.21,-605 782.21,-605 782.21,-617 782.21,-617 782.21,-623 776.21,-629 770.21,-629"/>
<text text-anchor="middle" x="722.21" y="-608.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_1_fv_preserved</text>
</a>
</g>
</g>
<!-- red1r_fv&#45;&gt;lemma_2_1_fv_preserved -->
<g id="edge25" class="edge">
<title>red1r_fv&#45;&gt;lemma_2_1_fv_preserved</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M593.92,-621.68C611.19,-620.23 634.18,-618.3 655.87,-616.48"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="656.15,-618.56 661.95,-615.97 655.79,-614.38 656.15,-618.56"/>
</g>
<!-- gen_fv_preserved -->
<g id="node42" class="node">
<title>gen_fv_preserved</title>
<g id="a_node42"><a xlink:title="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-559" rx="52.58" ry="18"/>
<text text-anchor="middle" x="885.25" y="-556.8" font-family="Inter" font-size="9.00" fill="#222222">gen_fv_preserved</text>
</a>
</g>
</g>
<!-- lemma_2_1_fv_preserved&#45;&gt;gen_fv_preserved -->
<g id="edge35" class="edge">
<title>lemma_2_1_fv_preserved&#45;&gt;gen_fv_preserved</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M779.08,-592.96C799.17,-586.47 821.52,-579.25 840.44,-573.15"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="841.13,-575.13 846.19,-571.29 839.84,-571.13 841.13,-575.13"/>
</g>
<!-- corpus_fv_preserved -->
<g id="node82" class="node">
<title>corpus_fv_preserved</title>
<g id="a_node82"><a xlink:title="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-611" rx="60.09" ry="18"/>
<text text-anchor="middle" x="885.25" y="-608.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_fv_preserved</text>
</a>
</g>
</g>
<!-- lemma_2_1_fv_preserved&#45;&gt;corpus_fv_preserved -->
<g id="edge62" class="edge">
<title>lemma_2_1_fv_preserved&#45;&gt;corpus_fv_preserved</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M782.26,-611C794.18,-611 806.79,-611 818.91,-611"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="819.2,-613.1 825.2,-611 819.2,-608.9 819.2,-613.1"/>
</g>
<!-- par_red1_iff -->
<g id="node31" class="node">
<title>par_red1_iff</title>
<g id="a_node31"><a xlink:title="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-884" rx="37.56" ry="18"/>
<text text-anchor="middle" x="65.24" y="-881.8" font-family="Inter" font-size="9.00" fill="#222222">par_red1_iff</text>
</a>
</g>
</g>
<!-- par_to_red1_or_eq -->
<g id="node34" class="node">
<title>par_to_red1_or_eq</title>
<g id="a_node34"><a xlink:title="par_to_red1_or_eq theory/Parallel.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-936" rx="53.23" ry="18"/>
<text text-anchor="middle" x="239.88" y="-933.8" font-family="Inter" font-size="9.00" fill="#222222">par_to_red1_or_eq</text>
</a>
</g>
</g>
<!-- par_red1_iff&#45;&gt;par_to_red1_or_eq -->
<g id="edge28" class="edge">
<title>par_red1_iff&#45;&gt;par_to_red1_or_eq</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M97.5,-893.42C124.38,-901.51 163.47,-913.29 193.73,-922.4"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="193.31,-924.47 199.66,-924.19 194.53,-920.45 193.31,-924.47"/>
</g>
<!-- red1_or_eq_to_par -->
<g id="node35" class="node">
<title>red1_or_eq_to_par</title>
<g id="a_node35"><a xlink:title="red1_or_eq_to_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-884" rx="53.23" ry="18"/>
<text text-anchor="middle" x="239.88" y="-881.8" font-family="Inter" font-size="9.00" fill="#222222">red1_or_eq_to_par</text>
</a>
</g>
</g>
<!-- par_red1_iff&#45;&gt;red1_or_eq_to_par -->
<g id="edge29" class="edge">
<title>par_red1_iff&#45;&gt;red1_or_eq_to_par</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-884C125.39,-884 154.79,-884 180.49,-884"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="180.6,-886.1 186.6,-884 180.6,-881.9 180.6,-886.1"/>
</g>
<!-- red1_in_par -->
<g id="node32" class="node">
<title>red1_in_par</title>
<g id="a_node32"><a xlink:title="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-936" rx="37.56" ry="18"/>
<text text-anchor="middle" x="65.24" y="-933.8" font-family="Inter" font-size="9.00" fill="#222222">red1_in_par</text>
</a>
</g>
</g>
<!-- par_context -->
<g id="node33" class="node">
<title>par_context</title>
<g id="a_node33"><a xlink:title="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-988" rx="38.87" ry="18"/>
<text text-anchor="middle" x="65.24" y="-985.8" font-family="Inter" font-size="9.00" fill="#222222">par_context</text>
</a>
</g>
</g>
<!-- par_reflexive -->
<g id="node36" class="node">
<title>par_reflexive</title>
<g id="a_node36"><a xlink:title="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1040" rx="41.64" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1037.8" font-family="Inter" font-size="9.00" fill="#222222">par_reflexive</text>
</a>
</g>
</g>
<!-- gen_list_length -->
<g id="node37" class="node">
<title>gen_list_length</title>
<g id="a_node37"><a xlink:title="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1092" rx="46.38" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1089.8" font-family="Inter" font-size="9.00" fill="#222222">gen_list_length</text>
</a>
</g>
</g>
<!-- check_term_true -->
<g id="node38" class="node">
<title>check_term_true</title>
<g id="a_node38"><a xlink:title="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-494" rx="50.61" ry="18"/>
<text text-anchor="middle" x="885.25" y="-491.8" font-family="Inter" font-size="9.00" fill="#222222">check_term_true</text>
</a>
</g>
</g>
<!-- check_all_true -->
<g id="node39" class="node">
<title>check_all_true</title>
<g id="a_node39"><a xlink:title="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="1032.75" cy="-494" rx="44.41" ry="18"/>
<text text-anchor="middle" x="1032.75" y="-491.8" font-family="Inter" font-size="9.00" fill="#222222">check_all_true</text>
</a>
</g>
</g>
<!-- check_term_true&#45;&gt;check_all_true -->
<g id="edge32" class="edge">
<title>check_term_true&#45;&gt;check_all_true</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M936.32,-494C951,-494 967.04,-494 981.71,-494"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="981.9,-496.1 987.9,-494 981.9,-491.9 981.9,-496.1"/>
</g>
<!-- gen_sound -->
<g id="node40" class="node">
<title>gen_sound</title>
<g id="a_node40"><a xlink:title="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-507" rx="35.59" ry="18"/>
<text text-anchor="middle" x="722.21" y="-504.8" font-family="Inter" font-size="9.00" fill="#222222">gen_sound</text>
</a>
</g>
</g>
<!-- gen_complete -->
<g id="node41" class="node">
<title>gen_complete</title>
<g id="a_node41"><a xlink:title="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-325" rx="43.76" ry="18"/>
<text text-anchor="middle" x="722.21" y="-322.8" font-family="Inter" font-size="9.00" fill="#222222">gen_complete</text>
</a>
</g>
</g>
<!-- zdecs_sound -->
<g id="node43" class="node">
<title>zdecs_sound</title>
<g id="a_node43"><a xlink:title="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-338" rx="40.98" ry="18"/>
<text text-anchor="middle" x="239.88" y="-335.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_sound</text>
</a>
</g>
</g>
<!-- zdecs_sound&#45;&gt;full_comp_aux -->
<g id="edge19" class="edge">
<title>zdecs_sound&#45;&gt;full_comp_aux</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M264.56,-323.56C278.24,-314.24 294.93,-301.06 306.27,-286 336.36,-246.05 314.37,-217.83 349.27,-182 354.3,-176.84 360.53,-172.63 367.03,-169.21"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="368.07,-171.04 372.54,-166.52 366.22,-167.27 368.07,-171.04"/>
</g>
<!-- root_steps_sound -->
<g id="node46" class="node">
<title>root_steps_sound</title>
<g id="a_node46"><a xlink:title="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-364" rx="51.27" ry="18"/>
<text text-anchor="middle" x="408.74" y="-361.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_sound</text>
</a>
</g>
</g>
<!-- zdecs_sound&#45;&gt;root_steps_sound -->
<g id="edge37" class="edge">
<title>zdecs_sound&#45;&gt;root_steps_sound</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M278.74,-343.9C301.34,-347.42 330.39,-351.95 355.19,-355.81"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="355.14,-357.93 361.4,-356.78 355.79,-353.78 355.14,-357.93"/>
</g>
<!-- zdecs_complete -->
<g id="node44" class="node">
<title>zdecs_complete</title>
<g id="a_node44"><a xlink:title="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-416" rx="49.15" ry="18"/>
<text text-anchor="middle" x="239.88" y="-413.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_complete</text>
</a>
</g>
</g>
<!-- root_steps_complete -->
<g id="node47" class="node">
<title>root_steps_complete</title>
<g id="a_node47"><a xlink:title="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-416" rx="59.43" ry="18"/>
<text text-anchor="middle" x="408.74" y="-413.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_complete</text>
</a>
</g>
</g>
<!-- zdecs_complete&#45;&gt;root_steps_complete -->
<g id="edge38" class="edge">
<title>zdecs_complete&#45;&gt;root_steps_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.14,-416C306,-416 325.21,-416 343.19,-416"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="343.23,-418.1 349.23,-416 343.23,-413.9 343.23,-418.1"/>
</g>
<!-- positions_at -->
<g id="node45" class="node">
<title>positions_at</title>
<g id="a_node45"><a xlink:title="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-520" rx="38.21" ry="18"/>
<text text-anchor="middle" x="408.74" y="-517.8" font-family="Inter" font-size="9.00" fill="#222222">positions_at</text>
</a>
</g>
</g>
<!-- steps_sound -->
<g id="node48" class="node">
<title>steps_sound</title>
<g id="a_node48"><a xlink:title="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-481" rx="39.02" ry="18"/>
<text text-anchor="middle" x="565.21" y="-478.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound</text>
</a>
</g>
</g>
<!-- positions_at&#45;&gt;steps_sound -->
<g id="edge39" class="edge">
<title>positions_at&#45;&gt;steps_sound</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M442.88,-511.63C466.76,-505.6 499.1,-497.44 524.39,-491.05"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="525.02,-493.06 530.32,-489.55 523.99,-488.99 525.02,-493.06"/>
</g>
<!-- root_steps_sound&#45;&gt;steps_sound -->
<g id="edge40" class="edge">
<title>root_steps_sound&#45;&gt;steps_sound</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M444.47,-377.11C452.54,-380.79 460.91,-385.13 468.21,-390 476.48,-395.52 517.51,-435.23 543.18,-460.34"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="542.02,-462.15 547.78,-464.85 544.96,-459.15 542.02,-462.15"/>
</g>
<!-- steps_complete -->
<g id="node55" class="node">
<title>steps_complete</title>
<g id="a_node55"><a xlink:title="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-318" rx="47.84" ry="18"/>
<text text-anchor="middle" x="565.21" y="-315.8" font-family="Inter" font-size="9.00" fill="#222222">steps_complete</text>
</a>
</g>
</g>
<!-- root_steps_complete&#45;&gt;steps_complete -->
<g id="edge46" class="edge">
<title>root_steps_complete&#45;&gt;steps_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M445.32,-401.71C453.03,-398.2 461.02,-394.22 468.21,-390 493.99,-374.86 521.03,-354.07 539.82,-338.72"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="541.6,-339.98 544.89,-334.54 538.93,-336.74 541.6,-339.98"/>
</g>
<!-- steps_sound&#45;&gt;gen_sound -->
<g id="edge33" class="edge">
<title>steps_sound&#45;&gt;gen_sound</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M602.55,-487.1C626.39,-491.09 657.54,-496.32 681.95,-500.42"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="681.74,-502.51 688,-501.43 682.43,-498.37 681.74,-502.51"/>
</g>
<!-- steps_sound_red1 -->
<g id="node49" class="node">
<title>steps_sound_red1</title>
<g id="a_node49"><a xlink:title="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-559" rx="51.92" ry="18"/>
<text text-anchor="middle" x="722.21" y="-556.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound_red1</text>
</a>
</g>
</g>
<!-- steps_sound&#45;&gt;steps_sound_red1 -->
<g id="edge41" class="edge">
<title>steps_sound&#45;&gt;steps_sound_red1</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M590.78,-495.03C610.01,-505.83 637.53,-520.9 662.21,-533 668.8,-536.23 675.89,-539.52 682.79,-542.61"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="682.19,-544.64 688.53,-545.17 683.9,-540.81 682.19,-544.64"/>
</g>
<!-- has_red_spec -->
<g id="node57" class="node">
<title>has_red_spec</title>
<g id="a_node57"><a xlink:title="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-403" rx="42.95" ry="18"/>
<text text-anchor="middle" x="722.21" y="-400.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_spec</text>
</a>
</g>
</g>
<!-- steps_sound&#45;&gt;has_red_spec -->
<g id="edge50" class="edge">
<title>steps_sound&#45;&gt;has_red_spec</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M590.78,-466.97C610.01,-456.17 637.53,-441.1 662.21,-429 669.65,-425.35 677.74,-421.63 685.46,-418.2"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="686.64,-419.97 691.28,-415.63 684.94,-416.13 686.64,-419.97"/>
</g>
<!-- corpus_sound -->
<g id="node79" class="node">
<title>corpus_sound</title>
<g id="a_node79"><a xlink:title="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-455" rx="43.1" ry="18"/>
<text text-anchor="middle" x="722.21" y="-452.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_sound</text>
</a>
</g>
</g>
<!-- steps_sound&#45;&gt;corpus_sound -->
<g id="edge59" class="edge">
<title>steps_sound&#45;&gt;corpus_sound</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M602.55,-474.9C624.4,-471.24 652.39,-466.54 675.7,-462.63"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="676.26,-464.67 681.83,-461.6 675.57,-460.53 676.26,-464.67"/>
</g>
<!-- steps_sound_red1&#45;&gt;check_term_true -->
<g id="edge31" class="edge">
<title>steps_sound_red1&#45;&gt;check_term_true</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M756.97,-545.37C782.8,-534.95 818.46,-520.56 845.46,-509.66"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="846.31,-511.58 851.09,-507.39 844.74,-507.68 846.31,-511.58"/>
</g>
<!-- steps_sound_red1&#45;&gt;gen_fv_preserved -->
<g id="edge36" class="edge">
<title>steps_sound_red1&#45;&gt;gen_fv_preserved</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M774.6,-559C791.08,-559 809.44,-559 826.35,-559"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="826.51,-561.1 832.51,-559 826.51,-556.9 826.51,-561.1"/>
</g>
<!-- steps_sound_red1&#45;&gt;corpus_fv_preserved -->
<g id="edge63" class="edge">
<title>steps_sound_red1&#45;&gt;corpus_fv_preserved</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M760.96,-571.19C783.94,-578.61 813.47,-588.15 837.87,-596.02"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="837.27,-598.04 843.63,-597.88 838.56,-594.04 837.27,-598.04"/>
</g>
<!-- positions_hole -->
<g id="node50" class="node">
<title>positions_hole</title>
<g id="a_node50"><a xlink:title="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-468" rx="44.41" ry="18"/>
<text text-anchor="middle" x="239.88" y="-465.8" font-family="Inter" font-size="9.00" fill="#222222">positions_hole</text>
</a>
</g>
</g>
<!-- root_steps_in_steps -->
<g id="node51" class="node">
<title>root_steps_in_steps</title>
<g id="a_node51"><a xlink:title="root_steps_in_steps theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-468" rx="56.66" ry="18"/>
<text text-anchor="middle" x="408.74" y="-465.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_in_steps</text>
</a>
</g>
</g>
<!-- positions_hole&#45;&gt;root_steps_in_steps -->
<g id="edge42" class="edge">
<title>positions_hole&#45;&gt;root_steps_in_steps</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.72,-468C303.36,-468 325.43,-468 345.69,-468"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="345.92,-470.1 351.92,-468 345.92,-465.9 345.92,-470.1"/>
</g>
<!-- root_steps_in_steps&#45;&gt;steps_complete -->
<g id="edge47" class="edge">
<title>root_steps_in_steps&#45;&gt;steps_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M447.78,-454.87C455.01,-451.36 462.19,-447.1 468.21,-442 494.65,-419.62 490.02,-404.4 511.21,-377 521.23,-364.04 533.38,-350.38 543.53,-339.47"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="545.17,-340.79 547.74,-334.97 542.1,-337.92 545.17,-340.79"/>
</g>
<!-- plug_comp -->
<g id="node52" class="node">
<title>plug_comp</title>
<g id="a_node52"><a xlink:title="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-208" rx="35.59" ry="18"/>
<text text-anchor="middle" x="408.74" y="-205.8" font-family="Inter" font-size="9.00" fill="#222222">plug_comp</text>
</a>
</g>
</g>
<!-- plug_comp&#45;&gt;steps_complete -->
<g id="edge44" class="edge">
<title>plug_comp&#45;&gt;steps_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M437.98,-218.53C447.88,-222.74 458.85,-228.02 468.21,-234 496.59,-252.14 525.14,-278.38 543.63,-296.69"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="542.38,-298.41 548.11,-301.16 545.35,-295.44 542.38,-298.41"/>
</g>
<!-- positions_comp -->
<g id="node53" class="node">
<title>positions_comp</title>
<g id="a_node53"><a xlink:title="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-312" rx="47.19" ry="18"/>
<text text-anchor="middle" x="408.74" y="-309.8" font-family="Inter" font-size="9.00" fill="#222222">positions_comp</text>
</a>
</g>
</g>
<!-- positions_comp&#45;&gt;steps_complete -->
<g id="edge45" class="edge">
<title>positions_comp&#45;&gt;steps_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M456.08,-313.8C473.49,-314.48 493.4,-315.25 511.35,-315.95"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="511.28,-318.05 517.36,-316.18 511.45,-313.85 511.28,-318.05"/>
</g>
<!-- at_ctx_comp -->
<g id="node54" class="node">
<title>at_ctx_comp</title>
<g id="a_node54"><a xlink:title="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-260" rx="40.33" ry="18"/>
<text text-anchor="middle" x="408.74" y="-257.8" font-family="Inter" font-size="9.00" fill="#222222">at_ctx_comp</text>
</a>
</g>
</g>
<!-- at_ctx_comp&#45;&gt;steps_complete -->
<g id="edge43" class="edge">
<title>at_ctx_comp&#45;&gt;steps_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M440.26,-271.46C464.53,-280.57 498.67,-293.39 524.98,-303.27"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="524.45,-305.32 530.81,-305.46 525.93,-301.38 524.45,-305.32"/>
</g>
<!-- steps_complete&#45;&gt;gen_complete -->
<g id="edge34" class="edge">
<title>steps_complete&#45;&gt;gen_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M613.13,-320.12C631.78,-320.96 653.25,-321.93 672.11,-322.78"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="672.31,-324.89 678.4,-323.07 672.5,-320.7 672.31,-324.89"/>
</g>
<!-- steps_complete&#45;&gt;has_red_spec -->
<g id="edge49" class="edge">
<title>steps_complete&#45;&gt;has_red_spec</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M593.2,-332.81C620.2,-347.61 661.68,-370.36 690.05,-385.92"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="689.27,-387.88 695.55,-388.93 691.29,-384.2 689.27,-387.88"/>
</g>
<!-- corpus_complete -->
<g id="node80" class="node">
<title>corpus_complete</title>
<g id="a_node80"><a xlink:title="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-273" rx="51.27" ry="18"/>
<text text-anchor="middle" x="722.21" y="-270.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_complete</text>
</a>
</g>
</g>
<!-- steps_complete&#45;&gt;corpus_complete -->
<g id="edge60" class="edge">
<title>steps_complete&#45;&gt;corpus_complete</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M603.73,-307.11C625.52,-300.78 653.13,-292.77 676.1,-286.1"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="676.96,-288.03 682.14,-284.34 675.79,-284 676.96,-288.03"/>
</g>
<!-- has_red_f -->
<g id="node56" class="node">
<title>has_red_f</title>
<g id="a_node56"><a xlink:title="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-403" rx="32.16" ry="18"/>
<text text-anchor="middle" x="565.21" y="-400.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_f</text>
</a>
</g>
</g>
<!-- has_red_f&#45;&gt;has_red_spec -->
<g id="edge48" class="edge">
<title>has_red_f&#45;&gt;has_red_spec</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M597.57,-403C619.26,-403 648.54,-403 673.15,-403"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="673.31,-405.1 679.31,-403 673.31,-400.9 673.31,-405.1"/>
</g>
<!-- has_red_spec&#45;&gt;check_term_true -->
<g id="edge30" class="edge">
<title>has_red_spec&#45;&gt;check_term_true</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M753.64,-415.36C762.95,-419.42 773.12,-424.14 782.21,-429 796.39,-436.58 830.11,-458.35 854.92,-474.62"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="853.9,-476.46 860.07,-478 856.21,-472.95 853.9,-476.46"/>
</g>
<!-- red1_dec -->
<g id="node58" class="node">
<title>red1_dec</title>
<g id="a_node58"><a xlink:title="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-429" rx="30.7" ry="18"/>
<text text-anchor="middle" x="885.25" y="-426.8" font-family="Inter" font-size="9.00" fill="#222222">red1_dec</text>
</a>
</g>
</g>
<!-- has_red_spec&#45;&gt;red1_dec -->
<g id="edge51" class="edge">
<title>has_red_spec&#45;&gt;red1_dec</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M762.6,-409.36C789.24,-413.66 824.09,-419.29 849.65,-423.41"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="849.36,-425.49 855.61,-424.38 850.03,-421.35 849.36,-425.49"/>
</g>
<!-- corpus_decides -->
<g id="node81" class="node">
<title>corpus_decides</title>
<g id="a_node81"><a xlink:title="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-377" rx="47.84" ry="18"/>
<text text-anchor="middle" x="885.25" y="-374.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_decides</text>
</a>
</g>
</g>
<!-- has_red_spec&#45;&gt;corpus_decides -->
<g id="edge61" class="edge">
<title>has_red_spec&#45;&gt;corpus_decides</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M762.6,-396.64C784.4,-393.12 811.69,-388.71 834.9,-384.97"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="835.43,-387.01 841.02,-383.98 834.76,-382.86 835.43,-387.01"/>
</g>
<!-- open_rec_app -->
<g id="node59" class="node">
<title>open_rec_app</title>
<g id="a_node59"><a xlink:title="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1144" rx="43.1" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1141.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_app</text>
</a>
</g>
</g>
<!-- open_rec_lam -->
<g id="node60" class="node">
<title>open_rec_lam</title>
<g id="a_node60"><a xlink:title="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1196" rx="43.76" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1193.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lam</text>
</a>
</g>
</g>
<!-- open_rec_esub -->
<g id="node61" class="node">
<title>open_rec_esub</title>
<g id="a_node61"><a xlink:title="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1248" rx="46.38" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1245.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_esub</text>
</a>
</g>
</g>
<!-- close_rec_app -->
<g id="node62" class="node">
<title>close_rec_app</title>
<g id="a_node62"><a xlink:title="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1300" rx="44.41" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1297.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_app</text>
</a>
</g>
</g>
<!-- close_rec_lam -->
<g id="node63" class="node">
<title>close_rec_lam</title>
<g id="a_node63"><a xlink:title="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1352" rx="44.41" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1349.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_lam</text>
</a>
</g>
</g>
<!-- close_rec_esub -->
<g id="node64" class="node">
<title>close_rec_esub</title>
<g id="a_node64"><a xlink:title="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1404" rx="46.53" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1401.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_esub</text>
</a>
</g>
</g>
<!-- subst_app -->
<g id="node65" class="node">
<title>subst_app</title>
<g id="a_node65"><a xlink:title="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1456" rx="34.13" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1453.8" font-family="Inter" font-size="9.00" fill="#222222">subst_app</text>
</a>
</g>
</g>
<!-- subst_lam -->
<g id="node66" class="node">
<title>subst_lam</title>
<g id="a_node66"><a xlink:title="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1508" rx="34.13" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1505.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lam</text>
</a>
</g>
</g>
<!-- subst_esub -->
<g id="node67" class="node">
<title>subst_esub</title>
<g id="a_node67"><a xlink:title="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1560" rx="36.25" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1557.8" font-family="Inter" font-size="9.00" fill="#222222">subst_esub</text>
</a>
</g>
</g>
<!-- red_sub_root_to_red1 -->
<g id="node71" class="node">
<title>red_sub_root_to_red1</title>
<g id="a_node71"><a xlink:title="red_sub_root_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1612" rx="60.09" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1609.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_root_to_red1</text>
</a>
</g>
</g>
<!-- red_sub_to_red1 -->
<g id="node72" class="node">
<title>red_sub_to_red1</title>
<g id="a_node72"><a xlink:title="red_sub_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1612" rx="47.84" ry="18"/>
<text text-anchor="middle" x="239.88" y="-1609.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_to_red1</text>
</a>
</g>
</g>
<!-- red_sub_root_to_red1&#45;&gt;red_sub_to_red1 -->
<g id="edge56" class="edge">
<title>red_sub_root_to_red1&#45;&gt;red_sub_to_red1</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M125.65,-1612C145.11,-1612 166.58,-1612 185.56,-1612"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.89,-1614.1 191.89,-1612 185.89,-1609.9 185.89,-1614.1"/>
</g>
<!-- red_sub_context -->
<g id="node73" class="node">
<title>red_sub_context</title>
<g id="a_node73"><a xlink:title="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1664" rx="49.15" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1661.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_context</text>
</a>
</g>
</g>
<!-- red_sub_gc -->
<g id="node74" class="node">
<title>red_sub_gc</title>
<g id="a_node74"><a xlink:title="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1716" rx="36.25" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1713.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_gc</text>
</a>
</g>
</g>
<!-- red_sub_r -->
<g id="node75" class="node">
<title>red_sub_r</title>
<g id="a_node75"><a xlink:title="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1768" rx="32.82" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1765.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_r</text>
</a>
</g>
</g>
<!-- occurs_zfill -->
<g id="node76" class="node">
<title>occurs_zfill</title>
<g id="a_node76"><a xlink:title="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1820" rx="37.56" ry="18"/>
<text text-anchor="middle" x="65.24" y="-1817.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_zfill</text>
</a>
</g>
</g>
<!-- zfill_occurs0 -->
<g id="node77" class="node">
<title>zfill_occurs0</title>
<g id="a_node77"><a xlink:title="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1820" rx="40.98" ry="18"/>
<text text-anchor="middle" x="239.88" y="-1817.8" font-family="Inter" font-size="9.00" fill="#222222">zfill_occurs0</text>
</a>
</g>
</g>
<!-- occurs_zfill&#45;&gt;zfill_occurs0 -->
<g id="edge57" class="edge">
<title>occurs_zfill&#45;&gt;zfill_occurs0</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-1820C128.98,-1820 164.34,-1820 192.45,-1820"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.7,-1822.1 198.7,-1820 192.7,-1817.9 192.7,-1822.1"/>
</g>
<!-- R_Gc_disjoint -->
<g id="node78" class="node">
<title>R_Gc_disjoint</title>
<g id="a_node78"><a xlink:title="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-1820" rx="41.64" ry="18"/>
<text text-anchor="middle" x="408.74" y="-1817.8" font-family="Inter" font-size="9.00" fill="#222222">R_Gc_disjoint</text>
</a>
</g>
</g>
<!-- zfill_occurs0&#45;&gt;R_Gc_disjoint -->
<g id="edge58" class="edge">
<title>zfill_occurs0&#45;&gt;R_Gc_disjoint</title>
<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-1820C305.28,-1820 335.83,-1820 360.89,-1820"/>
<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.14,-1822.1 367.14,-1820 361.14,-1817.9 361.14,-1822.1"/>
</g>
</g>
</svg>