digraph theorem_deps {
  rankdir=LR;
  bgcolor="white";
  splines=spline;
  nodesep=0.22;
  ranksep=0.6;
  node [fontname=Inter, fontsize=9, fontcolor="#222222"];
  edge [fontname=Inter, fontsize=8, color="#9a9a9a", arrowsize=0.6, penwidth=0.8];
  graph [fontname=Inter, fontsize=12, labelloc=t, label=<<B>Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M2)</B><BR/><FONT POINT-SIZE="9"><FONT COLOR="#38761d">proved</FONT>   <FONT COLOR="#b45f06">stated</FONT>   <FONT COLOR="#777777">planned</FONT>   <FONT COLOR="#cc0000">blocked</FONT></FONT>>];
  fvs_lift [label="fvs_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="fvs_lift theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  lift_lc [label="lift_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  lift_0_lc [label="lift_0_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_0_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  open_rec_bvar [label="open_rec_bvar", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_bvar theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  close_rec_fvar [label="close_rec_fvar", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_fvar theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  open_rec_occurs_false [label="open_rec_occurs_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_occurs_false theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  close_rec_notin [label="close_rec_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_notin theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  close_rec_fvs [label="close_rec_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  open_rec_bvar_neq [label="open_rec_bvar_neq", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_bvar_neq theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  open_rec_fvs [label="open_rec_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  open_close [label="open_close", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_close theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  subst_fvar_self [label="subst_fvar_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_self theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  subst_fvar_other [label="subst_fvar_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_other theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  subst_fvs [label="subst_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  Plus_red1_context [label="Plus_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  occurs_count_zero [label="occurs_count_zero", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  occurs_count_false [label="occurs_count_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  occurs_count_pos [label="occurs_count_pos", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_pos theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  occurs_lift_self [label="occurs_lift_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_lift_self theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  zdecs_nonempty [label="zdecs_nonempty", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_nonempty theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  occurs_count_zfill_plug [label="occurs_count_zfill_plug", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zfill_plug theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  open_rec_zplug_lift [label="open_rec_zplug_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  full_comp_aux [label="full_comp_aux", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="full_comp_aux theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  lemma_2_2_full_comp [label="lemma_2_2_full_comp", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
  fvs_zplug_lift [label="fvs_zplug_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="fvs_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  plug_fv_mono [label="plug_fv_mono", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plug_fv_mono theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  red1_root_fv [label="red1_root_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_root_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  red1r_fv [label="red1r_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  lemma_2_1_fv_preserved [label="lemma_2_1_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
  lemma_2_3_beta_sim [label="lemma_2_3_beta_sim", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
  zdecs_sound [label="zdecs_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  zdecs_complete [label="zdecs_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  positions_at [label="positions_at", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  root_steps_sound [label="root_steps_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  root_steps_complete [label="root_steps_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  steps_sound [label="steps_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  steps_sound_red1 [label="steps_sound_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  positions_hole [label="positions_hole", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  root_steps_in_steps [label="root_steps_in_steps", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_in_steps theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  plug_comp [label="plug_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  positions_comp [label="positions_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  at_ctx_comp [label="at_ctx_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  steps_complete [label="steps_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  has_red_f [label="has_red_f", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  has_red_spec [label="has_red_spec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  red1_dec [label="red1_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  corpus_sound [label="corpus_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  corpus_complete [label="corpus_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  corpus_decides [label="corpus_decides", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  corpus_fv_preserved [label="corpus_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
  lift_lc -> lift_0_lc;
  fvs_lift -> open_rec_fvs;
  open_rec_bvar -> open_rec_fvs;
  open_rec_bvar_neq -> open_rec_fvs;
  open_rec_bvar -> open_close;
  lift_0_lc -> subst_fvar_self;
  close_rec_fvs -> subst_fvs;
  open_rec_fvs -> subst_fvs;
  occurs_count_zero -> occurs_count_pos;
  occurs_count_false -> occurs_count_zfill_plug;
  occurs_lift_self -> occurs_count_zfill_plug;
  occurs_lift_self -> open_rec_zplug_lift;
  open_rec_occurs_false -> open_rec_zplug_lift;
  occurs_count_zero -> full_comp_aux;
  occurs_count_zfill_plug -> full_comp_aux;
  open_rec_occurs_false -> full_comp_aux;
  open_rec_zplug_lift -> full_comp_aux;
  zdecs_nonempty -> full_comp_aux;
  zdecs_sound -> full_comp_aux;
  full_comp_aux -> lemma_2_2_full_comp;
  fvs_lift -> fvs_zplug_lift;
  fvs_zplug_lift -> red1_root_fv;
  plug_fv_mono -> red1r_fv;
  red1_root_fv -> red1r_fv;
  red1r_fv -> lemma_2_1_fv_preserved;
  Plus_red1_context -> lemma_2_3_beta_sim;
  lemma_2_2_full_comp -> lemma_2_3_beta_sim;
  zdecs_sound -> root_steps_sound;
  zdecs_complete -> root_steps_complete;
  positions_at -> steps_sound;
  root_steps_sound -> steps_sound;
  steps_sound -> steps_sound_red1;
  positions_hole -> root_steps_in_steps;
  at_ctx_comp -> steps_complete;
  plug_comp -> steps_complete;
  positions_comp -> steps_complete;
  root_steps_complete -> steps_complete;
  root_steps_in_steps -> steps_complete;
  has_red_f -> has_red_spec;
  steps_complete -> has_red_spec;
  steps_sound -> has_red_spec;
  has_red_spec -> red1_dec;
  steps_sound -> corpus_sound;
  steps_complete -> corpus_complete;
  has_red_spec -> corpus_decides;
  lemma_2_1_fv_preserved -> corpus_fv_preserved;
  steps_sound_red1 -> corpus_fv_preserved;
}