263 lines
34 KiB
Plaintext
263 lines
34 KiB
Plaintext
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 (M4)</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];
|
|
Star_trans [label="Star_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_trans theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red1_star [label="red1_star", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_star theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Plus_to_Star [label="Plus_to_Star", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_to_Star theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Star_red1_context [label="Star_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_red1_context theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
star_one_trans [label="star_one_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="star_one_trans theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
in_comb [label="in_comb", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="in_comb theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
pow2_pos [label="pow2_pos", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="pow2_pos theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
size_all_terms [label="size_all_terms", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="size_all_terms theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
enumerate_check [label="enumerate_check", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_check theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
enumerate_sound [label="enumerate_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_sound theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
enumerate_complete [label="enumerate_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_complete theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_fvs [label="of_trm_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_fvs theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_lift [label="of_trm_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_lift theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_open [label="of_trm_open", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_open theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_close [label="of_trm_close", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_close theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_injective [label="of_trm_injective", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_injective theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mfvs_lift_m [label="mfvs_lift_m", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mfvs_lift_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mfvs_close_m [label="mfvs_close_m", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mfvs_close_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mfvs_open_m [label="mfvs_open_m", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mfvs_open_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_plug [label="of_trm_plug", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_plug theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_of_red1 [label="mred_of_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_of_red1 theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_context [label="mred_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_context theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_term_context [label="mred_term_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_term_context theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_moccurs [label="of_trm_moccurs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_moccurs theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
of_trm_moccurs0 [label="of_trm_moccurs0", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_moccurs0 theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_B_intro [label="mred_B_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_B_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_gc_intro [label="mred_gc_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_gc_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_r_intro [label="mred_r_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_r_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Plus_mred_of_Plus_red1 [label="Plus_mred_of_Plus_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_mred_of_Plus_red1 theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_full_comp_pure [label="mred_full_comp_pure", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_full_comp_pure theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
mred_plus_one [label="mred_plus_one", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_plus_one theory/Metaterm.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];
|
|
Plus_trans [label="Plus_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Plus_step_trans [label="Plus_step_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_step_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
isubst_meta_in [label="isubst_meta_in", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="isubst_meta_in theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
isubst_meta_notin [label="isubst_meta_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="isubst_meta_notin theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
eqC_in_Es [label="eqC_in_Es", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="eqC_in_Es theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Es_ctx_any [label="Es_ctx_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_ctx_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
nred_R_intro [label="nred_R_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_R_intro theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Es_refl_any [label="Es_refl_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_refl_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Es_sym_any [label="Es_sym_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_sym_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Es_trans_any [label="Es_trans_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_trans_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
in_filter_neq [label="in_filter_neq", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="in_filter_neq theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
filter_neq_in [label="filter_neq_in", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="filter_neq_in theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
nplug_fv_mono [label="nplug_fv_mono", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nplug_fv_mono theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
nplug_fv_upper [label="nplug_fv_upper", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nplug_fv_upper theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
nred_core_fv [label="nred_core_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_core_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
nplug_esub_fv [label="nplug_esub_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nplug_esub_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
nred_fv [label="nred_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
par_red1_iff [label="par_red1_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red1_in_par [label="red1_in_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
par_context [label="par_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
par_to_red1_or_eq [label="par_to_red1_or_eq", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_to_red1_or_eq theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red1_or_eq_to_par [label="red1_or_eq_to_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_or_eq_to_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
par_reflexive [label="par_reflexive", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
gen_list_length [label="gen_list_length", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
check_term_true [label="check_term_true", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
check_all_true [label="check_all_true", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
gen_sound [label="gen_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
gen_complete [label="gen_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
gen_fv_preserved [label="gen_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
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];
|
|
nf_iff_steps_nil [label="nf_iff_steps_nil", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nf_iff_steps_nil theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
normal_form_iff_nf [label="normal_form_iff_nf", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="normal_form_iff_nf theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
nf_dec [label="nf_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nf_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
open_rec_app [label="open_rec_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
open_rec_lam [label="open_rec_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
open_rec_esub [label="open_rec_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
close_rec_app [label="close_rec_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
close_rec_lam [label="close_rec_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
close_rec_esub [label="close_rec_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
subst_app [label="subst_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
subst_lam [label="subst_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
subst_esub [label="subst_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
subst_notin [label="subst_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
subst_lc_self [label="subst_lc_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
subst_other [label="subst_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
open_rec_lc_atom [label="open_rec_lc_atom", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lc_atom theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
open_rec_lc [label="open_rec_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lc theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_sub_root_to_red1 [label="red_sub_root_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_root_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_sub_to_red1 [label="red_sub_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_sub_context [label="red_sub_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_sub_gc [label="red_sub_gc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_sub_r [label="red_sub_r", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
occurs_zfill [label="occurs_zfill", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
zfill_occurs0 [label="zfill_occurs0", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
R_Gc_disjoint [label="R_Gc_disjoint", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
Star_red_sub_context [label="Star_red_sub_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
full_comp_aux_sub [label="full_comp_aux_sub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="full_comp_aux_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
plus_red_sub_full_comp [label="plus_red_sub_full_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plus_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
star_red_sub_full_comp [label="star_red_sub_full_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="star_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
es_count_plug_mono [label="es_count_plug_mono", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="es_count_plug_mono theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_gc_measure [label="red_gc_measure", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_measure theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_gc_terminates [label="red_gc_terminates", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_terminates theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
|
red_gc_to_red_sub [label="red_gc_to_red_sub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_to_red_sub theory/Subsystem.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;
|
|
in_comb -> size_all_terms;
|
|
pow2_pos -> size_all_terms;
|
|
check_all_true -> enumerate_check;
|
|
steps_sound -> enumerate_sound;
|
|
steps_complete -> enumerate_complete;
|
|
of_trm_lift -> of_trm_open;
|
|
mfvs_lift_m -> mfvs_open_m;
|
|
of_trm_plug -> mred_term_context;
|
|
of_trm_moccurs -> of_trm_moccurs0;
|
|
Plus_mred_of_Plus_red1 -> mred_full_comp_pure;
|
|
lemma_2_2_full_comp -> mred_full_comp_pure;
|
|
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;
|
|
filter_neq_in -> nplug_fv_mono;
|
|
in_filter_neq -> nplug_fv_mono;
|
|
filter_neq_in -> nplug_fv_upper;
|
|
in_filter_neq -> nplug_fv_upper;
|
|
filter_neq_in -> nred_core_fv;
|
|
in_filter_neq -> nred_core_fv;
|
|
nplug_fv_mono -> nred_core_fv;
|
|
nplug_fv_upper -> nred_core_fv;
|
|
filter_neq_in -> nplug_esub_fv;
|
|
in_filter_neq -> nplug_esub_fv;
|
|
filter_neq_in -> nred_fv;
|
|
in_filter_neq -> nred_fv;
|
|
nplug_esub_fv -> nred_fv;
|
|
nplug_fv_mono -> nred_fv;
|
|
nplug_fv_upper -> nred_fv;
|
|
par_red1_iff -> par_to_red1_or_eq;
|
|
par_red1_iff -> red1_or_eq_to_par;
|
|
has_red_spec -> check_term_true;
|
|
steps_sound_red1 -> check_term_true;
|
|
check_term_true -> check_all_true;
|
|
steps_sound -> gen_sound;
|
|
steps_complete -> gen_complete;
|
|
lemma_2_1_fv_preserved -> gen_fv_preserved;
|
|
steps_sound_red1 -> gen_fv_preserved;
|
|
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_complete -> nf_iff_steps_nil;
|
|
steps_sound_red1 -> nf_iff_steps_nil;
|
|
nf_iff_steps_nil -> normal_form_iff_nf;
|
|
nf_iff_steps_nil -> nf_dec;
|
|
close_rec_notin -> subst_notin;
|
|
open_rec_occurs_false -> subst_notin;
|
|
subst_fvar_self -> subst_lc_self;
|
|
subst_fvar_other -> subst_other;
|
|
open_rec_lc_atom -> open_rec_lc;
|
|
red_sub_root_to_red1 -> red_sub_to_red1;
|
|
occurs_zfill -> zfill_occurs0;
|
|
zfill_occurs0 -> R_Gc_disjoint;
|
|
red_sub_context -> Star_red_sub_context;
|
|
occurs_count_zero -> full_comp_aux_sub;
|
|
occurs_count_zfill_plug -> full_comp_aux_sub;
|
|
open_rec_occurs_false -> full_comp_aux_sub;
|
|
open_rec_zplug_lift -> full_comp_aux_sub;
|
|
red_sub_gc -> full_comp_aux_sub;
|
|
red_sub_r -> full_comp_aux_sub;
|
|
zdecs_nonempty -> full_comp_aux_sub;
|
|
zdecs_sound -> full_comp_aux_sub;
|
|
full_comp_aux_sub -> plus_red_sub_full_comp;
|
|
Plus_to_Star -> star_red_sub_full_comp;
|
|
plus_red_sub_full_comp -> star_red_sub_full_comp;
|
|
es_count_plug_mono -> red_gc_measure;
|
|
red_gc_measure -> red_gc_terminates;
|
|
red_sub_gc -> red_gc_to_red_sub;
|
|
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;
|
|
}
|