add(tests): bounded conformance suite for the reducer against the relational semantics (golden corpus)
This commit is contained in:
milner committed
1 parent
9f7696eb2f
commit
e60bdfae1a
9 files changed
+1438
-750
No files matched your search
+102
-105
@@ -1,110 +1,107 @@
|
||||
digraph theorem_deps {
|
||||
rankdir=LR;
|
||||
bgcolor="white";
|
||||
node [fontname=Inter, fontsize=10, fontcolor="#333333"];
|
||||
edge [fontname=Inter, fontsize=8, color="#333333"];
|
||||
graph [fontname=Inter, fontsize=12, labelloc=t, label="Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M0)"];
|
||||
subgraph cluster_M0 {
|
||||
label="M0";
|
||||
style="rounded";
|
||||
color="#bbbbbb";
|
||||
fontcolor="#333333";
|
||||
exec_step [label="exec_step", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#333333", tooltip="exec_step theory/ExecReducer.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
exec_examples [label="exec_examples", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#333333", tooltip="exec_examples theory/ExecReducer.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
}
|
||||
subgraph cluster_M1 {
|
||||
label="M1";
|
||||
style="rounded";
|
||||
color="#bbbbbb";
|
||||
fontcolor="#333333";
|
||||
m1_syntax [label="M1 syntax/binding", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_syntax (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
m1_open_close [label="open/close laws", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_open_close (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
m1_red1 [label="red1 (B, Gc, R)", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_red1 (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
}
|
||||
subgraph cluster_M2 {
|
||||
label="M2";
|
||||
style="rounded";
|
||||
color="#bbbbbb";
|
||||
fontcolor="#333333";
|
||||
lemma_2_1_fv_preserved [label="Lemma 2.1 fv preserved", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_1_fv_preserved (section 2) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
lemma_2_2_full_comp [label="Lemma 2.2 full composition", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_2_full_comp (section 2) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
lemma_2_3_beta_sim [label="Lemma 2.3 β-simulation", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_3_beta_sim (section 2) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
}
|
||||
subgraph cluster_M3 {
|
||||
label="M3";
|
||||
style="rounded";
|
||||
color="#bbbbbb";
|
||||
fontcolor="#333333";
|
||||
m3_measure [label="sub measure", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_measure (section A) https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
m3_termination [label="{R,Gc} termination", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_termination (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
m3_local_confluence [label="{R,Gc} local confluence", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_local_confluence (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
lemma_3_2_sub_nf_unique [label="Lemma 3.2 sub NF unique", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_3_2_sub_nf_unique (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
}
|
||||
subgraph cluster_M4 {
|
||||
label="M4";
|
||||
style="rounded";
|
||||
color="#bbbbbb";
|
||||
fontcolor="#333333";
|
||||
m4_par [label="parallel reduction par", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m4_par (section 3.2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
m4_par_diamond [label="par diamond", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m4_par_diamond (section 3.2) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
theorem_confluence_terms [label="Confluence on terms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="theorem_confluence_terms (section 3.2) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
}
|
||||
subgraph cluster_M5 {
|
||||
label="M5";
|
||||
style="rounded";
|
||||
color="#bbbbbb";
|
||||
fontcolor="#333333";
|
||||
m5_mvar [label="XΔ metaterms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_mvar (section 3.3) https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
m5_rx [label="RX rule", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_rx (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
m5_eq_C [label="=C setoid", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_eq_C (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
m5_coherence [label="RX + =C coherence", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_coherence (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
theorem_confluence_metaterms [label="Confluence on metaterms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="theorem_confluence_metaterms (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
}
|
||||
subgraph cluster_M6 {
|
||||
label="M6";
|
||||
style="rounded";
|
||||
color="#bbbbbb";
|
||||
fontcolor="#333333";
|
||||
m6_translation [label="translation to λβp", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_translation (section 4) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
m6_sn [label="SN for simply typed", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_sn (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
m6_intersection [label="intersection typing", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_intersection (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
m6_typable_sn [label="typable → SN", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_typable_sn (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
m6_sn_typable [label="SN → typable", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_sn_typable (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
corollary_6_21_psn [label="Cor 6.21 PSN", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="corollary_6_21_psn (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
}
|
||||
exec_step -> exec_examples;
|
||||
exec_examples -> m1_syntax;
|
||||
m1_syntax -> m1_open_close;
|
||||
m1_syntax -> m1_red1;
|
||||
m1_open_close -> m1_red1;
|
||||
m1_red1 -> lemma_2_1_fv_preserved;
|
||||
m1_red1 -> lemma_2_2_full_comp;
|
||||
m1_red1 -> lemma_2_3_beta_sim;
|
||||
splines=spline;
|
||||
nodesep=0.22;
|
||||
ranksep=0.6;
|
||||
node [fontname=Inter, fontsize=9, fontcolor="#222222"];
|
||||
edge [fontname=Inter, fontsize=8, color="#9a9a9a", arrowsize=0.6, penwidth=0.8];
|
||||
graph [fontname=Inter, fontsize=12, labelloc=t, label=<<B>Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M2)</B><BR/><FONT POINT-SIZE="9"><FONT COLOR="#38761d">proved</FONT> <FONT COLOR="#b45f06">stated</FONT> <FONT COLOR="#777777">planned</FONT> <FONT COLOR="#cc0000">blocked</FONT></FONT>>];
|
||||
fvs_lift [label="fvs_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="fvs_lift theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
lift_lc [label="lift_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
lift_0_lc [label="lift_0_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_0_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
open_rec_bvar [label="open_rec_bvar", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_bvar theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
close_rec_fvar [label="close_rec_fvar", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_fvar theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
open_rec_occurs_false [label="open_rec_occurs_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_occurs_false theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
close_rec_notin [label="close_rec_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_notin theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
close_rec_fvs [label="close_rec_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
open_rec_bvar_neq [label="open_rec_bvar_neq", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_bvar_neq theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
open_rec_fvs [label="open_rec_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
open_close [label="open_close", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_close theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
subst_fvar_self [label="subst_fvar_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_self theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
subst_fvar_other [label="subst_fvar_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_other theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
subst_fvs [label="subst_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
Plus_red1_context [label="Plus_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
occurs_count_zero [label="occurs_count_zero", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
occurs_count_false [label="occurs_count_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
occurs_count_pos [label="occurs_count_pos", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_pos theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
occurs_lift_self [label="occurs_lift_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_lift_self theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
zdecs_nonempty [label="zdecs_nonempty", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_nonempty theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
occurs_count_zfill_plug [label="occurs_count_zfill_plug", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zfill_plug theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
open_rec_zplug_lift [label="open_rec_zplug_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
full_comp_aux [label="full_comp_aux", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="full_comp_aux theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
lemma_2_2_full_comp [label="lemma_2_2_full_comp", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
fvs_zplug_lift [label="fvs_zplug_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="fvs_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
plug_fv_mono [label="plug_fv_mono", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plug_fv_mono theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
red1_root_fv [label="red1_root_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_root_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
red1r_fv [label="red1r_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
lemma_2_1_fv_preserved [label="lemma_2_1_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
lemma_2_3_beta_sim [label="lemma_2_3_beta_sim", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
|
||||
zdecs_sound [label="zdecs_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
zdecs_complete [label="zdecs_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
positions_at [label="positions_at", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
root_steps_sound [label="root_steps_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
root_steps_complete [label="root_steps_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
steps_sound [label="steps_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
steps_sound_red1 [label="steps_sound_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
positions_hole [label="positions_hole", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
root_steps_in_steps [label="root_steps_in_steps", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_in_steps theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
plug_comp [label="plug_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
positions_comp [label="positions_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
at_ctx_comp [label="at_ctx_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
steps_complete [label="steps_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
has_red_f [label="has_red_f", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
has_red_spec [label="has_red_spec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
red1_dec [label="red1_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
corpus_sound [label="corpus_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
corpus_complete [label="corpus_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
corpus_decides [label="corpus_decides", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
corpus_fv_preserved [label="corpus_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
|
||||
lift_lc -> lift_0_lc;
|
||||
fvs_lift -> open_rec_fvs;
|
||||
open_rec_bvar -> open_rec_fvs;
|
||||
open_rec_bvar_neq -> open_rec_fvs;
|
||||
open_rec_bvar -> open_close;
|
||||
lift_0_lc -> subst_fvar_self;
|
||||
close_rec_fvs -> subst_fvs;
|
||||
open_rec_fvs -> subst_fvs;
|
||||
occurs_count_zero -> occurs_count_pos;
|
||||
occurs_count_false -> occurs_count_zfill_plug;
|
||||
occurs_lift_self -> occurs_count_zfill_plug;
|
||||
occurs_lift_self -> open_rec_zplug_lift;
|
||||
open_rec_occurs_false -> open_rec_zplug_lift;
|
||||
occurs_count_zero -> full_comp_aux;
|
||||
occurs_count_zfill_plug -> full_comp_aux;
|
||||
open_rec_occurs_false -> full_comp_aux;
|
||||
open_rec_zplug_lift -> full_comp_aux;
|
||||
zdecs_nonempty -> full_comp_aux;
|
||||
zdecs_sound -> full_comp_aux;
|
||||
full_comp_aux -> lemma_2_2_full_comp;
|
||||
fvs_lift -> fvs_zplug_lift;
|
||||
fvs_zplug_lift -> red1_root_fv;
|
||||
plug_fv_mono -> red1r_fv;
|
||||
red1_root_fv -> red1r_fv;
|
||||
red1r_fv -> lemma_2_1_fv_preserved;
|
||||
Plus_red1_context -> lemma_2_3_beta_sim;
|
||||
lemma_2_2_full_comp -> lemma_2_3_beta_sim;
|
||||
m1_red1 -> m3_measure;
|
||||
m3_measure -> m3_termination;
|
||||
m3_termination -> m3_local_confluence;
|
||||
m1_red1 -> m3_local_confluence;
|
||||
m3_local_confluence -> lemma_3_2_sub_nf_unique;
|
||||
m1_red1 -> m4_par;
|
||||
lemma_3_2_sub_nf_unique -> m4_par;
|
||||
m4_par -> m4_par_diamond;
|
||||
m4_par_diamond -> theorem_confluence_terms;
|
||||
lemma_2_3_beta_sim -> theorem_confluence_terms;
|
||||
m1_syntax -> m5_mvar;
|
||||
m5_mvar -> m5_rx;
|
||||
m1_red1 -> m5_rx;
|
||||
m5_mvar -> m5_eq_C;
|
||||
m5_rx -> m5_coherence;
|
||||
m5_eq_C -> m5_coherence;
|
||||
lemma_3_2_sub_nf_unique -> m5_coherence;
|
||||
m5_coherence -> theorem_confluence_metaterms;
|
||||
m4_par_diamond -> theorem_confluence_metaterms;
|
||||
m1_red1 -> m6_translation;
|
||||
m6_translation -> m6_sn;
|
||||
m6_sn -> m6_intersection;
|
||||
m6_intersection -> m6_typable_sn;
|
||||
m6_typable_sn -> m6_sn_typable;
|
||||
m6_sn_typable -> corollary_6_21_psn;
|
||||
theorem_confluence_terms -> corollary_6_21_psn;
|
||||
zdecs_sound -> root_steps_sound;
|
||||
zdecs_complete -> root_steps_complete;
|
||||
positions_at -> steps_sound;
|
||||
root_steps_sound -> steps_sound;
|
||||
steps_sound -> steps_sound_red1;
|
||||
positions_hole -> root_steps_in_steps;
|
||||
at_ctx_comp -> steps_complete;
|
||||
plug_comp -> steps_complete;
|
||||
positions_comp -> steps_complete;
|
||||
root_steps_complete -> steps_complete;
|
||||
root_steps_in_steps -> steps_complete;
|
||||
has_red_f -> has_red_spec;
|
||||
steps_complete -> has_red_spec;
|
||||
steps_sound -> has_red_spec;
|
||||
has_red_spec -> red1_dec;
|
||||
steps_sound -> corpus_sound;
|
||||
steps_complete -> corpus_complete;
|
||||
has_red_spec -> corpus_decides;
|
||||
lemma_2_1_fv_preserved -> corpus_fv_preserved;
|
||||
steps_sound_red1 -> corpus_fv_preserved;
|
||||
}
|
||||
Binary file not shown.
|
Before Width: | Height: | Size: 160 KiB After Width: | Height: | Size: 222 KiB |
+670
-410
File diff suppressed because it is too large.
Load diff
|
Before Width: | Height: | Size: 29 KiB After Width: | Height: | Size: 40 KiB |
+518
-198
@@ -1,272 +1,592 @@
|
||||
{
|
||||
"paper": {
|
||||
"title": "Milner's Lambda-Calculus with Partial Substitutions",
|
||||
"authors": ["Delia Kesner", "Shane Ó Conchúir"],
|
||||
"authors": [
|
||||
"Delia Kesner",
|
||||
"Shane Ó Conchúir"
|
||||
],
|
||||
"url": "https://arxiv.org/abs/2312.13270",
|
||||
"html": "https://arxiv.org/html/2312.13270v1"
|
||||
},
|
||||
"milestones": ["M0", "M1", "M2", "M3", "M4", "M5", "M6"],
|
||||
"current": "M0",
|
||||
"milestones": [
|
||||
"M1",
|
||||
"M2"
|
||||
],
|
||||
"current": "M2",
|
||||
"nodes": [
|
||||
{
|
||||
"id": "exec_step",
|
||||
"label": "exec_step",
|
||||
"id": "fvs_lift",
|
||||
"label": "fvs_lift",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M0",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/ExecReducer.v",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "exec_examples",
|
||||
"label": "exec_examples",
|
||||
"id": "lift_lc",
|
||||
"label": "lift_lc",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M0",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/ExecReducer.v",
|
||||
"depends": ["exec_step"]
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m1_syntax",
|
||||
"label": "M1 syntax/binding",
|
||||
"id": "lift_0_lc",
|
||||
"label": "lift_0_lc",
|
||||
"kind": "infra",
|
||||
"status": "planned",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "2",
|
||||
"file": "",
|
||||
"depends": ["exec_examples"]
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": [
|
||||
"lift_lc"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "m1_open_close",
|
||||
"label": "open/close laws",
|
||||
"id": "open_rec_bvar",
|
||||
"label": "open_rec_bvar",
|
||||
"kind": "infra",
|
||||
"status": "planned",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "2",
|
||||
"file": "",
|
||||
"depends": ["m1_syntax"]
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m1_red1",
|
||||
"label": "red1 (B, Gc, R)",
|
||||
"id": "close_rec_fvar",
|
||||
"label": "close_rec_fvar",
|
||||
"kind": "infra",
|
||||
"status": "planned",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "2",
|
||||
"file": "",
|
||||
"depends": ["m1_syntax", "m1_open_close"]
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "lemma_2_1_fv_preserved",
|
||||
"label": "Lemma 2.1 fv preserved",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"id": "open_rec_occurs_false",
|
||||
"label": "open_rec_occurs_false",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "close_rec_notin",
|
||||
"label": "close_rec_notin",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "close_rec_fvs",
|
||||
"label": "close_rec_fvs",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "open_rec_bvar_neq",
|
||||
"label": "open_rec_bvar_neq",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "open_rec_fvs",
|
||||
"label": "open_rec_fvs",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": [
|
||||
"fvs_lift",
|
||||
"open_rec_bvar",
|
||||
"open_rec_bvar_neq"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "open_close",
|
||||
"label": "open_close",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": [
|
||||
"open_rec_bvar"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "subst_fvar_self",
|
||||
"label": "subst_fvar_self",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": [
|
||||
"lift_0_lc"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "subst_fvar_other",
|
||||
"label": "subst_fvar_other",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "subst_fvs",
|
||||
"label": "subst_fvs",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Binding.v",
|
||||
"depends": [
|
||||
"close_rec_fvs",
|
||||
"open_rec_fvs"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "Plus_red1_context",
|
||||
"label": "Plus_red1_context",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "2",
|
||||
"file": "",
|
||||
"depends": ["m1_red1"]
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "occurs_count_zero",
|
||||
"label": "occurs_count_zero",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "occurs_count_false",
|
||||
"label": "occurs_count_false",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "occurs_count_pos",
|
||||
"label": "occurs_count_pos",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"occurs_count_zero"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "occurs_lift_self",
|
||||
"label": "occurs_lift_self",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "zdecs_nonempty",
|
||||
"label": "zdecs_nonempty",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "occurs_count_zfill_plug",
|
||||
"label": "occurs_count_zfill_plug",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"occurs_count_false",
|
||||
"occurs_lift_self"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "open_rec_zplug_lift",
|
||||
"label": "open_rec_zplug_lift",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"occurs_lift_self",
|
||||
"open_rec_occurs_false"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "full_comp_aux",
|
||||
"label": "full_comp_aux",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"occurs_count_zero",
|
||||
"occurs_count_zfill_plug",
|
||||
"open_rec_occurs_false",
|
||||
"open_rec_zplug_lift",
|
||||
"zdecs_nonempty",
|
||||
"zdecs_sound"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "lemma_2_2_full_comp",
|
||||
"label": "Lemma 2.2 full composition",
|
||||
"label": "lemma_2_2_full_comp",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "2",
|
||||
"file": "",
|
||||
"depends": ["m1_red1"]
|
||||
"section": "2.2",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"full_comp_aux"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "fvs_zplug_lift",
|
||||
"label": "fvs_zplug_lift",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"fvs_lift"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "plug_fv_mono",
|
||||
"label": "plug_fv_mono",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "red1_root_fv",
|
||||
"label": "red1_root_fv",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"fvs_zplug_lift"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "red1r_fv",
|
||||
"label": "red1r_fv",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"plug_fv_mono",
|
||||
"red1_root_fv"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "lemma_2_1_fv_preserved",
|
||||
"label": "lemma_2_1_fv_preserved",
|
||||
"kind": "paper",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "2.1",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"red1r_fv"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "lemma_2_3_beta_sim",
|
||||
"label": "Lemma 2.3 β-simulation",
|
||||
"label": "lemma_2_3_beta_sim",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "2",
|
||||
"file": "",
|
||||
"depends": ["m1_red1", "lemma_2_2_full_comp"]
|
||||
"section": "2.3",
|
||||
"file": "theory/Metatheory.v",
|
||||
"depends": [
|
||||
"Plus_red1_context",
|
||||
"lemma_2_2_full_comp"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "m3_measure",
|
||||
"label": "sub measure",
|
||||
"id": "zdecs_sound",
|
||||
"label": "zdecs_sound",
|
||||
"kind": "infra",
|
||||
"status": "planned",
|
||||
"milestone": "M3",
|
||||
"section": "A",
|
||||
"file": "",
|
||||
"depends": ["m1_red1"]
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m3_termination",
|
||||
"label": "{R,Gc} termination",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M3",
|
||||
"section": "3.1",
|
||||
"file": "",
|
||||
"depends": ["m3_measure"]
|
||||
},
|
||||
{
|
||||
"id": "m3_local_confluence",
|
||||
"label": "{R,Gc} local confluence",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M3",
|
||||
"section": "3.1",
|
||||
"file": "",
|
||||
"depends": ["m3_termination", "m1_red1"]
|
||||
},
|
||||
{
|
||||
"id": "lemma_3_2_sub_nf_unique",
|
||||
"label": "Lemma 3.2 sub NF unique",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M3",
|
||||
"section": "3.1",
|
||||
"file": "",
|
||||
"depends": ["m3_local_confluence"]
|
||||
},
|
||||
{
|
||||
"id": "m4_par",
|
||||
"label": "parallel reduction par",
|
||||
"id": "zdecs_complete",
|
||||
"label": "zdecs_complete",
|
||||
"kind": "infra",
|
||||
"status": "planned",
|
||||
"milestone": "M4",
|
||||
"section": "3.2",
|
||||
"file": "",
|
||||
"depends": ["m1_red1", "lemma_3_2_sub_nf_unique"]
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m4_par_diamond",
|
||||
"label": "par diamond",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M4",
|
||||
"section": "3.2",
|
||||
"file": "",
|
||||
"depends": ["m4_par"]
|
||||
},
|
||||
{
|
||||
"id": "theorem_confluence_terms",
|
||||
"label": "Confluence on terms",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M4",
|
||||
"section": "3.2",
|
||||
"file": "",
|
||||
"depends": ["m4_par_diamond", "lemma_2_3_beta_sim"]
|
||||
},
|
||||
{
|
||||
"id": "m5_mvar",
|
||||
"label": "XΔ metaterms",
|
||||
"id": "positions_at",
|
||||
"label": "positions_at",
|
||||
"kind": "infra",
|
||||
"status": "planned",
|
||||
"milestone": "M5",
|
||||
"section": "3.3",
|
||||
"file": "",
|
||||
"depends": ["m1_syntax"]
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m5_rx",
|
||||
"label": "RX rule",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M5",
|
||||
"section": "3.3",
|
||||
"file": "",
|
||||
"depends": ["m5_mvar", "m1_red1"]
|
||||
"id": "root_steps_sound",
|
||||
"label": "root_steps_sound",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"zdecs_sound"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "m5_eq_C",
|
||||
"label": "=C setoid",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M5",
|
||||
"section": "3.3",
|
||||
"file": "",
|
||||
"depends": ["m5_mvar"]
|
||||
"id": "root_steps_complete",
|
||||
"label": "root_steps_complete",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"zdecs_complete"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "m5_coherence",
|
||||
"label": "RX + =C coherence",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M5",
|
||||
"section": "3.3",
|
||||
"file": "",
|
||||
"depends": ["m5_rx", "m5_eq_C", "lemma_3_2_sub_nf_unique"]
|
||||
"id": "steps_sound",
|
||||
"label": "steps_sound",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"positions_at",
|
||||
"root_steps_sound"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "theorem_confluence_metaterms",
|
||||
"label": "Confluence on metaterms",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M5",
|
||||
"section": "3.3",
|
||||
"file": "",
|
||||
"depends": ["m5_coherence", "m4_par_diamond"]
|
||||
"id": "steps_sound_red1",
|
||||
"label": "steps_sound_red1",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"steps_sound"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "m6_translation",
|
||||
"label": "translation to λβp",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M6",
|
||||
"section": "4",
|
||||
"file": "",
|
||||
"depends": ["m1_red1"]
|
||||
"id": "positions_hole",
|
||||
"label": "positions_hole",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m6_sn",
|
||||
"label": "SN for simply typed",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M6",
|
||||
"section": "6",
|
||||
"file": "",
|
||||
"depends": ["m6_translation"]
|
||||
"id": "root_steps_in_steps",
|
||||
"label": "root_steps_in_steps",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"positions_hole"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "m6_intersection",
|
||||
"label": "intersection typing",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M6",
|
||||
"section": "6",
|
||||
"file": "",
|
||||
"depends": ["m6_sn"]
|
||||
"id": "plug_comp",
|
||||
"label": "plug_comp",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m6_typable_sn",
|
||||
"label": "typable → SN",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M6",
|
||||
"section": "6",
|
||||
"file": "",
|
||||
"depends": ["m6_intersection"]
|
||||
"id": "positions_comp",
|
||||
"label": "positions_comp",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "m6_sn_typable",
|
||||
"label": "SN → typable",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M6",
|
||||
"section": "6",
|
||||
"file": "",
|
||||
"depends": ["m6_typable_sn"]
|
||||
"id": "at_ctx_comp",
|
||||
"label": "at_ctx_comp",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "corollary_6_21_psn",
|
||||
"label": "Cor 6.21 PSN",
|
||||
"kind": "paper",
|
||||
"status": "planned",
|
||||
"milestone": "M6",
|
||||
"section": "6",
|
||||
"file": "",
|
||||
"depends": ["m6_sn_typable", "theorem_confluence_terms"]
|
||||
"id": "steps_complete",
|
||||
"label": "steps_complete",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"at_ctx_comp",
|
||||
"plug_comp",
|
||||
"positions_comp",
|
||||
"root_steps_complete",
|
||||
"root_steps_in_steps"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "has_red_f",
|
||||
"label": "has_red_f",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": []
|
||||
},
|
||||
{
|
||||
"id": "has_red_spec",
|
||||
"label": "has_red_spec",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"has_red_f",
|
||||
"steps_complete",
|
||||
"steps_sound"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "red1_dec",
|
||||
"label": "red1_dec",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M1",
|
||||
"section": "",
|
||||
"file": "theory/Reduction.v",
|
||||
"depends": [
|
||||
"has_red_spec"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "corpus_sound",
|
||||
"label": "corpus_sound",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Tests.v",
|
||||
"depends": [
|
||||
"steps_sound"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "corpus_complete",
|
||||
"label": "corpus_complete",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Tests.v",
|
||||
"depends": [
|
||||
"steps_complete"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "corpus_decides",
|
||||
"label": "corpus_decides",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Tests.v",
|
||||
"depends": [
|
||||
"has_red_spec"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "corpus_fv_preserved",
|
||||
"label": "corpus_fv_preserved",
|
||||
"kind": "infra",
|
||||
"status": "proved",
|
||||
"milestone": "M2",
|
||||
"section": "",
|
||||
"file": "theory/Tests.v",
|
||||
"depends": [
|
||||
"lemma_2_1_fv_preserved",
|
||||
"steps_sound_red1"
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
Reference in new issue
Block a user