diff --git a/README.md b/README.md
index 408c869..84ec1cd 100644
--- a/README.md
+++ b/README.md
@@ -2,14 +2,36 @@ This was (mostly) me being bored in a Monday evening and in an attempt to formal
## Graphs
-The dependency graph covers the six milestones and every edge runs from a dependency to the result that uses it while the node colour encodes the status proved or stated or planned or blocked:
+The dependency graphs are drawn in black and white and split by milestone. Every edge runs from a dependency to the result that uses it. A box is a result named after a paper statement, an ellipse is a supporting result, and a dashed box labelled with a milestone is a result defined in another diagram. The overview gives the shape of the whole development:
-
+
+
+The details are then one diagram per milestone:
+
+### M1, binding and reduction
+
+
+
+### M2, metatheory and checks
+
+
+
+### M3, subsystem
+
+
+
+### M4, parallel reduction
+
+
+
+### M5, metaterms and the named calculus
+
+
The rule sketch gives the transition system generated by the rules B and Gc and R:
-
+
The reduction graph gives the bounded reduct set of the term that applies the duplicating identity to a variable with every edge labelled by its rule and with the normal form marked:
-
+
diff --git a/graphs/dependency-M1.dot b/graphs/dependency-M1.dot
new file mode 100644
index 0000000..226b1e9
--- /dev/null
+++ b/graphs/dependency-M1.dot
@@ -0,0 +1,71 @@
+digraph deps {
+ rankdir=LR;
+ bgcolor="#ffffff";
+ splines=polyline;
+ concentrate=true;
+ nodesep=0.2;
+ ranksep=0.9;
+ node [fontname=Inter, fontsize=9];
+ edge [fontname=Inter, fontsize=8, color="#000000", fontcolor="#000000", arrowsize=0.6, penwidth=0.8];
+ graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="#000000", label=<Theorem dependencies M1, 33 results >];
+ close_rec_fvar [label="close_rec_fvar", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_fvar theory/Binding.v proved"];
+ close_rec_fvs [label="close_rec_fvs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_fvs theory/Binding.v proved"];
+ close_rec_notin [label="close_rec_notin", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_notin theory/Binding.v proved"];
+ fvs_lift [label="fvs_lift", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="fvs_lift theory/Binding.v proved"];
+ lift_0_lc [label="lift_0_lc", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="lift_0_lc theory/Binding.v proved"];
+ lift_lc [label="lift_lc", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="lift_lc theory/Binding.v proved"];
+ open_close [label="open_close", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_close theory/Binding.v proved"];
+ open_rec_bvar [label="open_rec_bvar", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_bvar theory/Binding.v proved"];
+ open_rec_bvar_neq [label="open_rec_bvar_neq", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_bvar_neq theory/Binding.v proved"];
+ open_rec_fvs [label="open_rec_fvs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_fvs theory/Binding.v proved"];
+ open_rec_occurs_false [label="open_rec_occurs_false", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_occurs_false theory/Binding.v proved"];
+ subst_fvar_other [label="subst_fvar_other", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_fvar_other theory/Binding.v proved"];
+ subst_fvar_self [label="subst_fvar_self", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_fvar_self theory/Binding.v proved"];
+ subst_fvs [label="subst_fvs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_fvs theory/Binding.v proved"];
+ at_ctx_comp [label="at_ctx_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="at_ctx_comp theory/Reduction.v proved"];
+ has_red_f [label="has_red_f", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="has_red_f theory/Reduction.v proved"];
+ has_red_spec [label="has_red_spec", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="has_red_spec theory/Reduction.v proved"];
+ nf_dec [label="nf_dec", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nf_dec theory/Reduction.v proved"];
+ nf_iff_steps_nil [label="nf_iff_steps_nil", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nf_iff_steps_nil theory/Reduction.v proved"];
+ normal_form_iff_nf [label="normal_form_iff_nf", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="normal_form_iff_nf theory/Reduction.v proved"];
+ plug_comp [label="plug_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="plug_comp theory/Reduction.v proved"];
+ positions_at [label="positions_at", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="positions_at theory/Reduction.v proved"];
+ positions_comp [label="positions_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="positions_comp theory/Reduction.v proved"];
+ positions_hole [label="positions_hole", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="positions_hole theory/Reduction.v proved"];
+ red1_dec [label="red1_dec", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red1_dec theory/Reduction.v proved"];
+ root_steps_complete [label="root_steps_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="root_steps_complete theory/Reduction.v proved"];
+ root_steps_in_steps [label="root_steps_in_steps", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="root_steps_in_steps theory/Reduction.v proved"];
+ root_steps_sound [label="root_steps_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="root_steps_sound theory/Reduction.v proved"];
+ steps_complete [label="steps_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="steps_complete theory/Reduction.v proved"];
+ steps_sound [label="steps_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="steps_sound theory/Reduction.v proved"];
+ steps_sound_red1 [label="steps_sound_red1", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="steps_sound_red1 theory/Reduction.v proved"];
+ zdecs_complete [label="zdecs_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="zdecs_complete theory/Reduction.v proved"];
+ zdecs_sound [label="zdecs_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="zdecs_sound theory/Reduction.v proved"];
+ 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;
+ 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;
+}
diff --git a/graphs/dependency-M1.png b/graphs/dependency-M1.png
new file mode 100644
index 0000000..2decc03
Binary files /dev/null and b/graphs/dependency-M1.png differ
diff --git a/graphs/dependency-M1.svg b/graphs/dependency-M1.svg
new file mode 100644
index 0000000..8db0f72
--- /dev/null
+++ b/graphs/dependency-M1.svg
@@ -0,0 +1,473 @@
+
+
+
+
+
+
+deps
+Theorem dependencies M1, 33 results
+
+
+close_rec_fvar
+
+close_rec_fvar
+
+
+
+
+close_rec_fvs
+
+close_rec_fvs
+
+
+
+
+subst_fvs
+
+subst_fvs
+
+
+
+
+close_rec_fvs->subst_fvs
+
+
+
+close_rec_notin
+
+close_rec_notin
+
+
+
+
+fvs_lift
+
+fvs_lift
+
+
+
+
+open_rec_fvs
+
+open_rec_fvs
+
+
+
+
+fvs_lift->open_rec_fvs
+
+
+
+lift_0_lc
+
+lift_0_lc
+
+
+
+
+subst_fvar_self
+
+subst_fvar_self
+
+
+
+
+lift_0_lc->subst_fvar_self
+
+
+
+lift_lc
+
+lift_lc
+
+
+
+
+lift_lc->lift_0_lc
+
+
+
+open_close
+
+open_close
+
+
+
+
+open_rec_bvar
+
+open_rec_bvar
+
+
+
+
+open_rec_bvar->open_close
+
+
+
+open_rec_bvar->open_rec_fvs
+
+
+
+open_rec_bvar_neq
+
+open_rec_bvar_neq
+
+
+
+
+open_rec_bvar_neq->open_rec_fvs
+
+
+
+open_rec_fvs->subst_fvs
+
+
+
+open_rec_occurs_false
+
+open_rec_occurs_false
+
+
+
+
+subst_fvar_other
+
+subst_fvar_other
+
+
+
+
+at_ctx_comp
+
+at_ctx_comp
+
+
+
+
+steps_complete
+
+steps_complete
+
+
+
+
+at_ctx_comp->steps_complete
+
+
+
+has_red_f
+
+has_red_f
+
+
+
+
+has_red_spec
+
+has_red_spec
+
+
+
+
+has_red_f->has_red_spec
+
+
+
+red1_dec
+
+red1_dec
+
+
+
+
+has_red_spec->red1_dec
+
+
+
+nf_dec
+
+nf_dec
+
+
+
+
+nf_iff_steps_nil
+
+nf_iff_steps_nil
+
+
+
+
+nf_iff_steps_nil->nf_dec
+
+
+
+normal_form_iff_nf
+
+normal_form_iff_nf
+
+
+
+
+nf_iff_steps_nil->normal_form_iff_nf
+
+
+
+plug_comp
+
+plug_comp
+
+
+
+
+plug_comp->steps_complete
+
+
+
+positions_at
+
+positions_at
+
+
+
+
+steps_sound
+
+steps_sound
+
+
+
+
+positions_at->steps_sound
+
+
+
+positions_comp
+
+positions_comp
+
+
+
+
+positions_comp->steps_complete
+
+
+
+positions_hole
+
+positions_hole
+
+
+
+
+root_steps_in_steps
+
+root_steps_in_steps
+
+
+
+
+positions_hole->root_steps_in_steps
+
+
+
+root_steps_complete
+
+root_steps_complete
+
+
+
+
+root_steps_complete->steps_complete
+
+
+
+root_steps_in_steps->steps_complete
+
+
+
+root_steps_sound
+
+root_steps_sound
+
+
+
+
+root_steps_sound->steps_sound
+
+
+
+steps_complete->has_red_spec
+
+
+
+steps_complete->nf_iff_steps_nil
+
+
+
+steps_sound->has_red_spec
+
+
+
+steps_sound_red1
+
+steps_sound_red1
+
+
+
+
+steps_sound->steps_sound_red1
+
+
+
+steps_sound_red1->nf_iff_steps_nil
+
+
+
+zdecs_complete
+
+zdecs_complete
+
+
+
+
+zdecs_complete->root_steps_complete
+
+
+
+zdecs_sound
+
+zdecs_sound
+
+
+
+
+zdecs_sound->root_steps_sound
+
+
+
diff --git a/graphs/dependency-M2.dot b/graphs/dependency-M2.dot
new file mode 100644
index 0000000..8d50a7b
--- /dev/null
+++ b/graphs/dependency-M2.dot
@@ -0,0 +1,115 @@
+digraph deps {
+ rankdir=LR;
+ bgcolor="#ffffff";
+ splines=polyline;
+ concentrate=true;
+ nodesep=0.2;
+ ranksep=0.9;
+ node [fontname=Inter, fontsize=9];
+ edge [fontname=Inter, fontsize=8, color="#000000", fontcolor="#000000", arrowsize=0.6, penwidth=0.8];
+ graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="#000000", label=<Theorem dependencies M2, 53 results >];
+ close_rec_notin [label="close_rec_notin\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="close_rec_notin theory/Binding.v proved"];
+ fvs_lift [label="fvs_lift\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="fvs_lift theory/Binding.v proved"];
+ has_red_spec [label="has_red_spec\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="has_red_spec theory/Reduction.v proved"];
+ open_rec_occurs_false [label="open_rec_occurs_false\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="open_rec_occurs_false theory/Binding.v proved"];
+ steps_complete [label="steps_complete\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="steps_complete theory/Reduction.v proved"];
+ steps_sound [label="steps_sound\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="steps_sound theory/Reduction.v proved"];
+ steps_sound_red1 [label="steps_sound_red1\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="steps_sound_red1 theory/Reduction.v proved"];
+ subst_fvar_other [label="subst_fvar_other\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="subst_fvar_other theory/Binding.v proved"];
+ subst_fvar_self [label="subst_fvar_self\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="subst_fvar_self theory/Binding.v proved"];
+ zdecs_sound [label="zdecs_sound\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="zdecs_sound theory/Reduction.v proved"];
+ Plus_to_Star [label="Plus_to_Star", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Plus_to_Star theory/Closure.v proved"];
+ Star_red1_context [label="Star_red1_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Star_red1_context theory/Closure.v proved"];
+ Star_trans [label="Star_trans", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Star_trans theory/Closure.v proved"];
+ red1_star [label="red1_star", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red1_star theory/Closure.v proved"];
+ star_one_trans [label="star_one_trans", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="star_one_trans theory/Closure.v proved"];
+ enumerate_check [label="enumerate_check", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="enumerate_check theory/Enumerate.v proved"];
+ enumerate_complete [label="enumerate_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="enumerate_complete theory/Enumerate.v proved"];
+ enumerate_sound [label="enumerate_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="enumerate_sound theory/Enumerate.v proved"];
+ in_comb [label="in_comb", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="in_comb theory/Enumerate.v proved"];
+ pow2_pos [label="pow2_pos", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="pow2_pos theory/Enumerate.v proved"];
+ size_all_terms [label="size_all_terms", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="size_all_terms theory/Enumerate.v proved"];
+ Plus_red1_context [label="Plus_red1_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Plus_red1_context theory/Metatheory.v proved"];
+ Plus_step_trans [label="Plus_step_trans", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Plus_step_trans theory/Metatheory.v proved"];
+ Plus_trans [label="Plus_trans", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Plus_trans theory/Metatheory.v proved"];
+ full_comp_aux [label="full_comp_aux", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="full_comp_aux theory/Metatheory.v proved"];
+ fvs_zplug_lift [label="fvs_zplug_lift", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="fvs_zplug_lift theory/Metatheory.v proved"];
+ lemma_2_1_fv_preserved [label="lemma_2_1_fv_preserved", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v proved"];
+ lemma_2_2_full_comp [label="lemma_2_2_full_comp", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v proved"];
+ lemma_2_3_beta_sim [label="lemma_2_3_beta_sim", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v proved"];
+ occurs_count_false [label="occurs_count_false", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="occurs_count_false theory/Metatheory.v proved"];
+ occurs_count_pos [label="occurs_count_pos", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="occurs_count_pos theory/Metatheory.v proved"];
+ occurs_count_zero [label="occurs_count_zero", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="occurs_count_zero theory/Metatheory.v proved"];
+ occurs_count_zfill_plug [label="occurs_count_zfill_plug", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="occurs_count_zfill_plug theory/Metatheory.v proved"];
+ occurs_lift_self [label="occurs_lift_self", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="occurs_lift_self theory/Metatheory.v proved"];
+ open_rec_zplug_lift [label="open_rec_zplug_lift", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_zplug_lift theory/Metatheory.v proved"];
+ plug_fv_mono [label="plug_fv_mono", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="plug_fv_mono theory/Metatheory.v proved"];
+ red1_root_fv [label="red1_root_fv", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red1_root_fv theory/Metatheory.v proved"];
+ red1r_fv [label="red1r_fv", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red1r_fv theory/Metatheory.v proved"];
+ zdecs_nonempty [label="zdecs_nonempty", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="zdecs_nonempty theory/Metatheory.v proved"];
+ check_all_true [label="check_all_true", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="check_all_true theory/Random.v proved"];
+ check_term_true [label="check_term_true", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="check_term_true theory/Random.v proved"];
+ gen_complete [label="gen_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="gen_complete theory/Random.v proved"];
+ gen_fv_preserved [label="gen_fv_preserved", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="gen_fv_preserved theory/Random.v proved"];
+ gen_list_length [label="gen_list_length", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="gen_list_length theory/Random.v proved"];
+ gen_sound [label="gen_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="gen_sound theory/Random.v proved"];
+ close_rec_app [label="close_rec_app", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_app theory/Substitution.v proved"];
+ close_rec_esub [label="close_rec_esub", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_esub theory/Substitution.v proved"];
+ close_rec_lam [label="close_rec_lam", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_lam theory/Substitution.v proved"];
+ open_rec_app [label="open_rec_app", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_app theory/Substitution.v proved"];
+ open_rec_esub [label="open_rec_esub", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_esub theory/Substitution.v proved"];
+ open_rec_lam [label="open_rec_lam", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_lam theory/Substitution.v proved"];
+ open_rec_lc [label="open_rec_lc", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_lc theory/Substitution.v proved"];
+ open_rec_lc_atom [label="open_rec_lc_atom", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_lc_atom theory/Substitution.v proved"];
+ subst_app [label="subst_app", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_app theory/Substitution.v proved"];
+ subst_esub [label="subst_esub", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_esub theory/Substitution.v proved"];
+ subst_lam [label="subst_lam", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_lam theory/Substitution.v proved"];
+ subst_lc_self [label="subst_lc_self", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_lc_self theory/Substitution.v proved"];
+ subst_notin [label="subst_notin", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_notin theory/Substitution.v proved"];
+ subst_other [label="subst_other", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_other theory/Substitution.v proved"];
+ corpus_complete [label="corpus_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="corpus_complete theory/Tests.v proved"];
+ corpus_decides [label="corpus_decides", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="corpus_decides theory/Tests.v proved"];
+ corpus_fv_preserved [label="corpus_fv_preserved", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="corpus_fv_preserved theory/Tests.v proved"];
+ corpus_sound [label="corpus_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="corpus_sound theory/Tests.v proved"];
+ in_comb -> size_all_terms;
+ pow2_pos -> size_all_terms;
+ check_all_true -> enumerate_check;
+ steps_sound -> enumerate_sound;
+ steps_complete -> enumerate_complete;
+ 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;
+ 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;
+ 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;
+ 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;
+}
diff --git a/graphs/dependency-M2.png b/graphs/dependency-M2.png
new file mode 100644
index 0000000..eeb6123
Binary files /dev/null and b/graphs/dependency-M2.png differ
diff --git a/graphs/dependency-M2.svg b/graphs/dependency-M2.svg
new file mode 100644
index 0000000..cf2089f
--- /dev/null
+++ b/graphs/dependency-M2.svg
@@ -0,0 +1,827 @@
+
+
+
+
+
+
+deps
+Theorem dependencies M2, 53 results
+
+
+close_rec_notin
+
+close_rec_notin\n(M1)
+
+
+
+
+subst_notin
+
+subst_notin
+
+
+
+
+close_rec_notin->subst_notin
+
+
+
+fvs_lift
+
+fvs_lift\n(M1)
+
+
+
+
+fvs_zplug_lift
+
+fvs_zplug_lift
+
+
+
+
+fvs_lift->fvs_zplug_lift
+
+
+
+has_red_spec
+
+has_red_spec\n(M1)
+
+
+
+
+check_term_true
+
+check_term_true
+
+
+
+
+has_red_spec->check_term_true
+
+
+
+corpus_decides
+
+corpus_decides
+
+
+
+
+has_red_spec->corpus_decides
+
+
+
+open_rec_occurs_false
+
+open_rec_occurs_false\n(M1)
+
+
+
+
+full_comp_aux
+
+full_comp_aux
+
+
+
+
+open_rec_occurs_false->full_comp_aux
+
+
+
+open_rec_zplug_lift
+
+open_rec_zplug_lift
+
+
+
+
+open_rec_occurs_false->open_rec_zplug_lift
+
+
+
+open_rec_occurs_false->subst_notin
+
+
+
+steps_complete
+
+steps_complete\n(M1)
+
+
+
+
+enumerate_complete
+
+enumerate_complete
+
+
+
+
+steps_complete->enumerate_complete
+
+
+
+gen_complete
+
+gen_complete
+
+
+
+
+steps_complete->gen_complete
+
+
+
+corpus_complete
+
+corpus_complete
+
+
+
+
+steps_complete->corpus_complete
+
+
+
+steps_sound
+
+steps_sound\n(M1)
+
+
+
+
+enumerate_sound
+
+enumerate_sound
+
+
+
+
+steps_sound->enumerate_sound
+
+
+
+gen_sound
+
+gen_sound
+
+
+
+
+steps_sound->gen_sound
+
+
+
+corpus_sound
+
+corpus_sound
+
+
+
+
+steps_sound->corpus_sound
+
+
+
+steps_sound_red1
+
+steps_sound_red1\n(M1)
+
+
+
+
+steps_sound_red1->check_term_true
+
+
+
+gen_fv_preserved
+
+gen_fv_preserved
+
+
+
+
+steps_sound_red1->gen_fv_preserved
+
+
+
+corpus_fv_preserved
+
+corpus_fv_preserved
+
+
+
+
+steps_sound_red1->corpus_fv_preserved
+
+
+
+subst_fvar_other
+
+subst_fvar_other\n(M1)
+
+
+
+
+subst_other
+
+subst_other
+
+
+
+
+subst_fvar_other->subst_other
+
+
+
+subst_fvar_self
+
+subst_fvar_self\n(M1)
+
+
+
+
+subst_lc_self
+
+subst_lc_self
+
+
+
+
+subst_fvar_self->subst_lc_self
+
+
+
+zdecs_sound
+
+zdecs_sound\n(M1)
+
+
+
+
+zdecs_sound->full_comp_aux
+
+
+
+Plus_to_Star
+
+Plus_to_Star
+
+
+
+
+Star_red1_context
+
+Star_red1_context
+
+
+
+
+Star_trans
+
+Star_trans
+
+
+
+
+red1_star
+
+red1_star
+
+
+
+
+star_one_trans
+
+star_one_trans
+
+
+
+
+enumerate_check
+
+enumerate_check
+
+
+
+
+in_comb
+
+in_comb
+
+
+
+
+size_all_terms
+
+size_all_terms
+
+
+
+
+in_comb->size_all_terms
+
+
+
+pow2_pos
+
+pow2_pos
+
+
+
+
+pow2_pos->size_all_terms
+
+
+
+Plus_red1_context
+
+Plus_red1_context
+
+
+
+
+lemma_2_3_beta_sim
+
+lemma_2_3_beta_sim
+
+
+
+
+Plus_red1_context->lemma_2_3_beta_sim
+
+
+
+Plus_step_trans
+
+Plus_step_trans
+
+
+
+
+Plus_trans
+
+Plus_trans
+
+
+
+
+lemma_2_2_full_comp
+
+lemma_2_2_full_comp
+
+
+
+
+full_comp_aux->lemma_2_2_full_comp
+
+
+
+red1_root_fv
+
+red1_root_fv
+
+
+
+
+fvs_zplug_lift->red1_root_fv
+
+
+
+lemma_2_1_fv_preserved
+
+lemma_2_1_fv_preserved
+
+
+
+
+lemma_2_1_fv_preserved->gen_fv_preserved
+
+
+
+lemma_2_1_fv_preserved->corpus_fv_preserved
+
+
+
+lemma_2_2_full_comp->lemma_2_3_beta_sim
+
+
+
+occurs_count_false
+
+occurs_count_false
+
+
+
+
+occurs_count_zfill_plug
+
+occurs_count_zfill_plug
+
+
+
+
+occurs_count_false->occurs_count_zfill_plug
+
+
+
+occurs_count_pos
+
+occurs_count_pos
+
+
+
+
+occurs_count_zero
+
+occurs_count_zero
+
+
+
+
+occurs_count_zero->full_comp_aux
+
+
+
+occurs_count_zero->occurs_count_pos
+
+
+
+occurs_count_zfill_plug->full_comp_aux
+
+
+
+occurs_lift_self
+
+occurs_lift_self
+
+
+
+
+occurs_lift_self->occurs_count_zfill_plug
+
+
+
+occurs_lift_self->open_rec_zplug_lift
+
+
+
+open_rec_zplug_lift->full_comp_aux
+
+
+
+plug_fv_mono
+
+plug_fv_mono
+
+
+
+
+red1r_fv
+
+red1r_fv
+
+
+
+
+plug_fv_mono->red1r_fv
+
+
+
+red1_root_fv->red1r_fv
+
+
+
+red1r_fv->lemma_2_1_fv_preserved
+
+
+
+zdecs_nonempty
+
+zdecs_nonempty
+
+
+
+
+zdecs_nonempty->full_comp_aux
+
+
+
+check_all_true
+
+check_all_true
+
+
+
+
+check_all_true->enumerate_check
+
+
+
+check_term_true->check_all_true
+
+
+
+gen_list_length
+
+gen_list_length
+
+
+
+
+close_rec_app
+
+close_rec_app
+
+
+
+
+close_rec_esub
+
+close_rec_esub
+
+
+
+
+close_rec_lam
+
+close_rec_lam
+
+
+
+
+open_rec_app
+
+open_rec_app
+
+
+
+
+open_rec_esub
+
+open_rec_esub
+
+
+
+
+open_rec_lam
+
+open_rec_lam
+
+
+
+
+open_rec_lc
+
+open_rec_lc
+
+
+
+
+open_rec_lc_atom
+
+open_rec_lc_atom
+
+
+
+
+open_rec_lc_atom->open_rec_lc
+
+
+
+subst_app
+
+subst_app
+
+
+
+
+subst_esub
+
+subst_esub
+
+
+
+
+subst_lam
+
+subst_lam
+
+
+
+
diff --git a/graphs/dependency-M3.dot b/graphs/dependency-M3.dot
new file mode 100644
index 0000000..bb68146
--- /dev/null
+++ b/graphs/dependency-M3.dot
@@ -0,0 +1,52 @@
+digraph deps {
+ rankdir=LR;
+ bgcolor="#ffffff";
+ splines=polyline;
+ concentrate=true;
+ nodesep=0.2;
+ ranksep=0.9;
+ node [fontname=Inter, fontsize=9];
+ edge [fontname=Inter, fontsize=8, color="#000000", fontcolor="#000000", arrowsize=0.6, penwidth=0.8];
+ graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="#000000", label=<Theorem dependencies M3, 16 results >];
+ Plus_to_Star [label="Plus_to_Star\\n(M2)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="Plus_to_Star theory/Closure.v proved"];
+ occurs_count_zero [label="occurs_count_zero\\n(M2)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="occurs_count_zero theory/Metatheory.v proved"];
+ occurs_count_zfill_plug [label="occurs_count_zfill_plug\\n(M2)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="occurs_count_zfill_plug theory/Metatheory.v proved"];
+ open_rec_occurs_false [label="open_rec_occurs_false\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="open_rec_occurs_false theory/Binding.v proved"];
+ open_rec_zplug_lift [label="open_rec_zplug_lift\\n(M2)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="open_rec_zplug_lift theory/Metatheory.v proved"];
+ zdecs_nonempty [label="zdecs_nonempty\\n(M2)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="zdecs_nonempty theory/Metatheory.v proved"];
+ zdecs_sound [label="zdecs_sound\\n(M1)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="zdecs_sound theory/Reduction.v proved"];
+ R_Gc_disjoint [label="R_Gc_disjoint", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="R_Gc_disjoint theory/Subsystem.v proved"];
+ Star_red_sub_context [label="Star_red_sub_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Star_red_sub_context theory/Subsystem.v proved"];
+ es_count_plug_mono [label="es_count_plug_mono", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="es_count_plug_mono theory/Subsystem.v proved"];
+ full_comp_aux_sub [label="full_comp_aux_sub", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="full_comp_aux_sub theory/Subsystem.v proved"];
+ occurs_zfill [label="occurs_zfill", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="occurs_zfill theory/Subsystem.v proved"];
+ plus_red_sub_full_comp [label="plus_red_sub_full_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="plus_red_sub_full_comp theory/Subsystem.v proved"];
+ red_gc_measure [label="red_gc_measure", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_gc_measure theory/Subsystem.v proved"];
+ red_gc_terminates [label="red_gc_terminates", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_gc_terminates theory/Subsystem.v proved"];
+ red_gc_to_red_sub [label="red_gc_to_red_sub", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_gc_to_red_sub theory/Subsystem.v proved"];
+ red_sub_context [label="red_sub_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_sub_context theory/Subsystem.v proved"];
+ red_sub_gc [label="red_sub_gc", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_sub_gc theory/Subsystem.v proved"];
+ red_sub_r [label="red_sub_r", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_sub_r theory/Subsystem.v proved"];
+ red_sub_root_to_red1 [label="red_sub_root_to_red1", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_sub_root_to_red1 theory/Subsystem.v proved"];
+ red_sub_to_red1 [label="red_sub_to_red1", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red_sub_to_red1 theory/Subsystem.v proved"];
+ star_red_sub_full_comp [label="star_red_sub_full_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="star_red_sub_full_comp theory/Subsystem.v proved"];
+ zfill_occurs0 [label="zfill_occurs0", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="zfill_occurs0 theory/Subsystem.v proved"];
+ 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;
+}
diff --git a/graphs/dependency-M3.png b/graphs/dependency-M3.png
new file mode 100644
index 0000000..c1de881
Binary files /dev/null and b/graphs/dependency-M3.png differ
diff --git a/graphs/dependency-M3.svg b/graphs/dependency-M3.svg
new file mode 100644
index 0000000..a61c8aa
--- /dev/null
+++ b/graphs/dependency-M3.svg
@@ -0,0 +1,329 @@
+
+
+
+
+
+
+deps
+Theorem dependencies M3, 16 results
+
+
+Plus_to_Star
+
+Plus_to_Star\n(M2)
+
+
+
+
+star_red_sub_full_comp
+
+star_red_sub_full_comp
+
+
+
+
+Plus_to_Star->star_red_sub_full_comp
+
+
+
+occurs_count_zero
+
+occurs_count_zero\n(M2)
+
+
+
+
+full_comp_aux_sub
+
+full_comp_aux_sub
+
+
+
+
+occurs_count_zero->full_comp_aux_sub
+
+
+
+occurs_count_zfill_plug
+
+occurs_count_zfill_plug\n(M2)
+
+
+
+
+occurs_count_zfill_plug->full_comp_aux_sub
+
+
+
+open_rec_occurs_false
+
+open_rec_occurs_false\n(M1)
+
+
+
+
+open_rec_occurs_false->full_comp_aux_sub
+
+
+
+open_rec_zplug_lift
+
+open_rec_zplug_lift\n(M2)
+
+
+
+
+open_rec_zplug_lift->full_comp_aux_sub
+
+
+
+zdecs_nonempty
+
+zdecs_nonempty\n(M2)
+
+
+
+
+zdecs_nonempty->full_comp_aux_sub
+
+
+
+zdecs_sound
+
+zdecs_sound\n(M1)
+
+
+
+
+zdecs_sound->full_comp_aux_sub
+
+
+
+R_Gc_disjoint
+
+R_Gc_disjoint
+
+
+
+
+Star_red_sub_context
+
+Star_red_sub_context
+
+
+
+
+es_count_plug_mono
+
+es_count_plug_mono
+
+
+
+
+red_gc_measure
+
+red_gc_measure
+
+
+
+
+es_count_plug_mono->red_gc_measure
+
+
+
+plus_red_sub_full_comp
+
+plus_red_sub_full_comp
+
+
+
+
+full_comp_aux_sub->plus_red_sub_full_comp
+
+
+
+occurs_zfill
+
+occurs_zfill
+
+
+
+
+zfill_occurs0
+
+zfill_occurs0
+
+
+
+
+occurs_zfill->zfill_occurs0
+
+
+
+plus_red_sub_full_comp->star_red_sub_full_comp
+
+
+
+red_gc_terminates
+
+red_gc_terminates
+
+
+
+
+red_gc_measure->red_gc_terminates
+
+
+
+red_gc_to_red_sub
+
+red_gc_to_red_sub
+
+
+
+
+red_sub_context
+
+red_sub_context
+
+
+
+
+red_sub_context->Star_red_sub_context
+
+
+
+red_sub_gc
+
+red_sub_gc
+
+
+
+
+red_sub_gc->full_comp_aux_sub
+
+
+
+red_sub_gc->red_gc_to_red_sub
+
+
+
+red_sub_r
+
+red_sub_r
+
+
+
+
+red_sub_r->full_comp_aux_sub
+
+
+
+red_sub_root_to_red1
+
+red_sub_root_to_red1
+
+
+
+
+red_sub_to_red1
+
+red_sub_to_red1
+
+
+
+
+red_sub_root_to_red1->red_sub_to_red1
+
+
+
+zfill_occurs0->R_Gc_disjoint
+
+
+
diff --git a/graphs/dependency-M4.dot b/graphs/dependency-M4.dot
new file mode 100644
index 0000000..7c28ced
--- /dev/null
+++ b/graphs/dependency-M4.dot
@@ -0,0 +1,19 @@
+digraph deps {
+ rankdir=LR;
+ bgcolor="#ffffff";
+ splines=polyline;
+ concentrate=true;
+ nodesep=0.2;
+ ranksep=0.9;
+ node [fontname=Inter, fontsize=9];
+ edge [fontname=Inter, fontsize=8, color="#000000", fontcolor="#000000", arrowsize=0.6, penwidth=0.8];
+ graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="#000000", label=<Theorem dependencies M4, 6 results >];
+ par_context [label="par_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="par_context theory/Parallel.v proved"];
+ par_red1_iff [label="par_red1_iff", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="par_red1_iff theory/Parallel.v proved"];
+ par_reflexive [label="par_reflexive", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="par_reflexive theory/Parallel.v proved"];
+ par_to_red1_or_eq [label="par_to_red1_or_eq", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="par_to_red1_or_eq theory/Parallel.v proved"];
+ red1_in_par [label="red1_in_par", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red1_in_par theory/Parallel.v proved"];
+ red1_or_eq_to_par [label="red1_or_eq_to_par", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red1_or_eq_to_par theory/Parallel.v proved"];
+ par_red1_iff -> par_to_red1_or_eq;
+ par_red1_iff -> red1_or_eq_to_par;
+}
diff --git a/graphs/dependency-M4.png b/graphs/dependency-M4.png
new file mode 100644
index 0000000..7a565e9
Binary files /dev/null and b/graphs/dependency-M4.png differ
diff --git a/graphs/dependency-M4.svg b/graphs/dependency-M4.svg
new file mode 100644
index 0000000..d8a49f3
--- /dev/null
+++ b/graphs/dependency-M4.svg
@@ -0,0 +1,80 @@
+
+
+
+
+
+
+deps
+Theorem dependencies M4, 6 results
+
+
+par_context
+
+par_context
+
+
+
+
+par_red1_iff
+
+par_red1_iff
+
+
+
+
+par_to_red1_or_eq
+
+par_to_red1_or_eq
+
+
+
+
+par_red1_iff->par_to_red1_or_eq
+
+
+
+red1_or_eq_to_par
+
+red1_or_eq_to_par
+
+
+
+
+par_red1_iff->red1_or_eq_to_par
+
+
+
+par_reflexive
+
+par_reflexive
+
+
+
+
+red1_in_par
+
+red1_in_par
+
+
+
+
diff --git a/graphs/dependency-M5.dot b/graphs/dependency-M5.dot
new file mode 100644
index 0000000..2675344
--- /dev/null
+++ b/graphs/dependency-M5.dot
@@ -0,0 +1,126 @@
+digraph deps {
+ rankdir=LR;
+ bgcolor="#ffffff";
+ splines=polyline;
+ concentrate=true;
+ nodesep=0.2;
+ ranksep=0.9;
+ node [fontname=Inter, fontsize=9];
+ edge [fontname=Inter, fontsize=8, color="#000000", fontcolor="#000000", arrowsize=0.6, penwidth=0.8];
+ graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="#000000", label=<Theorem dependencies M5, 69 results >];
+ lemma_2_2_full_comp [label="lemma_2_2_full_comp\\n(M2)", shape=box, style="rounded,dashed,filled", fillcolor="#ffffff", color="#000000", penwidth=0.9, fontcolor="#000000", tooltip="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v proved"];
+ Plus_mred_of_Plus_red1 [label="Plus_mred_of_Plus_red1", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Plus_mred_of_Plus_red1 theory/Metaterm.v proved"];
+ mfvs_close_m [label="mfvs_close_m", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mfvs_close_m theory/Metaterm.v proved"];
+ mfvs_lift_m [label="mfvs_lift_m", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mfvs_lift_m theory/Metaterm.v proved"];
+ mfvs_open_m [label="mfvs_open_m", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mfvs_open_m theory/Metaterm.v proved"];
+ mred_B_intro [label="mred_B_intro", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_B_intro theory/Metaterm.v proved"];
+ mred_context [label="mred_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_context theory/Metaterm.v proved"];
+ mred_full_comp_pure [label="mred_full_comp_pure", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_full_comp_pure theory/Metaterm.v proved"];
+ mred_gc_intro [label="mred_gc_intro", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_gc_intro theory/Metaterm.v proved"];
+ mred_of_red1 [label="mred_of_red1", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_of_red1 theory/Metaterm.v proved"];
+ mred_plus_one [label="mred_plus_one", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_plus_one theory/Metaterm.v proved"];
+ mred_r_intro [label="mred_r_intro", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_r_intro theory/Metaterm.v proved"];
+ mred_term_context [label="mred_term_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="mred_term_context theory/Metaterm.v proved"];
+ of_trm_close [label="of_trm_close", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_close theory/Metaterm.v proved"];
+ of_trm_fvs [label="of_trm_fvs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_fvs theory/Metaterm.v proved"];
+ of_trm_injective [label="of_trm_injective", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_injective theory/Metaterm.v proved"];
+ of_trm_lift [label="of_trm_lift", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_lift theory/Metaterm.v proved"];
+ of_trm_moccurs [label="of_trm_moccurs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_moccurs theory/Metaterm.v proved"];
+ of_trm_moccurs0 [label="of_trm_moccurs0", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_moccurs0 theory/Metaterm.v proved"];
+ of_trm_open [label="of_trm_open", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_open theory/Metaterm.v proved"];
+ of_trm_plug [label="of_trm_plug", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="of_trm_plug theory/Metaterm.v proved"];
+ PlusN_to_StarN [label="PlusN_to_StarN", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="PlusN_to_StarN theory/NamedEs.v proved"];
+ StarN_one_trans [label="StarN_one_trans", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="StarN_one_trans theory/NamedEs.v proved"];
+ StarN_subred_context [label="StarN_subred_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="StarN_subred_context theory/NamedEs.v proved"];
+ StarN_trans [label="StarN_trans", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="StarN_trans theory/NamedEs.v proved"];
+ nred_stable_source [label="nred_stable_source", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nred_stable_source theory/NamedEs.v proved"];
+ nred_stable_target [label="nred_stable_target", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nred_stable_target theory/NamedEs.v proved"];
+ subred_Es_l [label="subred_Es_l", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_Es_l theory/NamedEs.v proved"];
+ subred_Es_lr [label="subred_Es_lr", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_Es_lr theory/NamedEs.v proved"];
+ subred_Es_r [label="subred_Es_r", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_Es_r theory/NamedEs.v proved"];
+ subred_context [label="subred_context", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_context theory/NamedEs.v proved"];
+ subred_context_rule [label="subred_context_rule", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_context_rule theory/NamedEs.v proved"];
+ subred_intro [label="subred_intro", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_intro theory/NamedEs.v proved"];
+ subred_nred [label="subred_nred", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_nred theory/NamedEs.v proved"];
+ subred_of_Es_nred_Es [label="subred_of_Es_nred_Es", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_of_Es_nred_Es theory/NamedEs.v proved"];
+ A1_C_related [label="A1_C_related", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="A1_C_related theory/NamedMeasure.v proved"];
+ A1_Mx_differ [label="A1_Mx_differ", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="A1_Mx_differ theory/NamedMeasure.v proved"];
+ A1_not_invariant [label="A1_not_invariant", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="A1_not_invariant theory/NamedMeasure.v proved"];
+ A1_s_differ [label="A1_s_differ", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="A1_s_differ theory/NamedMeasure.v proved"];
+ Gc_special_nondecrease [label="Gc_special_nondecrease", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Gc_special_nondecrease theory/NamedMeasure.v proved"];
+ Mx_fresh_fails [label="Mx_fresh_fails", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Mx_fresh_fails theory/NamedMeasure.v proved"];
+ Mx_ge_0 [label="Mx_ge_0", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Mx_ge_0 theory/NamedMeasure.v proved"];
+ current_sm_not_terminating [label="current_sm_not_terminating", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="current_sm_not_terminating theory/NamedMeasure.v proved"];
+ current_subred_not_terminating [label="current_subred_not_terminating", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="current_subred_not_terminating theory/NamedMeasure.v proved"];
+ head_has_pos [label="head_has_pos", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="head_has_pos theory/NamedMeasure.v proved"];
+ le_mul_of_one_le [label="le_mul_of_one_le", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="le_mul_of_one_le theory/NamedMeasure.v proved"];
+ nfv_annot_bound_example [label="nfv_annot_bound_example", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nfv_annot_bound_example theory/NamedMeasure.v proved"];
+ nocc_le_Mx [label="nocc_le_Mx", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nocc_le_Mx theory/NamedMeasure.v proved"];
+ nred_Gc_special [label="nred_Gc_special", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nred_Gc_special theory/NamedMeasure.v proved"];
+ nred_R_selfloop [label="nred_R_selfloop", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nred_R_selfloop theory/NamedMeasure.v proved"];
+ s_metavar_empty [label="s_metavar_empty", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="s_metavar_empty theory/NamedMeasure.v proved"];
+ subred_selfloop [label="subred_selfloop", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subred_selfloop theory/NamedMeasure.v proved"];
+ Es_ctx_any [label="Es_ctx_any", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Es_ctx_any theory/NamedMeta.v proved"];
+ Es_fv [label="Es_fv", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Es_fv theory/NamedMeta.v proved"];
+ Es_fv_both [label="Es_fv_both", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Es_fv_both theory/NamedMeta.v proved"];
+ Es_refl_any [label="Es_refl_any", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Es_refl_any theory/NamedMeta.v proved"];
+ Es_sym_any [label="Es_sym_any", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Es_sym_any theory/NamedMeta.v proved"];
+ Es_trans_any [label="Es_trans_any", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="Es_trans_any theory/NamedMeta.v proved"];
+ eqC_in_Es [label="eqC_in_Es", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="eqC_in_Es theory/NamedMeta.v proved"];
+ filter_neq_in [label="filter_neq_in", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="filter_neq_in theory/NamedMeta.v proved"];
+ in_filter_neq [label="in_filter_neq", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="in_filter_neq theory/NamedMeta.v proved"];
+ in_filter_neq_iff [label="in_filter_neq_iff", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="in_filter_neq_iff theory/NamedMeta.v proved"];
+ isubst_meta_in [label="isubst_meta_in", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="isubst_meta_in theory/NamedMeta.v proved"];
+ isubst_meta_notin [label="isubst_meta_notin", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="isubst_meta_notin theory/NamedMeta.v proved"];
+ nplug_esub_fv [label="nplug_esub_fv", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nplug_esub_fv theory/NamedMeta.v proved"];
+ nplug_fv_mono [label="nplug_fv_mono", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nplug_fv_mono theory/NamedMeta.v proved"];
+ nplug_fv_upper [label="nplug_fv_upper", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nplug_fv_upper theory/NamedMeta.v proved"];
+ nred_R_intro [label="nred_R_intro", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nred_R_intro theory/NamedMeta.v proved"];
+ nred_core_fv [label="nred_core_fv", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nred_core_fv theory/NamedMeta.v proved"];
+ nred_fv [label="nred_fv", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nred_fv theory/NamedMeta.v proved"];
+ 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;
+ subred_intro -> subred_nred;
+ subred_intro -> subred_Es_l;
+ subred_intro -> subred_Es_r;
+ subred_Es_l -> subred_Es_lr;
+ subred_Es_r -> subred_Es_lr;
+ subred_intro -> subred_context;
+ subred_context -> subred_context_rule;
+ subred_nred -> subred_context_rule;
+ subred_intro -> subred_of_Es_nred_Es;
+ subred_intro -> nred_stable_source;
+ subred_intro -> nred_stable_target;
+ subred_context -> StarN_subred_context;
+ head_has_pos -> nocc_le_Mx;
+ le_mul_of_one_le -> nocc_le_Mx;
+ nfv_annot_bound_example -> Mx_fresh_fails;
+ A1_C_related -> A1_not_invariant;
+ A1_s_differ -> A1_not_invariant;
+ nred_R_selfloop -> current_sm_not_terminating;
+ nred_R_selfloop -> subred_selfloop;
+ subred_nred -> subred_selfloop;
+ subred_selfloop -> current_subred_not_terminating;
+ 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;
+ in_filter_neq_iff -> Es_fv_both;
+ nplug_fv_mono -> Es_fv_both;
+ Es_fv_both -> Es_fv;
+}
diff --git a/graphs/dependency-M5.png b/graphs/dependency-M5.png
new file mode 100644
index 0000000..d889c06
Binary files /dev/null and b/graphs/dependency-M5.png differ
diff --git a/graphs/dependency-M5.svg b/graphs/dependency-M5.svg
new file mode 100644
index 0000000..7e6a3e1
--- /dev/null
+++ b/graphs/dependency-M5.svg
@@ -0,0 +1,914 @@
+
+
+
+
+
+
+deps
+Theorem dependencies M5, 69 results
+
+
+lemma_2_2_full_comp
+
+lemma_2_2_full_comp\n(M2)
+
+
+
+
+mred_full_comp_pure
+
+mred_full_comp_pure
+
+
+
+
+lemma_2_2_full_comp->mred_full_comp_pure
+
+
+
+Plus_mred_of_Plus_red1
+
+Plus_mred_of_Plus_red1
+
+
+
+
+Plus_mred_of_Plus_red1->mred_full_comp_pure
+
+
+
+mfvs_close_m
+
+mfvs_close_m
+
+
+
+
+mfvs_lift_m
+
+mfvs_lift_m
+
+
+
+
+mfvs_open_m
+
+mfvs_open_m
+
+
+
+
+mfvs_lift_m->mfvs_open_m
+
+
+
+mred_B_intro
+
+mred_B_intro
+
+
+
+
+mred_context
+
+mred_context
+
+
+
+
+mred_gc_intro
+
+mred_gc_intro
+
+
+
+
+mred_of_red1
+
+mred_of_red1
+
+
+
+
+mred_plus_one
+
+mred_plus_one
+
+
+
+
+mred_r_intro
+
+mred_r_intro
+
+
+
+
+mred_term_context
+
+mred_term_context
+
+
+
+
+of_trm_close
+
+of_trm_close
+
+
+
+
+of_trm_fvs
+
+of_trm_fvs
+
+
+
+
+of_trm_injective
+
+of_trm_injective
+
+
+
+
+of_trm_lift
+
+of_trm_lift
+
+
+
+
+of_trm_open
+
+of_trm_open
+
+
+
+
+of_trm_lift->of_trm_open
+
+
+
+of_trm_moccurs
+
+of_trm_moccurs
+
+
+
+
+of_trm_moccurs0
+
+of_trm_moccurs0
+
+
+
+
+of_trm_moccurs->of_trm_moccurs0
+
+
+
+of_trm_plug
+
+of_trm_plug
+
+
+
+
+of_trm_plug->mred_term_context
+
+
+
+PlusN_to_StarN
+
+PlusN_to_StarN
+
+
+
+
+StarN_one_trans
+
+StarN_one_trans
+
+
+
+
+StarN_subred_context
+
+StarN_subred_context
+
+
+
+
+StarN_trans
+
+StarN_trans
+
+
+
+
+nred_stable_source
+
+nred_stable_source
+
+
+
+
+nred_stable_target
+
+nred_stable_target
+
+
+
+
+subred_Es_l
+
+subred_Es_l
+
+
+
+
+subred_Es_lr
+
+subred_Es_lr
+
+
+
+
+subred_Es_l->subred_Es_lr
+
+
+
+subred_Es_r
+
+subred_Es_r
+
+
+
+
+subred_Es_r->subred_Es_lr
+
+
+
+subred_context
+
+subred_context
+
+
+
+
+subred_context->StarN_subred_context
+
+
+
+subred_context_rule
+
+subred_context_rule
+
+
+
+
+subred_context->subred_context_rule
+
+
+
+subred_intro
+
+subred_intro
+
+
+
+
+subred_intro->nred_stable_source
+
+
+
+subred_intro->nred_stable_target
+
+
+
+subred_intro->subred_Es_l
+
+
+
+subred_intro->subred_Es_r
+
+
+
+subred_intro->subred_context
+
+
+
+subred_nred
+
+subred_nred
+
+
+
+
+subred_intro->subred_nred
+
+
+
+subred_of_Es_nred_Es
+
+subred_of_Es_nred_Es
+
+
+
+
+subred_intro->subred_of_Es_nred_Es
+
+
+
+subred_nred->subred_context_rule
+
+
+
+subred_selfloop
+
+subred_selfloop
+
+
+
+
+subred_nred->subred_selfloop
+
+
+
+A1_C_related
+
+A1_C_related
+
+
+
+
+A1_not_invariant
+
+A1_not_invariant
+
+
+
+
+A1_C_related->A1_not_invariant
+
+
+
+A1_Mx_differ
+
+A1_Mx_differ
+
+
+
+
+A1_s_differ
+
+A1_s_differ
+
+
+
+
+A1_s_differ->A1_not_invariant
+
+
+
+Gc_special_nondecrease
+
+Gc_special_nondecrease
+
+
+
+
+Mx_fresh_fails
+
+Mx_fresh_fails
+
+
+
+
+Mx_ge_0
+
+Mx_ge_0
+
+
+
+
+current_sm_not_terminating
+
+current_sm_not_terminating
+
+
+
+
+current_subred_not_terminating
+
+current_subred_not_terminating
+
+
+
+
+head_has_pos
+
+head_has_pos
+
+
+
+
+nocc_le_Mx
+
+nocc_le_Mx
+
+
+
+
+head_has_pos->nocc_le_Mx
+
+
+
+le_mul_of_one_le
+
+le_mul_of_one_le
+
+
+
+
+le_mul_of_one_le->nocc_le_Mx
+
+
+
+nfv_annot_bound_example
+
+nfv_annot_bound_example
+
+
+
+
+nfv_annot_bound_example->Mx_fresh_fails
+
+
+
+nred_Gc_special
+
+nred_Gc_special
+
+
+
+
+nred_R_selfloop
+
+nred_R_selfloop
+
+
+
+
+nred_R_selfloop->current_sm_not_terminating
+
+
+
+nred_R_selfloop->subred_selfloop
+
+
+
+s_metavar_empty
+
+s_metavar_empty
+
+
+
+
+subred_selfloop->current_subred_not_terminating
+
+
+
+Es_ctx_any
+
+Es_ctx_any
+
+
+
+
+Es_fv
+
+Es_fv
+
+
+
+
+Es_fv_both
+
+Es_fv_both
+
+
+
+
+Es_fv_both->Es_fv
+
+
+
+Es_refl_any
+
+Es_refl_any
+
+
+
+
+Es_sym_any
+
+Es_sym_any
+
+
+
+
+Es_trans_any
+
+Es_trans_any
+
+
+
+
+eqC_in_Es
+
+eqC_in_Es
+
+
+
+
+filter_neq_in
+
+filter_neq_in
+
+
+
+
+nplug_esub_fv
+
+nplug_esub_fv
+
+
+
+
+filter_neq_in->nplug_esub_fv
+
+
+
+nplug_fv_mono
+
+nplug_fv_mono
+
+
+
+
+filter_neq_in->nplug_fv_mono
+
+
+
+nplug_fv_upper
+
+nplug_fv_upper
+
+
+
+
+filter_neq_in->nplug_fv_upper
+
+
+
+nred_core_fv
+
+nred_core_fv
+
+
+
+
+filter_neq_in->nred_core_fv
+
+
+
+nred_fv
+
+nred_fv
+
+
+
+
+filter_neq_in->nred_fv
+
+
+
+in_filter_neq
+
+in_filter_neq
+
+
+
+
+in_filter_neq->nplug_esub_fv
+
+
+
+in_filter_neq->nplug_fv_mono
+
+
+
+in_filter_neq->nplug_fv_upper
+
+
+
+in_filter_neq->nred_core_fv
+
+
+
+in_filter_neq->nred_fv
+
+
+
+in_filter_neq_iff
+
+in_filter_neq_iff
+
+
+
+
+in_filter_neq_iff->Es_fv_both
+
+
+
+isubst_meta_in
+
+isubst_meta_in
+
+
+
+
+isubst_meta_notin
+
+isubst_meta_notin
+
+
+
+
+nplug_esub_fv->nred_fv
+
+
+
+nplug_fv_mono->Es_fv_both
+
+
+
+nplug_fv_mono->nred_core_fv
+
+
+
+nplug_fv_mono->nred_fv
+
+
+
+nplug_fv_upper->nred_core_fv
+
+
+
+nplug_fv_upper->nred_fv
+
+
+
+nred_R_intro
+
+nred_R_intro
+
+
+
+
diff --git a/graphs/dependency-overview.dot b/graphs/dependency-overview.dot
new file mode 100644
index 0000000..7ec6ba8
--- /dev/null
+++ b/graphs/dependency-overview.dot
@@ -0,0 +1,20 @@
+digraph deps {
+ rankdir=LR;
+ bgcolor="#ffffff";
+ splines=polyline;
+ concentrate=true;
+ nodesep=0.2;
+ ranksep=0.9;
+ node [fontname=Inter, fontsize=9];
+ edge [fontname=Inter, fontsize=8, color="#000000", fontcolor="#000000", arrowsize=0.6, penwidth=0.8];
+ graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="#000000", label=<Theorem dependency by milestone >];
+ M1 [label="M1\\n33 results", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ M2 [label="M2\\n53 results", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ M3 [label="M3\\n16 results", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ M4 [label="M4\\n6 results", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ M5 [label="M5\\n69 results", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ M1 -> M2;
+ M1 -> M3;
+ M2 -> M3;
+ M2 -> M5;
+}
diff --git a/graphs/dependency-overview.png b/graphs/dependency-overview.png
new file mode 100644
index 0000000..acdfdd3
Binary files /dev/null and b/graphs/dependency-overview.png differ
diff --git a/graphs/dependency-overview.svg b/graphs/dependency-overview.svg
new file mode 100644
index 0000000..173198a
--- /dev/null
+++ b/graphs/dependency-overview.svg
@@ -0,0 +1,68 @@
+
+
+
+
+
+
+deps
+Theorem dependency by milestone
+
+
+M1
+M1\n33 results
+
+
+
+M2
+M2\n53 results
+
+
+
+M1->M2
+
+
+
+M3
+M3\n16 results
+
+
+
+M1->M3
+
+
+
+M2->M3
+
+
+
+M5
+M5\n69 results
+
+
+
+M2->M5
+
+
+
+M4
+M4\n6 results
+
+
+
diff --git a/graphs/dependency.dot b/graphs/dependency.dot
deleted file mode 100644
index 9fb35b0..0000000
--- a/graphs/dependency.dot
+++ /dev/null
@@ -1,268 +0,0 @@
-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=<Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M4) proved stated planned blocked
-
-theorem_deps
-Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M4)
-proved
-
-stated
-
-planned
-
-blocked
-
-
-fvs_lift
-
-fvs_lift
-
-
-
-
-open_rec_fvs
-
-open_rec_fvs
-
-
-
-
-fvs_lift->open_rec_fvs
-
-
-
-fvs_zplug_lift
-
-fvs_zplug_lift
-
-
-
-
-fvs_lift->fvs_zplug_lift
-
-
-
-lift_lc
-
-lift_lc
-
-
-
-
-lift_0_lc
-
-lift_0_lc
-
-
-
-
-lift_lc->lift_0_lc
-
-
-
-subst_fvar_self
-
-subst_fvar_self
-
-
-
-
-lift_0_lc->subst_fvar_self
-
-
-
-open_rec_bvar
-
-open_rec_bvar
-
-
-
-
-open_rec_bvar->open_rec_fvs
-
-
-
-open_close
-
-open_close
-
-
-
-
-open_rec_bvar->open_close
-
-
-
-close_rec_fvar
-
-close_rec_fvar
-
-
-
-
-open_rec_occurs_false
-
-open_rec_occurs_false
-
-
-
-
-open_rec_zplug_lift
-
-open_rec_zplug_lift
-
-
-
-
-open_rec_occurs_false->open_rec_zplug_lift
-
-
-
-full_comp_aux
-
-full_comp_aux
-
-
-
-
-open_rec_occurs_false->full_comp_aux
-
-
-
-subst_notin
-
-subst_notin
-
-
-
-
-open_rec_occurs_false->subst_notin
-
-
-
-full_comp_aux_sub
-
-full_comp_aux_sub
-
-
-
-
-open_rec_occurs_false->full_comp_aux_sub
-
-
-
-close_rec_notin
-
-close_rec_notin
-
-
-
-
-close_rec_notin->subst_notin
-
-
-
-close_rec_fvs
-
-close_rec_fvs
-
-
-
-
-subst_fvs
-
-subst_fvs
-
-
-
-
-close_rec_fvs->subst_fvs
-
-
-
-open_rec_bvar_neq
-
-open_rec_bvar_neq
-
-
-
-
-open_rec_bvar_neq->open_rec_fvs
-
-
-
-open_rec_fvs->subst_fvs
-
-
-
-subst_lc_self
-
-subst_lc_self
-
-
-
-
-subst_fvar_self->subst_lc_self
-
-
-
-subst_fvar_other
-
-subst_fvar_other
-
-
-
-
-subst_other
-
-subst_other
-
-
-
-
-subst_fvar_other->subst_other
-
-
-
-Star_trans
-
-Star_trans
-
-
-
-
-red1_star
-
-red1_star
-
-
-
-
-Plus_to_Star
-
-Plus_to_Star
-
-
-
-
-star_red_sub_full_comp
-
-star_red_sub_full_comp
-
-
-
-
-Plus_to_Star->star_red_sub_full_comp
-
-
-
-Star_red1_context
-
-Star_red1_context
-
-
-
-
-star_one_trans
-
-star_one_trans
-
-
-
-
-in_comb
-
-in_comb
-
-
-
-
-size_all_terms
-
-size_all_terms
-
-
-
-
-in_comb->size_all_terms
-
-
-
-pow2_pos
-
-pow2_pos
-
-
-
-
-pow2_pos->size_all_terms
-
-
-
-enumerate_check
-
-enumerate_check
-
-
-
-
-enumerate_sound
-
-enumerate_sound
-
-
-
-
-enumerate_complete
-
-enumerate_complete
-
-
-
-
-of_trm_fvs
-
-of_trm_fvs
-
-
-
-
-of_trm_lift
-
-of_trm_lift
-
-
-
-
-of_trm_open
-
-of_trm_open
-
-
-
-
-of_trm_lift->of_trm_open
-
-
-
-of_trm_close
-
-of_trm_close
-
-
-
-
-of_trm_injective
-
-of_trm_injective
-
-
-
-
-mfvs_lift_m
-
-mfvs_lift_m
-
-
-
-
-mfvs_open_m
-
-mfvs_open_m
-
-
-
-
-mfvs_lift_m->mfvs_open_m
-
-
-
-mfvs_close_m
-
-mfvs_close_m
-
-
-
-
-of_trm_plug
-
-of_trm_plug
-
-
-
-
-mred_term_context
-
-mred_term_context
-
-
-
-
-of_trm_plug->mred_term_context
-
-
-
-mred_of_red1
-
-mred_of_red1
-
-
-
-
-mred_context
-
-mred_context
-
-
-
-
-of_trm_moccurs
-
-of_trm_moccurs
-
-
-
-
-of_trm_moccurs0
-
-of_trm_moccurs0
-
-
-
-
-of_trm_moccurs->of_trm_moccurs0
-
-
-
-mred_B_intro
-
-mred_B_intro
-
-
-
-
-mred_gc_intro
-
-mred_gc_intro
-
-
-
-
-mred_r_intro
-
-mred_r_intro
-
-
-
-
-Plus_mred_of_Plus_red1
-
-Plus_mred_of_Plus_red1
-
-
-
-
-mred_full_comp_pure
-
-mred_full_comp_pure
-
-
-
-
-Plus_mred_of_Plus_red1->mred_full_comp_pure
-
-
-
-mred_plus_one
-
-mred_plus_one
-
-
-
-
-Plus_red1_context
-
-Plus_red1_context
-
-
-
-
-lemma_2_3_beta_sim
-
-lemma_2_3_beta_sim
-
-
-
-
-Plus_red1_context->lemma_2_3_beta_sim
-
-
-
-occurs_count_zero
-
-occurs_count_zero
-
-
-
-
-occurs_count_pos
-
-occurs_count_pos
-
-
-
-
-occurs_count_zero->occurs_count_pos
-
-
-
-occurs_count_zero->full_comp_aux
-
-
-
-occurs_count_zero->full_comp_aux_sub
-
-
-
-occurs_count_false
-
-occurs_count_false
-
-
-
-
-occurs_count_zfill_plug
-
-occurs_count_zfill_plug
-
-
-
-
-occurs_count_false->occurs_count_zfill_plug
-
-
-
-occurs_lift_self
-
-occurs_lift_self
-
-
-
-
-occurs_lift_self->occurs_count_zfill_plug
-
-
-
-occurs_lift_self->open_rec_zplug_lift
-
-
-
-zdecs_nonempty
-
-zdecs_nonempty
-
-
-
-
-zdecs_nonempty->full_comp_aux
-
-
-
-zdecs_nonempty->full_comp_aux_sub
-
-
-
-occurs_count_zfill_plug->full_comp_aux
-
-
-
-occurs_count_zfill_plug->full_comp_aux_sub
-
-
-
-open_rec_zplug_lift->full_comp_aux
-
-
-
-open_rec_zplug_lift->full_comp_aux_sub
-
-
-
-lemma_2_2_full_comp
-
-lemma_2_2_full_comp
-
-
-
-
-full_comp_aux->lemma_2_2_full_comp
-
-
-
-lemma_2_2_full_comp->mred_full_comp_pure
-
-
-
-lemma_2_2_full_comp->lemma_2_3_beta_sim
-
-
-
-red1_root_fv
-
-red1_root_fv
-
-
-
-
-fvs_zplug_lift->red1_root_fv
-
-
-
-plug_fv_mono
-
-plug_fv_mono
-
-
-
-
-red1r_fv
-
-red1r_fv
-
-
-
-
-plug_fv_mono->red1r_fv
-
-
-
-red1_root_fv->red1r_fv
-
-
-
-lemma_2_1_fv_preserved
-
-lemma_2_1_fv_preserved
-
-
-
-
-red1r_fv->lemma_2_1_fv_preserved
-
-
-
-gen_fv_preserved
-
-gen_fv_preserved
-
-
-
-
-lemma_2_1_fv_preserved->gen_fv_preserved
-
-
-
-corpus_fv_preserved
-
-corpus_fv_preserved
-
-
-
-
-lemma_2_1_fv_preserved->corpus_fv_preserved
-
-
-
-Plus_trans
-
-Plus_trans
-
-
-
-
-Plus_step_trans
-
-Plus_step_trans
-
-
-
-
-isubst_meta_in
-
-isubst_meta_in
-
-
-
-
-isubst_meta_notin
-
-isubst_meta_notin
-
-
-
-
-eqC_in_Es
-
-eqC_in_Es
-
-
-
-
-Es_ctx_any
-
-Es_ctx_any
-
-
-
-
-nred_R_intro
-
-nred_R_intro
-
-
-
-
-Es_refl_any
-
-Es_refl_any
-
-
-
-
-Es_sym_any
-
-Es_sym_any
-
-
-
-
-Es_trans_any
-
-Es_trans_any
-
-
-
-
-in_filter_neq
-
-in_filter_neq
-
-
-
-
-nplug_fv_mono
-
-nplug_fv_mono
-
-
-
-
-in_filter_neq->nplug_fv_mono
-
-
-
-nplug_fv_upper
-
-nplug_fv_upper
-
-
-
-
-in_filter_neq->nplug_fv_upper
-
-
-
-nred_core_fv
-
-nred_core_fv
-
-
-
-
-in_filter_neq->nred_core_fv
-
-
-
-nplug_esub_fv
-
-nplug_esub_fv
-
-
-
-
-in_filter_neq->nplug_esub_fv
-
-
-
-nred_fv
-
-nred_fv
-
-
-
-
-in_filter_neq->nred_fv
-
-
-
-filter_neq_in
-
-filter_neq_in
-
-
-
-
-filter_neq_in->nplug_fv_mono
-
-
-
-filter_neq_in->nplug_fv_upper
-
-
-
-filter_neq_in->nred_core_fv
-
-
-
-filter_neq_in->nplug_esub_fv
-
-
-
-filter_neq_in->nred_fv
-
-
-
-nplug_fv_mono->nred_core_fv
-
-
-
-nplug_fv_mono->nred_fv
-
-
-
-Es_fv_both
-
-Es_fv_both
-
-
-
-
-nplug_fv_mono->Es_fv_both
-
-
-
-nplug_fv_upper->nred_core_fv
-
-
-
-nplug_fv_upper->nred_fv
-
-
-
-nplug_esub_fv->nred_fv
-
-
-
-in_filter_neq_iff
-
-in_filter_neq_iff
-
-
-
-
-in_filter_neq_iff->Es_fv_both
-
-
-
-Es_fv
-
-Es_fv
-
-
-
-
-Es_fv_both->Es_fv
-
-
-
-par_red1_iff
-
-par_red1_iff
-
-
-
-
-par_to_red1_or_eq
-
-par_to_red1_or_eq
-
-
-
-
-par_red1_iff->par_to_red1_or_eq
-
-
-
-red1_or_eq_to_par
-
-red1_or_eq_to_par
-
-
-
-
-par_red1_iff->red1_or_eq_to_par
-
-
-
-red1_in_par
-
-red1_in_par
-
-
-
-
-par_context
-
-par_context
-
-
-
-
-par_reflexive
-
-par_reflexive
-
-
-
-
-gen_list_length
-
-gen_list_length
-
-
-
-
-check_term_true
-
-check_term_true
-
-
-
-
-check_all_true
-
-check_all_true
-
-
-
-
-check_term_true->check_all_true
-
-
-
-check_all_true->enumerate_check
-
-
-
-gen_sound
-
-gen_sound
-
-
-
-
-gen_complete
-
-gen_complete
-
-
-
-
-zdecs_sound
-
-zdecs_sound
-
-
-
-
-zdecs_sound->full_comp_aux
-
-
-
-root_steps_sound
-
-root_steps_sound
-
-
-
-
-zdecs_sound->root_steps_sound
-
-
-
-zdecs_sound->full_comp_aux_sub
-
-
-
-zdecs_complete
-
-zdecs_complete
-
-
-
-
-root_steps_complete
-
-root_steps_complete
-
-
-
-
-zdecs_complete->root_steps_complete
-
-
-
-positions_at
-
-positions_at
-
-
-
-
-steps_sound
-
-steps_sound
-
-
-
-
-positions_at->steps_sound
-
-
-
-root_steps_sound->steps_sound
-
-
-
-steps_complete
-
-steps_complete
-
-
-
-
-root_steps_complete->steps_complete
-
-
-
-steps_sound->enumerate_sound
-
-
-
-steps_sound->gen_sound
-
-
-
-steps_sound_red1
-
-steps_sound_red1
-
-
-
-
-steps_sound->steps_sound_red1
-
-
-
-has_red_spec
-
-has_red_spec
-
-
-
-
-steps_sound->has_red_spec
-
-
-
-corpus_sound
-
-corpus_sound
-
-
-
-
-steps_sound->corpus_sound
-
-
-
-steps_sound_red1->check_term_true
-
-
-
-steps_sound_red1->gen_fv_preserved
-
-
-
-nf_iff_steps_nil
-
-nf_iff_steps_nil
-
-
-
-
-steps_sound_red1->nf_iff_steps_nil
-
-
-
-steps_sound_red1->corpus_fv_preserved
-
-
-
-positions_hole
-
-positions_hole
-
-
-
-
-root_steps_in_steps
-
-root_steps_in_steps
-
-
-
-
-positions_hole->root_steps_in_steps
-
-
-
-root_steps_in_steps->steps_complete
-
-
-
-plug_comp
-
-plug_comp
-
-
-
-
-plug_comp->steps_complete
-
-
-
-positions_comp
-
-positions_comp
-
-
-
-
-positions_comp->steps_complete
-
-
-
-at_ctx_comp
-
-at_ctx_comp
-
-
-
-
-at_ctx_comp->steps_complete
-
-
-
-steps_complete->enumerate_complete
-
-
-
-steps_complete->gen_complete
-
-
-
-steps_complete->has_red_spec
-
-
-
-steps_complete->nf_iff_steps_nil
-
-
-
-corpus_complete
-
-corpus_complete
-
-
-
-
-steps_complete->corpus_complete
-
-
-
-has_red_f
-
-has_red_f
-
-
-
-
-has_red_f->has_red_spec
-
-
-
-has_red_spec->check_term_true
-
-
-
-red1_dec
-
-red1_dec
-
-
-
-
-has_red_spec->red1_dec
-
-
-
-corpus_decides
-
-corpus_decides
-
-
-
-
-has_red_spec->corpus_decides
-
-
-
-normal_form_iff_nf
-
-normal_form_iff_nf
-
-
-
-
-nf_iff_steps_nil->normal_form_iff_nf
-
-
-
-nf_dec
-
-nf_dec
-
-
-
-
-nf_iff_steps_nil->nf_dec
-
-
-
-open_rec_app
-
-open_rec_app
-
-
-
-
-open_rec_lam
-
-open_rec_lam
-
-
-
-
-open_rec_esub
-
-open_rec_esub
-
-
-
-
-close_rec_app
-
-close_rec_app
-
-
-
-
-close_rec_lam
-
-close_rec_lam
-
-
-
-
-close_rec_esub
-
-close_rec_esub
-
-
-
-
-subst_app
-
-subst_app
-
-
-
-
-subst_lam
-
-subst_lam
-
-
-
-
-subst_esub
-
-subst_esub
-
-
-
-
-open_rec_lc_atom
-
-open_rec_lc_atom
-
-
-
-
-open_rec_lc
-
-open_rec_lc
-
-
-
-
-open_rec_lc_atom->open_rec_lc
-
-
-
-red_sub_root_to_red1
-
-red_sub_root_to_red1
-
-
-
-
-red_sub_to_red1
-
-red_sub_to_red1
-
-
-
-
-red_sub_root_to_red1->red_sub_to_red1
-
-
-
-red_sub_context
-
-red_sub_context
-
-
-
-
-Star_red_sub_context
-
-Star_red_sub_context
-
-
-
-
-red_sub_context->Star_red_sub_context
-
-
-
-red_sub_gc
-
-red_sub_gc
-
-
-
-
-red_sub_gc->full_comp_aux_sub
-
-
-
-red_gc_to_red_sub
-
-red_gc_to_red_sub
-
-
-
-
-red_sub_gc->red_gc_to_red_sub
-
-
-
-red_sub_r
-
-red_sub_r
-
-
-
-
-red_sub_r->full_comp_aux_sub
-
-
-
-occurs_zfill
-
-occurs_zfill
-
-
-
-
-zfill_occurs0
-
-zfill_occurs0
-
-
-
-
-occurs_zfill->zfill_occurs0
-
-
-
-R_Gc_disjoint
-
-R_Gc_disjoint
-
-
-
-
-zfill_occurs0->R_Gc_disjoint
-
-
-
-plus_red_sub_full_comp
-
-plus_red_sub_full_comp
-
-
-
-
-full_comp_aux_sub->plus_red_sub_full_comp
-
-
-
-plus_red_sub_full_comp->star_red_sub_full_comp
-
-
-
-es_count_plug_mono
-
-es_count_plug_mono
-
-
-
-
-red_gc_measure
-
-red_gc_measure
-
-
-
-
-es_count_plug_mono->red_gc_measure
-
-
-
-red_gc_terminates
-
-red_gc_terminates
-
-
-
-
-red_gc_measure->red_gc_terminates
-
-
-
diff --git a/graphs/dune b/graphs/dune
index 6913097..f4963a2 100644
--- a/graphs/dune
+++ b/graphs/dune
@@ -6,9 +6,24 @@
(source_tree ../theory))
(targets
theorems.json
- dependency.dot
- dependency.svg
- dependency.png
+ dependency-overview.dot
+ dependency-overview.svg
+ dependency-overview.png
+ dependency-M1.dot
+ dependency-M1.svg
+ dependency-M1.png
+ dependency-M2.dot
+ dependency-M2.svg
+ dependency-M2.png
+ dependency-M3.dot
+ dependency-M3.svg
+ dependency-M3.png
+ dependency-M4.dot
+ dependency-M4.svg
+ dependency-M4.png
+ dependency-M5.dot
+ dependency-M5.svg
+ dependency-M5.png
rules.dot
rules.svg
rules.png
diff --git a/graphs/index.txt b/graphs/index.txt
index 331c76b..1c1ab31 100644
--- a/graphs/index.txt
+++ b/graphs/index.txt
@@ -1,42 +1,4 @@
status milestone kind name file
-proved M0 infra Es_ctx_any theory/NamedMeta.v
-proved M0 infra Es_fv theory/NamedMeta.v
-proved M0 infra Es_fv_both theory/NamedMeta.v
-proved M0 infra Es_refl_any theory/NamedMeta.v
-proved M0 infra Es_sym_any theory/NamedMeta.v
-proved M0 infra Es_trans_any theory/NamedMeta.v
-proved M0 infra Plus_mred_of_Plus_red1 theory/Metaterm.v
-proved M0 infra eqC_in_Es theory/NamedMeta.v
-proved M0 infra filter_neq_in theory/NamedMeta.v
-proved M0 infra in_filter_neq theory/NamedMeta.v
-proved M0 infra in_filter_neq_iff theory/NamedMeta.v
-proved M0 infra isubst_meta_in theory/NamedMeta.v
-proved M0 infra isubst_meta_notin theory/NamedMeta.v
-proved M0 infra mfvs_close_m theory/Metaterm.v
-proved M0 infra mfvs_lift_m theory/Metaterm.v
-proved M0 infra mfvs_open_m theory/Metaterm.v
-proved M0 infra mred_B_intro theory/Metaterm.v
-proved M0 infra mred_context theory/Metaterm.v
-proved M0 infra mred_full_comp_pure theory/Metaterm.v
-proved M0 infra mred_gc_intro theory/Metaterm.v
-proved M0 infra mred_of_red1 theory/Metaterm.v
-proved M0 infra mred_plus_one theory/Metaterm.v
-proved M0 infra mred_r_intro theory/Metaterm.v
-proved M0 infra mred_term_context theory/Metaterm.v
-proved M0 infra nplug_esub_fv theory/NamedMeta.v
-proved M0 infra nplug_fv_mono theory/NamedMeta.v
-proved M0 infra nplug_fv_upper theory/NamedMeta.v
-proved M0 infra nred_R_intro theory/NamedMeta.v
-proved M0 infra nred_core_fv theory/NamedMeta.v
-proved M0 infra nred_fv theory/NamedMeta.v
-proved M0 infra of_trm_close theory/Metaterm.v
-proved M0 infra of_trm_fvs theory/Metaterm.v
-proved M0 infra of_trm_injective theory/Metaterm.v
-proved M0 infra of_trm_lift theory/Metaterm.v
-proved M0 infra of_trm_moccurs theory/Metaterm.v
-proved M0 infra of_trm_moccurs0 theory/Metaterm.v
-proved M0 infra of_trm_open theory/Metaterm.v
-proved M0 infra of_trm_plug theory/Metaterm.v
proved M1 infra at_ctx_comp theory/Reduction.v
proved M1 infra close_rec_fvar theory/Binding.v
proved M1 infra close_rec_fvs theory/Binding.v
@@ -145,3 +107,72 @@ proved M4 infra par_reflexive theory/Parallel.v
proved M4 infra par_to_red1_or_eq theory/Parallel.v
proved M4 infra red1_in_par theory/Parallel.v
proved M4 infra red1_or_eq_to_par theory/Parallel.v
+proved M5 infra A1_C_related theory/NamedMeasure.v
+proved M5 infra A1_Mx_differ theory/NamedMeasure.v
+proved M5 infra A1_not_invariant theory/NamedMeasure.v
+proved M5 infra A1_s_differ theory/NamedMeasure.v
+proved M5 infra Es_ctx_any theory/NamedMeta.v
+proved M5 infra Es_fv theory/NamedMeta.v
+proved M5 infra Es_fv_both theory/NamedMeta.v
+proved M5 infra Es_refl_any theory/NamedMeta.v
+proved M5 infra Es_sym_any theory/NamedMeta.v
+proved M5 infra Es_trans_any theory/NamedMeta.v
+proved M5 infra Gc_special_nondecrease theory/NamedMeasure.v
+proved M5 infra Mx_fresh_fails theory/NamedMeasure.v
+proved M5 infra Mx_ge_0 theory/NamedMeasure.v
+proved M5 infra PlusN_to_StarN theory/NamedEs.v
+proved M5 infra Plus_mred_of_Plus_red1 theory/Metaterm.v
+proved M5 infra StarN_one_trans theory/NamedEs.v
+proved M5 infra StarN_subred_context theory/NamedEs.v
+proved M5 infra StarN_trans theory/NamedEs.v
+proved M5 infra current_sm_not_terminating theory/NamedMeasure.v
+proved M5 infra current_subred_not_terminating theory/NamedMeasure.v
+proved M5 infra eqC_in_Es theory/NamedMeta.v
+proved M5 infra filter_neq_in theory/NamedMeta.v
+proved M5 infra head_has_pos theory/NamedMeasure.v
+proved M5 infra in_filter_neq theory/NamedMeta.v
+proved M5 infra in_filter_neq_iff theory/NamedMeta.v
+proved M5 infra isubst_meta_in theory/NamedMeta.v
+proved M5 infra isubst_meta_notin theory/NamedMeta.v
+proved M5 infra le_mul_of_one_le theory/NamedMeasure.v
+proved M5 infra mfvs_close_m theory/Metaterm.v
+proved M5 infra mfvs_lift_m theory/Metaterm.v
+proved M5 infra mfvs_open_m theory/Metaterm.v
+proved M5 infra mred_B_intro theory/Metaterm.v
+proved M5 infra mred_context theory/Metaterm.v
+proved M5 infra mred_full_comp_pure theory/Metaterm.v
+proved M5 infra mred_gc_intro theory/Metaterm.v
+proved M5 infra mred_of_red1 theory/Metaterm.v
+proved M5 infra mred_plus_one theory/Metaterm.v
+proved M5 infra mred_r_intro theory/Metaterm.v
+proved M5 infra mred_term_context theory/Metaterm.v
+proved M5 infra nfv_annot_bound_example theory/NamedMeasure.v
+proved M5 infra nocc_le_Mx theory/NamedMeasure.v
+proved M5 infra nplug_esub_fv theory/NamedMeta.v
+proved M5 infra nplug_fv_mono theory/NamedMeta.v
+proved M5 infra nplug_fv_upper theory/NamedMeta.v
+proved M5 infra nred_Gc_special theory/NamedMeasure.v
+proved M5 infra nred_R_intro theory/NamedMeta.v
+proved M5 infra nred_R_selfloop theory/NamedMeasure.v
+proved M5 infra nred_core_fv theory/NamedMeta.v
+proved M5 infra nred_fv theory/NamedMeta.v
+proved M5 infra nred_stable_source theory/NamedEs.v
+proved M5 infra nred_stable_target theory/NamedEs.v
+proved M5 infra of_trm_close theory/Metaterm.v
+proved M5 infra of_trm_fvs theory/Metaterm.v
+proved M5 infra of_trm_injective theory/Metaterm.v
+proved M5 infra of_trm_lift theory/Metaterm.v
+proved M5 infra of_trm_moccurs theory/Metaterm.v
+proved M5 infra of_trm_moccurs0 theory/Metaterm.v
+proved M5 infra of_trm_open theory/Metaterm.v
+proved M5 infra of_trm_plug theory/Metaterm.v
+proved M5 infra s_metavar_empty theory/NamedMeasure.v
+proved M5 infra subred_Es_l theory/NamedEs.v
+proved M5 infra subred_Es_lr theory/NamedEs.v
+proved M5 infra subred_Es_r theory/NamedEs.v
+proved M5 infra subred_context theory/NamedEs.v
+proved M5 infra subred_context_rule theory/NamedEs.v
+proved M5 infra subred_intro theory/NamedEs.v
+proved M5 infra subred_nred theory/NamedEs.v
+proved M5 infra subred_of_Es_nred_Es theory/NamedEs.v
+proved M5 infra subred_selfloop theory/NamedMeasure.v
diff --git a/graphs/reduction.dot b/graphs/reduction.dot
index 2115012..4ee708f 100644
--- a/graphs/reduction.dot
+++ b/graphs/reduction.dot
@@ -1,20 +1,20 @@
digraph reduction_dup {
rankdir=LR;
- bgcolor="white";
- node [fontname=Inter, fontsize=10];
- edge [fontname=Inter, fontsize=9, color="#333333"];
- graph [labelloc=t, fontcolor="#333333", label="(lambda x. x x) y reduction graph"];
- n0 [label="(lambda x. x x) y", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"];
- n1 [label="(x x)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"];
- n2 [label="(y x)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"];
- n2b [label="(x y)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"];
- n3 [label="(y y)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"];
- nf [label="y y (normal form)", shape=doublecircle, style=filled, fillcolor="#d9ead3", color="#38761d", fontcolor="#333333"];
- n0 -> n1 [label="B", color="#990000"];
- n1 -> n2 [label="R", color="#674ea7"];
- n1 -> n2b [label="R", color="#674ea7"];
- n2 -> n3 [label="R", color="#674ea7"];
- n2b -> n3 [label="R", color="#674ea7"];
- n3 -> nf [label="Gc", color="#38761d"];
+ bgcolor="#ffffff";
+ node [fontname=Inter, fontsize=10, fontcolor="#000000"];
+ edge [fontname=Inter, fontsize=9, color="#000000", fontcolor="#000000"];
+ graph [labelloc=t, fontcolor="#000000", label="(lambda x. x x) y reduction graph"];
+ n0 [label="(lambda x. x x) y", shape=box, style="filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ n1 [label="(x x)[x/y]", shape=box, style="filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ n2 [label="(y x)[x/y]", shape=box, style="filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ n2b [label="(x y)[x/y]", shape=box, style="filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ n3 [label="(y y)[x/y]", shape=box, style="filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ nf [label="y y (normal form)", shape=doublecircle, style=filled, fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ n0 -> n1 [label="B", color="#000000"];
+ n1 -> n2 [label="R", color="#000000"];
+ n1 -> n2b [label="R", color="#000000"];
+ n2 -> n3 [label="R", color="#000000"];
+ n2b -> n3 [label="R", color="#000000"];
+ n3 -> nf [label="Gc", color="#000000"];
{rank=same; n2; n2b;}
}
diff --git a/graphs/reduction.png b/graphs/reduction.png
index 951435e..85a7792 100644
Binary files a/graphs/reduction.png and b/graphs/reduction.png differ
diff --git a/graphs/reduction.svg b/graphs/reduction.svg
index fcb47ca..3647749 100644
--- a/graphs/reduction.svg
+++ b/graphs/reduction.svg
@@ -4,90 +4,90 @@
-
-
+
+
reduction_dup
-(lambda x. x x) y reduction graph
+(lambda x. x x) y reduction graph
n0
-(lambda x. x x) y
+(lambda x. x x) y
n1
-(x x)[x/y]
+(x x)[x/y]
n0->n1
-B
+B
n2
-(y x)[x/y]
+(y x)[x/y]
n1->n2
-R
+R
n2b
-(x y)[x/y]
+(x y)[x/y]
n1->n2b
-R
+R
n3
-(y y)[x/y]
+(y y)[x/y]
n2->n3
-R
+R
n2b->n3
-R
+R
nf
-y y (normal form)
+y y (normal form)
n3->nf
-Gc
+Gc
diff --git a/graphs/rules.dot b/graphs/rules.dot
index c0054d6..a577aef 100644
--- a/graphs/rules.dot
+++ b/graphs/rules.dot
@@ -1,19 +1,19 @@
digraph lambda_sub_cfg {
rankdir=TB;
- bgcolor="white";
- node [fontname=Inter, fontsize=10];
- edge [fontname=Inter, fontsize=9, color="#333333"];
- start [label="term", shape=oval, style=filled, fillcolor="#f3f3f3", color="#333333"];
- beta [label="(lambda x. t) u", shape=box, style="rounded,filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"];
- es [label="t[x/u]", shape=box, style="rounded,filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"];
- pure [label="pure term", shape=oval, style=filled, fillcolor="#f3f3f3", color="#333333"];
- nf [label="normal form", shape=doublecircle, style=filled, fillcolor="#d9ead3", color="#38761d"];
+ bgcolor="#ffffff";
+ node [fontname=Inter, fontsize=10, fontcolor="#000000"];
+ edge [fontname=Inter, fontsize=9, color="#000000", fontcolor="#000000"];
+ start [label="term", shape=oval, style=filled, fillcolor="#ffffff", color="#000000"];
+ beta [label="(lambda x. t) u", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ es [label="t[x/u]", shape=box, style="rounded,filled", fillcolor="#ffffff", color="#000000", fontcolor="#000000"];
+ pure [label="pure term", shape=oval, style=filled, fillcolor="#ffffff", color="#000000"];
+ nf [label="normal form", shape=doublecircle, style=filled, fillcolor="#ffffff", color="#000000"];
start -> beta [label="App(Lam,_)"];
start -> es [label="ESub"];
start -> pure [label="BVar/FVar/Lam"];
- beta -> es [label="B", color="#990000"];
- es -> es [label="R (one occurrence)", color="#674ea7"];
- es -> pure [label="Gc (x not in fv)", color="#38761d"];
- pure -> pure [label="B under context", color="#990000"];
- es -> nf [label="R/Gc normalisation", color="#674ea7"];
+ beta -> es [label="B", color="#000000"];
+ es -> es [label="R (one occurrence)", color="#000000"];
+ es -> pure [label="Gc (x not in fv)", color="#000000"];
+ pure -> pure [label="B under context", color="#000000"];
+ es -> nf [label="R/Gc normalisation", color="#000000"];
}
diff --git a/graphs/rules.png b/graphs/rules.png
index cb48afa..f3c3870 100644
Binary files a/graphs/rules.png and b/graphs/rules.png differ
diff --git a/graphs/rules.svg b/graphs/rules.svg
index a051cf0..450b18d 100644
--- a/graphs/rules.svg
+++ b/graphs/rules.svg
@@ -4,97 +4,97 @@
-
-
+
+
lambda_sub_cfg
-
start
-term
+term
beta
-(lambda x. t) u
+(lambda x. t) u
start->beta
-App(Lam,_)
+App(Lam,_)
es
-t[x/u]
+t[x/u]
start->es
-ESub
+ESub
pure
-pure term
+pure term
start->pure
-BVar/FVar/Lam
+BVar/FVar/Lam
beta->es
-B
+B
es->es
-R (one occurrence)
+R (one occurrence)
es->pure
-Gc (x not in fv)
+Gc (x not in fv)
nf
-normal form
+normal form
es->nf
-R/Gc normalisation
+R/Gc normalisation
pure->pure
-B under context
+B under context
diff --git a/graphs/theorems.json b/graphs/theorems.json
index 7f6769c..71e02e8 100644
--- a/graphs/theorems.json
+++ b/graphs/theorems.json
@@ -9,13 +9,13 @@
"html": "https://arxiv.org/html/2312.13270v1"
},
"milestones": [
- "M0",
"M1",
"M2",
"M3",
- "M4"
+ "M4",
+ "M5"
],
- "current": "M4",
+ "current": "M5",
"nodes": [
{
"id": "fvs_lift",
@@ -294,7 +294,7 @@
"label": "of_trm_fvs",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -304,7 +304,7 @@
"label": "of_trm_lift",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -314,7 +314,7 @@
"label": "of_trm_open",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": [
@@ -326,7 +326,7 @@
"label": "of_trm_close",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -336,7 +336,7 @@
"label": "of_trm_injective",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -346,7 +346,7 @@
"label": "mfvs_lift_m",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -356,7 +356,7 @@
"label": "mfvs_close_m",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -366,7 +366,7 @@
"label": "mfvs_open_m",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": [
@@ -378,7 +378,7 @@
"label": "of_trm_plug",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -388,7 +388,7 @@
"label": "mred_of_red1",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -398,7 +398,7 @@
"label": "mred_context",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -408,7 +408,7 @@
"label": "mred_term_context",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": [
@@ -420,7 +420,7 @@
"label": "of_trm_moccurs",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -430,7 +430,7 @@
"label": "of_trm_moccurs0",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": [
@@ -442,7 +442,7 @@
"label": "mred_B_intro",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -452,7 +452,7 @@
"label": "mred_gc_intro",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -462,7 +462,7 @@
"label": "mred_r_intro",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -472,7 +472,7 @@
"label": "Plus_mred_of_Plus_red1",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -482,7 +482,7 @@
"label": "mred_full_comp_pure",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": [
@@ -495,7 +495,7 @@
"label": "mred_plus_one",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/Metaterm.v",
"depends": []
@@ -709,12 +709,359 @@
"file": "theory/Metatheory.v",
"depends": []
},
+ {
+ "id": "subred_intro",
+ "label": "subred_intro",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": []
+ },
+ {
+ "id": "subred_nred",
+ "label": "subred_nred",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_intro"
+ ]
+ },
+ {
+ "id": "subred_Es_l",
+ "label": "subred_Es_l",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_intro"
+ ]
+ },
+ {
+ "id": "subred_Es_r",
+ "label": "subred_Es_r",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_intro"
+ ]
+ },
+ {
+ "id": "subred_Es_lr",
+ "label": "subred_Es_lr",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_Es_l",
+ "subred_Es_r"
+ ]
+ },
+ {
+ "id": "subred_context",
+ "label": "subred_context",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_intro"
+ ]
+ },
+ {
+ "id": "subred_context_rule",
+ "label": "subred_context_rule",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_context",
+ "subred_nred"
+ ]
+ },
+ {
+ "id": "subred_of_Es_nred_Es",
+ "label": "subred_of_Es_nred_Es",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_intro"
+ ]
+ },
+ {
+ "id": "nred_stable_source",
+ "label": "nred_stable_source",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_intro"
+ ]
+ },
+ {
+ "id": "nred_stable_target",
+ "label": "nred_stable_target",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_intro"
+ ]
+ },
+ {
+ "id": "StarN_trans",
+ "label": "StarN_trans",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": []
+ },
+ {
+ "id": "StarN_one_trans",
+ "label": "StarN_one_trans",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": []
+ },
+ {
+ "id": "PlusN_to_StarN",
+ "label": "PlusN_to_StarN",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": []
+ },
+ {
+ "id": "StarN_subred_context",
+ "label": "StarN_subred_context",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedEs.v",
+ "depends": [
+ "subred_context"
+ ]
+ },
+ {
+ "id": "Mx_ge_0",
+ "label": "Mx_ge_0",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "head_has_pos",
+ "label": "head_has_pos",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "le_mul_of_one_le",
+ "label": "le_mul_of_one_le",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "nocc_le_Mx",
+ "label": "nocc_le_Mx",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": [
+ "head_has_pos",
+ "le_mul_of_one_le"
+ ]
+ },
+ {
+ "id": "nfv_annot_bound_example",
+ "label": "nfv_annot_bound_example",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "Mx_fresh_fails",
+ "label": "Mx_fresh_fails",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": [
+ "nfv_annot_bound_example"
+ ]
+ },
+ {
+ "id": "A1_C_related",
+ "label": "A1_C_related",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "A1_s_differ",
+ "label": "A1_s_differ",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "A1_Mx_differ",
+ "label": "A1_Mx_differ",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "A1_not_invariant",
+ "label": "A1_not_invariant",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": [
+ "A1_C_related",
+ "A1_s_differ"
+ ]
+ },
+ {
+ "id": "Gc_special_nondecrease",
+ "label": "Gc_special_nondecrease",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "nred_Gc_special",
+ "label": "nred_Gc_special",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "s_metavar_empty",
+ "label": "s_metavar_empty",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "nred_R_selfloop",
+ "label": "nred_R_selfloop",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": []
+ },
+ {
+ "id": "current_sm_not_terminating",
+ "label": "current_sm_not_terminating",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": [
+ "nred_R_selfloop"
+ ]
+ },
+ {
+ "id": "subred_selfloop",
+ "label": "subred_selfloop",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": [
+ "nred_R_selfloop",
+ "subred_nred"
+ ]
+ },
+ {
+ "id": "current_subred_not_terminating",
+ "label": "current_subred_not_terminating",
+ "kind": "infra",
+ "status": "proved",
+ "milestone": "M5",
+ "section": "",
+ "file": "theory/NamedMeasure.v",
+ "depends": [
+ "subred_selfloop"
+ ]
+ },
{
"id": "isubst_meta_in",
"label": "isubst_meta_in",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -724,7 +1071,7 @@
"label": "isubst_meta_notin",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -734,7 +1081,7 @@
"label": "eqC_in_Es",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -744,7 +1091,7 @@
"label": "Es_ctx_any",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -754,7 +1101,7 @@
"label": "nred_R_intro",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -764,7 +1111,7 @@
"label": "Es_refl_any",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -774,7 +1121,7 @@
"label": "Es_sym_any",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -784,7 +1131,7 @@
"label": "Es_trans_any",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -794,7 +1141,7 @@
"label": "in_filter_neq",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -804,7 +1151,7 @@
"label": "filter_neq_in",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -814,7 +1161,7 @@
"label": "nplug_fv_mono",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": [
@@ -827,7 +1174,7 @@
"label": "nplug_fv_upper",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": [
@@ -840,7 +1187,7 @@
"label": "nred_core_fv",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": [
@@ -855,7 +1202,7 @@
"label": "nplug_esub_fv",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": [
@@ -868,7 +1215,7 @@
"label": "nred_fv",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": [
@@ -884,7 +1231,7 @@
"label": "in_filter_neq_iff",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": []
@@ -894,7 +1241,7 @@
"label": "Es_fv_both",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": [
@@ -907,7 +1254,7 @@
"label": "Es_fv",
"kind": "infra",
"status": "proved",
- "milestone": "M0",
+ "milestone": "M5",
"section": "",
"file": "theory/NamedMeta.v",
"depends": [
diff --git a/scripts/audit.sh b/scripts/audit.sh
index 35692b5..3fcf4d4 100755
--- a/scripts/audit.sh
+++ b/scripts/audit.sh
@@ -35,7 +35,7 @@ done < <(find theory -name '*.v' -print0 2>/dev/null)
echo "== Print Assumptions =="
WORK="$(mktemp -d ./.audit-work.XXXXXX)"
cp theory/*.v "$WORK"/
-for f in ExecReducer Binding Reduction Metatheory Closure Subsystem Substitution Parallel Metaterm NamedMeta NamedEs Tests Random Enumerate; do
+for f in ExecReducer Binding Reduction Metatheory Closure Subsystem Substitution Parallel Metaterm NamedMeta NamedEs NamedMeasure Tests Random Enumerate; do
echo "-- $f"
out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
echo "$out"
diff --git a/scripts/gen_graphs.py b/scripts/gen_graphs.py
index 9e73456..029e001 100755
--- a/scripts/gen_graphs.py
+++ b/scripts/gen_graphs.py
@@ -9,28 +9,16 @@ ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
GRAPH_DIR = os.path.join(ROOT, "graphs")
META = os.path.join(GRAPH_DIR, "theorems.json")
-STATUS_FILL = {
- "proved": "#d9ead3",
- "stated": "#fff2cc",
- "planned": "#f3f3f3",
- "blocked": "#f4cccc",
-}
-STATUS_PEN = {
- "proved": "#38761d",
- "stated": "#b45f06",
- "planned": "#777777",
- "blocked": "#cc0000",
-}
-STATUS_STYLE = {
- "proved": "filled",
- "stated": "filled,dashed",
- "planned": "dashed",
- "blocked": "filled,bold",
-}
-INK = "#333333"
-RULE_B = "#990000"
-RULE_R = "#674ea7"
-RULE_G = "#38761d"
+INK = "#000000"
+MUTED = "#000000"
+FONT = "#000000"
+FILL = "#ffffff"
+EXT_FILL = "#ffffff"
+NF_FILL = "#ffffff"
+
+RULE_B = "#000000"
+RULE_R = "#000000"
+RULE_G = "#000000"
def q(s):
@@ -46,110 +34,146 @@ def esc_html(s):
return str(s).replace("&", "&").replace("<", "<").replace(">", ">")
-def dependency_dot(data):
- nodes = data["nodes"]
- by_id = {n["id"]: n for n in nodes}
- title = data["paper"]["title"] + " - theorem dependency (" + data["current"] + ")"
- legend = (
- "" + esc_html(title) + " "
- ""
- "proved "
- "stated "
- "planned "
- "blocked "
- " "
+def node_line(n, external=False):
+ if external:
+ label = n["id"] + "\\n(" + n["milestone"] + ")"
+ shape = "box"
+ style = "rounded,dashed,filled"
+ fill = EXT_FILL
+ color = MUTED
+ fontcolor = FONT
+ pen = 0.9
+ else:
+ label = n["id"]
+ shape = "box" if n["kind"] == "paper" else "ellipse"
+ style = "rounded,filled" if n["kind"] == "paper" else "filled"
+ fill = FILL
+ color = INK
+ fontcolor = FONT
+ pen = 1.0
+ tip = n["id"]
+ if n.get("section"):
+ tip += " (section " + n["section"] + ")"
+ if n.get("file"):
+ tip += " " + n["file"]
+ tip += " " + n["status"]
+ return (
+ " %s [label=%s, shape=%s, style=%s, fillcolor=%s, color=%s, "
+ "penwidth=%.1f, fontcolor=%s, tooltip=%s];"
+ % (n["id"], q(label), shape, q(style), q(fill), q(color), pen, q(fontcolor), q(tip))
)
- lines = [
- "digraph theorem_deps {",
+
+
+def dep_header(title):
+ return [
+ "digraph 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=<%s>];" % legend,
+ ' bgcolor="#ffffff";',
+ " splines=polyline;",
+ " concentrate=true;",
+ " nodesep=0.2;",
+ " ranksep=0.9;",
+ ' node [fontname=Inter, fontsize=9];',
+ ' edge [fontname=Inter, fontsize=8, color="%s", fontcolor="%s", arrowsize=0.6, penwidth=0.8];' % (MUTED, FONT),
+ ' graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="%s", label=<%s >];' % (FONT, esc_html(title)),
]
- for n in nodes:
- fill = STATUS_FILL.get(n["status"], "#f3f3f3")
- pen = STATUS_PEN.get(n["status"], "#777777")
- style = STATUS_STYLE.get(n["status"], "dashed")
- tip = n["id"]
- if n.get("section"):
- tip += " (section " + n["section"] + ")"
- if n.get("file"):
- tip += " " + n["file"]
- tip += " " + data["paper"]["html"]
- if n["kind"] == "paper":
- shape = "box"
- style = "rounded," + style
- else:
- shape = "ellipse"
- attrs = [
- "label=%s" % q(n["label"]),
- "color=%s" % q(pen),
- "fillcolor=%s" % q(fill),
- "style=%s" % q(style),
- "fontcolor=%s" % q("#222222"),
- "tooltip=%s" % q(tip),
- "shape=%s" % shape,
- ]
- lines.append(" %s [%s];" % (n["id"], ", ".join(attrs)))
- for n in nodes:
- for d in n.get("depends", []):
+
+
+def dependency_overview_dot(data):
+ by_id = {n["id"]: n for n in data["nodes"]}
+ counts = {}
+ for n in data["nodes"]:
+ counts[n["milestone"]] = counts.get(n["milestone"], 0) + 1
+ milestones = [m for m in data["milestones"] if counts.get(m)]
+ edges = set()
+ for n in data["nodes"]:
+ for d in n["depends"]:
if d in by_id:
+ a = by_id[d]["milestone"]
+ b = n["milestone"]
+ if a != b and a in counts and b in counts:
+ edges.add((a, b))
+ lines = dep_header("Theorem dependency by milestone")
+ for m in milestones:
+ label = "%s\\n%d results" % (m, counts[m])
+ lines.append(
+ ' %s [label=%s, shape=box, style="rounded,filled", fillcolor=%s, '
+ "color=%s, fontcolor=%s];" % (m, q(label), q(FILL), q(INK), q(FONT))
+ )
+ for a, b in sorted(edges):
+ lines.append(" %s -> %s;" % (a, b))
+ lines.append("}")
+ return "\n".join(lines) + "\n"
+
+
+def dependency_subset_dot(data, title, keep_ids):
+ by_id = {n["id"]: n for n in data["nodes"]}
+ inside = [n for n in data["nodes"] if n["id"] in keep_ids]
+ ids = {n["id"] for n in inside}
+ ext_ids = sorted(
+ {d for n in inside for d in n["depends"] if d not in ids and d in by_id}
+ )
+ lines = dep_header(title)
+ for d in ext_ids:
+ lines.append(node_line(by_id[d], external=True))
+ for n in sorted(inside, key=lambda x: (x["file"], x["id"])):
+ lines.append(node_line(n))
+ keep = ids | set(ext_ids)
+ for n in inside:
+ for d in n["depends"]:
+ if d in keep:
lines.append(" %s -> %s;" % (d, n["id"]))
lines.append("}")
return "\n".join(lines) + "\n"
def rules_dot():
- box = 'shape=box, style="rounded,filled", fillcolor="#f5f5f5", color="%s", fontcolor="%s"' % (INK, INK)
+ box = 'shape=box, style="rounded,filled", fillcolor="%s", color="%s", fontcolor="%s"' % (FILL, INK, FONT)
lines = [
"digraph lambda_sub_cfg {",
" rankdir=TB;",
- " bgcolor=\"white\";",
- " node [fontname=Inter, fontsize=10];",
- " edge [fontname=Inter, fontsize=9, color=\"%s\"];" % INK,
- " start [label=\"term\", shape=oval, style=filled, fillcolor=\"#f3f3f3\", color=\"%s\"];" % INK,
+ ' bgcolor="#ffffff";',
+ ' node [fontname=Inter, fontsize=10, fontcolor="%s"];' % FONT,
+ ' edge [fontname=Inter, fontsize=9, color="%s", fontcolor="%s"];' % (MUTED, FONT),
+ ' start [label="term", shape=oval, style=filled, fillcolor="%s", color="%s"];' % (FILL, INK),
" beta [label=\"(lambda x. t) u\", %s];" % box,
" es [label=\"t[x/u]\", %s];" % box,
- " pure [label=\"pure term\", shape=oval, style=filled, fillcolor=\"#f3f3f3\", color=\"%s\"];" % INK,
- " nf [label=\"normal form\", shape=doublecircle, style=filled, fillcolor=\"#d9ead3\", color=\"%s\"];" % RULE_G,
- " start -> beta [label=\"App(Lam,_)\"];",
- " start -> es [label=\"ESub\"];",
- " start -> pure [label=\"BVar/FVar/Lam\"];",
- " beta -> es [label=\"B\", color=\"%s\"];" % RULE_B,
- " es -> es [label=\"R (one occurrence)\", color=\"%s\"];" % RULE_R,
- " es -> pure [label=\"Gc (x not in fv)\", color=\"%s\"];" % RULE_G,
- " pure -> pure [label=\"B under context\", color=\"%s\"];" % RULE_B,
- " es -> nf [label=\"R/Gc normalisation\", color=\"%s\"];" % RULE_R,
+ ' pure [label="pure term", shape=oval, style=filled, fillcolor="%s", color="%s"];' % (FILL, INK),
+ ' nf [label="normal form", shape=doublecircle, style=filled, fillcolor="%s", color="%s"];' % (NF_FILL, RULE_G),
+ ' start -> beta [label="App(Lam,_)"];',
+ ' start -> es [label="ESub"];',
+ ' start -> pure [label="BVar/FVar/Lam"];',
+ ' beta -> es [label="B", color="%s"];' % RULE_B,
+ ' es -> es [label="R (one occurrence)", color="%s"];' % RULE_R,
+ ' es -> pure [label="Gc (x not in fv)", color="%s"];' % RULE_G,
+ ' pure -> pure [label="B under context", color="%s"];' % RULE_B,
+ ' es -> nf [label="R/Gc normalisation", color="%s"];' % RULE_R,
"}",
]
return "\n".join(lines) + "\n"
def reduction_dot():
- box = 'shape=box, style="filled", fillcolor="#f5f5f5", color="%s", fontcolor="%s"' % (INK, INK)
+ box = 'shape=box, style="filled", fillcolor="%s", color="%s", fontcolor="%s"' % (FILL, INK, FONT)
lines = [
"digraph reduction_dup {",
" rankdir=LR;",
- " bgcolor=\"white\";",
- " node [fontname=Inter, fontsize=10];",
- " edge [fontname=Inter, fontsize=9, color=\"%s\"];" % INK,
- " graph [labelloc=t, fontcolor=\"%s\", label=\"(lambda x. x x) y reduction graph\"];" % INK,
+ ' bgcolor="#ffffff";',
+ ' node [fontname=Inter, fontsize=10, fontcolor="%s"];' % FONT,
+ ' edge [fontname=Inter, fontsize=9, color="%s", fontcolor="%s"];' % (MUTED, FONT),
+ ' graph [labelloc=t, fontcolor="%s", label="(lambda x. x x) y reduction graph"];' % FONT,
" n0 [label=\"(lambda x. x x) y\", %s];" % box,
" n1 [label=\"(x x)[x/y]\", %s];" % box,
" n2 [label=\"(y x)[x/y]\", %s];" % box,
" n2b [label=\"(x y)[x/y]\", %s];" % box,
" n3 [label=\"(y y)[x/y]\", %s];" % box,
- " nf [label=\"y y (normal form)\", shape=doublecircle, style=filled, fillcolor=\"#d9ead3\", color=\"%s\", fontcolor=\"%s\"];" % (RULE_G, INK),
- " n0 -> n1 [label=\"B\", color=\"%s\"];" % RULE_B,
- " n1 -> n2 [label=\"R\", color=\"%s\"];" % RULE_R,
- " n1 -> n2b [label=\"R\", color=\"%s\"];" % RULE_R,
- " n2 -> n3 [label=\"R\", color=\"%s\"];" % RULE_R,
- " n2b -> n3 [label=\"R\", color=\"%s\"];" % RULE_R,
- " n3 -> nf [label=\"Gc\", color=\"%s\"];" % RULE_G,
+ ' nf [label="y y (normal form)", shape=doublecircle, style=filled, fillcolor="%s", color="%s", fontcolor="%s"];' % (NF_FILL, RULE_G, FONT),
+ ' n0 -> n1 [label="B", color="%s"];' % RULE_B,
+ ' n1 -> n2 [label="R", color="%s"];' % RULE_R,
+ ' n1 -> n2b [label="R", color="%s"];' % RULE_R,
+ ' n2 -> n3 [label="R", color="%s"];' % RULE_R,
+ ' n2b -> n3 [label="R", color="%s"];' % RULE_R,
+ ' n3 -> nf [label="Gc", color="%s"];' % RULE_G,
" {rank=same; n2; n2b;}",
"}",
]
@@ -192,11 +216,22 @@ def main():
print("wrote", os.path.relpath(args.meta, ROOT))
else:
data = load(args.meta)
- outputs = {
- "dependency.dot": dependency_dot(data),
- "rules.dot": rules_dot(),
- "reduction.dot": reduction_dot(),
- }
+
+ counts = {}
+ for n in data["nodes"]:
+ counts[n["milestone"]] = counts.get(n["milestone"], 0) + 1
+
+ outputs = {"dependency-overview.dot": dependency_overview_dot(data)}
+ for m in data["milestones"]:
+ if not counts.get(m):
+ continue
+ keep = {n["id"] for n in data["nodes"] if n["milestone"] == m}
+ title = "Theorem dependencies %s, %d results" % (m, counts[m])
+ outputs["dependency-%s.dot" % m] = dependency_subset_dot(data, title, keep)
+
+ outputs["rules.dot"] = rules_dot()
+ outputs["reduction.dot"] = reduction_dot()
+
ok = True
for name, text in outputs.items():
path = os.path.join(args.outdir, name)
diff --git a/theory/NamedMeasure.v b/theory/NamedMeasure.v
new file mode 100644
index 0000000..167da1f
--- /dev/null
+++ b/theory/NamedMeasure.v
@@ -0,0 +1,230 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+From Stdlib Require Import Setoid Morphisms.
+Import ListNotations.
+From LambdaSub Require Import NamedMeta NamedEs.
+
+(* The measure of Appendix A of the paper.
+
+ For a metaterm t the paper defines two functions:
+ Mx(t) an upper bound on the number of free occurrences of x that can
+ give rise to redexes in sub-reducts of t,
+ s(t) the size measure used to orient the rules R, RX and Gc.
+ Both discriminate on whether the body of a substitution is a chain
+ X_Delta[x1/u1]...[xn/un] ending in a metavariable and the substituted
+ variable belongs to the annotation Delta. We capture that shape with
+ mhead below. *)
+
+Fixpoint mhead (t : ntrm) : option (list atom) :=
+ match t with
+ | NMVar _ d => Some d
+ | NESub a _ _ => mhead a
+ | _ => None
+ end.
+
+Definition head_has (a : ntrm) (y : atom) : bool :=
+ match mhead a with
+ | Some d => existsb (Nat.eqb y) d
+ | None => false
+ end.
+
+Fixpoint Mx (x : atom) (t : ntrm) : nat :=
+ match t with
+ | NVar y => if Nat.eqb y x then 1 else 0
+ | NApp a b => Mx x a + Mx x b
+ | NLam _ a => Mx x a
+ | NMVar _ d => if existsb (Nat.eqb x) d then 1 else 0
+ | NESub a y u =>
+ if head_has a y
+ then Mx x a + Mx y a * Mx x u
+ else Mx x a + Mx x u + Mx y a * Mx x u
+ end.
+
+Fixpoint s (t : ntrm) : nat :=
+ match t with
+ | NVar _ => 1
+ | NApp a b => s a + s b
+ | NLam _ a => s a
+ | NMVar _ d => length d
+ | NESub a y u =>
+ if head_has a y
+ then s a - 1 + Mx y a * s u
+ else s a + s u + Mx y a * s u
+ end.
+
+(* The counting invariant of the paper: Mx is an upper bound on the number
+ of free occurrences of x. We count free occurrences directly with nocc. *)
+Fixpoint nocc (x : atom) (t : ntrm) : nat :=
+ match t with
+ | NVar y => if Nat.eqb y x then 1 else 0
+ | NApp a b => nocc x a + nocc x b
+ | NLam y a => if Nat.eqb y x then 0 else nocc x a
+ | NESub a y u => (if Nat.eqb y x then 0 else nocc x a) + nocc x u
+ | NMVar _ d => if existsb (Nat.eqb x) d then 1 else 0
+ end.
+
+Lemma Mx_ge_0 : forall x t, 0 <= Mx x t.
+Proof. intros x t. induction t; simpl; lia. Qed.
+
+Lemma head_has_pos : forall a y, head_has a y = true -> 1 <= Mx y a.
+Proof.
+ intros a. induction a as [z | a1 IHa1 a2 _ | z a IHa | a1 IHa1 z u _ | X d]; intros y H.
+ - simpl in H. discriminate H.
+ - simpl in H. discriminate H.
+ - simpl in H. discriminate H.
+ - simpl in H. simpl. destruct (head_has a1 z) eqn:E; pose proof (IHa1 y H); lia.
+ - simpl in H. simpl.
+ assert (Hex : existsb (Nat.eqb y) d = true).
+ { unfold head_has, mhead in H. exact H. }
+ rewrite Hex. lia.
+Qed.
+
+Lemma le_mul_of_one_le : forall n m, 1 <= n -> m <= n * m.
+Proof.
+ intros n m H. rewrite <- (Nat.mul_1_l m) at 1.
+ apply Nat.mul_le_mono_r. exact H.
+Qed.
+
+Lemma nocc_le_Mx : forall x t, nocc x t <= Mx x t.
+Proof.
+ intros x t. induction t as [y | a IHa b IHb | y a IHa | a IHa y u IHu | X d].
+ - simpl. destruct (Nat.eqb y x); lia.
+ - simpl. lia.
+ - simpl. destruct (Nat.eqb y x); lia.
+ - simpl. destruct (head_has a y) eqn:E.
+ + assert (Hpos : 1 <= Mx y a) by (apply head_has_pos; exact E).
+ assert (Hnl : Mx x u <= Mx y a * Mx x u) by (apply le_mul_of_one_le; exact Hpos).
+ destruct (Nat.eqb y x) eqn:Ey; lia.
+ + destruct (Nat.eqb y x) eqn:Ey; lia.
+ - simpl. destruct (existsb (Nat.eqb x) d); lia.
+Qed.
+
+Print Assumptions Mx_ge_0.
+Print Assumptions head_has_pos.
+Print Assumptions le_mul_of_one_le.
+Print Assumptions nocc_le_Mx.
+
+(* ------------------------------------------------------------------ *)
+(* The missing invariants.
+
+ The measure proof needs the reduction rules to preserve freeness, in the
+ sense that a variable that is not free in a term contributes nothing
+ to the measure. Concretely the paper uses
+
+ x notin fv(t) implies Mx(x,t) = 0
+
+ for the Gc case and, through Lemma A.2, for the R and RX cases. That
+ property is not true on the raw named syntax: a metavariable may carry
+ an annotation variable that an enclosing substitution binds. The
+ metaterm X_[x][x/y] below is the smallest witness. Its free variables
+ are {y}, it therefore has no free occurrence of x, yet Mx(x, .) = 1. *)
+
+Lemma nfv_annot_bound_example :
+ nfv (NESub (NMVar 9 [0]) 0 (NVar 1)) = [1].
+Proof. reflexivity. Qed.
+
+Lemma Mx_fresh_fails :
+ ~ (forall x t, ~ In x (nfv t) -> Mx x t = 0).
+Proof.
+ intro H.
+ assert (Hn : ~ In 0 (nfv (NESub (NMVar 9 [0]) 0 (NVar 1)))).
+ { rewrite nfv_annot_bound_example. intros [Hc|Hc]; [discriminate Hc | destruct Hc]. }
+ specialize (H 0 (NESub (NMVar 9 [0]) 0 (NVar 1)) Hn).
+ compute in H. discriminate H.
+Qed.
+
+(* Lemma A.1, invariance of Mx and s under the C equation, also needs the
+ invariant. The two terms below are related by C with x = 0, y = 1, y not
+ free in u and x not free in v, yet their sizes and Mx values differ: the
+ occurrences of 1 and 0 that sit inside the metavariable annotation but
+ below the substitutions are counted by the special clauses. *)
+Definition A1_t : ntrm := NMVar 0 [0; 1].
+Definition A1_u : ntrm :=
+ NApp (NESub (NMVar 8 [1]) 1 (NVar 3))
+ (NApp (NApp (NVar 5) (NVar 6)) (NVar 7)).
+Definition A1_v : ntrm := NESub (NMVar 7 [0]) 0 (NVar 4).
+Definition A1_lhs : ntrm := NESub (NESub A1_t 0 A1_u) 1 A1_v.
+Definition A1_rhs : ntrm := NESub (NESub A1_t 1 A1_v) 0 A1_u.
+
+Lemma A1_C_related : Es A1_lhs A1_rhs.
+Proof.
+ apply Es_C with (x := 0) (y := 1).
+ - intro E. discriminate E.
+ - compute. intros [H|[H|[H|[H|H]]]]; try discriminate H; destruct H.
+ - compute. intros [H|H]; [discriminate H | destruct H].
+Qed.
+
+Lemma A1_s_differ : s A1_lhs <> s A1_rhs.
+Proof. compute. discriminate. Qed.
+
+Lemma A1_Mx_differ : Mx 0 A1_lhs <> Mx 0 A1_rhs.
+Proof. compute. discriminate. Qed.
+
+Lemma A1_not_invariant :
+ ~ (forall t u, Es t u -> s t = s u /\ forall z, Mx z t = Mx z u).
+Proof.
+ intro H. destruct (H A1_lhs A1_rhs A1_C_related) as [Hs _].
+ apply A1_s_differ. exact Hs.
+Qed.
+
+(* The corresponding Gc step is legal in the current rule system, but the
+ measure does not decrease: the redex has the same size as its reduct.
+ The body is X_[x][x/y] with x in the annotation, so the special clause
+ of s applies and the (bound) x in the annotation is counted by Mx,
+ cancelling the subtraction of one. *)
+Lemma Gc_special_nondecrease :
+ s (NESub (NESub (NMVar 9 [0]) 0 (NVar 1)) 0 (NVar 2))
+ = s (NESub (NMVar 9 [0]) 0 (NVar 1)).
+Proof. reflexivity. Qed.
+
+Lemma nred_Gc_special :
+ nred (NESub (NESub (NMVar 9 [0]) 0 (NVar 1)) 0 (NVar 2))
+ (NESub (NMVar 9 [0]) 0 (NVar 1)).
+Proof.
+ apply nred_Gc. simpl. intros [Hc|Hc]; [discriminate Hc | destruct Hc].
+Qed.
+
+(* A second, independent, gap: the paper states s(t) >= 1, but a
+ metavariable with empty annotation has size zero. Empty annotations are
+ not excluded by the raw syntax. *)
+Lemma s_metavar_empty : s (NMVar 9 []) = 0.
+Proof. reflexivity. Qed.
+
+(* Rule R as currently stated has no freshness side condition on the
+ substituted term, so it creates a loop, which no terminating measure can
+ orient. The step below is derivable with the empty context. The paper
+ excludes it through the convention that no free and bound variable of a
+ term share a name: x[x/u] with x free in u is not an alpha-canonical
+ metaterm. *)
+Lemma nred_R_selfloop : forall x,
+ nred (NESub (NVar x) x (NVar x)) (NESub (NVar x) x (NVar x)).
+Proof.
+ intro x. apply nred_R with (C := nHole) (phi := [x]).
+ - simpl. left. reflexivity.
+ - intros y Hy. simpl in Hy. destruct Hy as [Hy|[]]. subst y. simpl. left. reflexivity.
+ - reflexivity.
+Qed.
+
+Theorem current_sm_not_terminating : exists t, nred t t.
+Proof. exists (NESub (NVar 0) 0 (NVar 0)). apply nred_R_selfloop. Qed.
+
+(* Consequence for Es: the modulo relation subred inherits the loop, so it
+ is not terminating either without the freshness invariant. *)
+Lemma subred_selfloop : forall x,
+ subred (NESub (NVar x) x (NVar x)) (NESub (NVar x) x (NVar x)).
+Proof. intro x. apply subred_nred. apply nred_R_selfloop. Qed.
+
+Theorem current_subred_not_terminating : exists t, subred t t.
+Proof. exists (NESub (NVar 0) 0 (NVar 0)). apply subred_selfloop. Qed.
+
+Print Assumptions Mx_fresh_fails.
+Print Assumptions A1_C_related.
+Print Assumptions A1_s_differ.
+Print Assumptions A1_Mx_differ.
+Print Assumptions A1_not_invariant.
+Print Assumptions Gc_special_nondecrease.
+Print Assumptions nred_Gc_special.
+Print Assumptions s_metavar_empty.
+Print Assumptions nred_R_selfloop.
+Print Assumptions current_sm_not_terminating.
+Print Assumptions subred_selfloop.
+Print Assumptions current_subred_not_terminating.
