sneeker/lambda-sub
1
30 Fork 3
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add(index): a generated plain text index of every result with its status and file (tooling)

Browse Source
This commit is contained in:
milner committed 2026-09-22 19:31:00 +02:00
1 parent 5227268cc0
commit b672a137f2
7 files changed
+1402 -523
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

graphs/dependency.dot
+52 -1
View File
@@ -6,7 +6,7 @@ digraph theorem_deps {
ranksep=0.6;
node [fontname=Inter, fontsize=9, fontcolor="#222222"];
edge [fontname=Inter, fontsize=8, color="#9a9a9a", arrowsize=0.6, penwidth=0.8];
graph [fontname=Inter, fontsize=12, labelloc=t, label=<<B>Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M2)</B><BR/><FONT POINT-SIZE="9"><FONT COLOR="#38761d">proved</FONT> <FONT COLOR="#b45f06">stated</FONT> <FONT COLOR="#777777">planned</FONT> <FONT COLOR="#cc0000">blocked</FONT></FONT>>];
graph [fontname=Inter, fontsize=12, labelloc=t, label=<<B>Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M4)</B><BR/><FONT POINT-SIZE="9"><FONT COLOR="#38761d">proved</FONT> <FONT COLOR="#b45f06">stated</FONT> <FONT COLOR="#777777">planned</FONT> <FONT COLOR="#cc0000">blocked</FONT></FONT>>];
fvs_lift [label="fvs_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="fvs_lift theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
lift_lc [label="lift_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
lift_0_lc [label="lift_0_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_0_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -21,6 +21,17 @@ digraph theorem_deps {
subst_fvar_self [label="subst_fvar_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_self theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
subst_fvar_other [label="subst_fvar_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_other theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
subst_fvs [label="subst_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
Star_trans [label="Star_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_trans theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red1_star [label="red1_star", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_star theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
Plus_to_Star [label="Plus_to_Star", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_to_Star theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
Star_red1_context [label="Star_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_red1_context theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
star_one_trans [label="star_one_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="star_one_trans theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
in_comb [label="in_comb", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="in_comb theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
pow2_pos [label="pow2_pos", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="pow2_pos theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
size_all_terms [label="size_all_terms", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="size_all_terms theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
enumerate_check [label="enumerate_check", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_check theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
enumerate_sound [label="enumerate_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_sound theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
enumerate_complete [label="enumerate_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_complete theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
Plus_red1_context [label="Plus_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
occurs_count_zero [label="occurs_count_zero", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
occurs_count_false [label="occurs_count_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -37,6 +48,8 @@ digraph theorem_deps {
red1r_fv [label="red1r_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
lemma_2_1_fv_preserved [label="lemma_2_1_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
lemma_2_3_beta_sim [label="lemma_2_3_beta_sim", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
Plus_trans [label="Plus_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
Plus_step_trans [label="Plus_step_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_step_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
par_red1_iff [label="par_red1_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red1_in_par [label="red1_in_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
par_context [label="par_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -65,6 +78,9 @@ digraph theorem_deps {
has_red_f [label="has_red_f", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
has_red_spec [label="has_red_spec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red1_dec [label="red1_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
nf_iff_steps_nil [label="nf_iff_steps_nil", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nf_iff_steps_nil theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
normal_form_iff_nf [label="normal_form_iff_nf", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="normal_form_iff_nf theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
nf_dec [label="nf_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nf_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
open_rec_app [label="open_rec_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
open_rec_lam [label="open_rec_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
open_rec_esub [label="open_rec_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -77,6 +93,8 @@ digraph theorem_deps {
subst_notin [label="subst_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
subst_lc_self [label="subst_lc_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
subst_other [label="subst_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
open_rec_lc_atom [label="open_rec_lc_atom", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lc_atom theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
open_rec_lc [label="open_rec_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lc theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red_sub_root_to_red1 [label="red_sub_root_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_root_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red_sub_to_red1 [label="red_sub_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red_sub_context [label="red_sub_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -85,6 +103,14 @@ digraph theorem_deps {
occurs_zfill [label="occurs_zfill", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
zfill_occurs0 [label="zfill_occurs0", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
R_Gc_disjoint [label="R_Gc_disjoint", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
Star_red_sub_context [label="Star_red_sub_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
full_comp_aux_sub [label="full_comp_aux_sub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="full_comp_aux_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
plus_red_sub_full_comp [label="plus_red_sub_full_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plus_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
star_red_sub_full_comp [label="star_red_sub_full_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="star_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
es_count_plug_mono [label="es_count_plug_mono", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="es_count_plug_mono theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red_gc_measure [label="red_gc_measure", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_measure theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red_gc_terminates [label="red_gc_terminates", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_terminates theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red_gc_to_red_sub [label="red_gc_to_red_sub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_to_red_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
corpus_sound [label="corpus_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
corpus_complete [label="corpus_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
corpus_decides [label="corpus_decides", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -97,6 +123,11 @@ digraph theorem_deps {
lift_0_lc -> subst_fvar_self;
close_rec_fvs -> subst_fvs;
open_rec_fvs -> subst_fvs;
in_comb -> size_all_terms;
pow2_pos -> size_all_terms;
check_all_true -> enumerate_check;
steps_sound -> enumerate_sound;
steps_complete -> enumerate_complete;
occurs_count_zero -> occurs_count_pos;
occurs_count_false -> occurs_count_zfill_plug;
occurs_lift_self -> occurs_count_zfill_plug;
@@ -140,13 +171,33 @@ digraph theorem_deps {
steps_complete -> has_red_spec;
steps_sound -> has_red_spec;
has_red_spec -> red1_dec;
steps_complete -> nf_iff_steps_nil;
steps_sound_red1 -> nf_iff_steps_nil;
nf_iff_steps_nil -> normal_form_iff_nf;
nf_iff_steps_nil -> nf_dec;
close_rec_notin -> subst_notin;
open_rec_occurs_false -> subst_notin;
subst_fvar_self -> subst_lc_self;
subst_fvar_other -> subst_other;
open_rec_lc_atom -> open_rec_lc;
red_sub_root_to_red1 -> red_sub_to_red1;
occurs_zfill -> zfill_occurs0;
zfill_occurs0 -> R_Gc_disjoint;
red_sub_context -> Star_red_sub_context;
occurs_count_zero -> full_comp_aux_sub;
occurs_count_zfill_plug -> full_comp_aux_sub;
open_rec_occurs_false -> full_comp_aux_sub;
open_rec_zplug_lift -> full_comp_aux_sub;
red_sub_gc -> full_comp_aux_sub;
red_sub_r -> full_comp_aux_sub;
zdecs_nonempty -> full_comp_aux_sub;
zdecs_sound -> full_comp_aux_sub;
full_comp_aux_sub -> plus_red_sub_full_comp;
Plus_to_Star -> star_red_sub_full_comp;
plus_red_sub_full_comp -> star_red_sub_full_comp;
es_count_plug_mono -> red_gc_measure;
red_gc_measure -> red_gc_terminates;
red_sub_gc -> red_gc_to_red_sub;
steps_sound -> corpus_sound;
steps_complete -> corpus_complete;
has_red_spec -> corpus_decides;