110 lines
5.3 KiB
Plaintext
110 lines
5.3 KiB
Plaintext
status milestone kind name file
|
|
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
|
|
proved M1 infra close_rec_notin theory/Binding.v
|
|
proved M1 infra fvs_lift theory/Binding.v
|
|
proved M1 infra has_red_f theory/Reduction.v
|
|
proved M1 infra has_red_spec theory/Reduction.v
|
|
proved M1 infra lift_0_lc theory/Binding.v
|
|
proved M1 infra lift_lc theory/Binding.v
|
|
proved M1 infra nf_dec theory/Reduction.v
|
|
proved M1 infra nf_iff_steps_nil theory/Reduction.v
|
|
proved M1 infra normal_form_iff_nf theory/Reduction.v
|
|
proved M1 infra open_close theory/Binding.v
|
|
proved M1 infra open_rec_bvar theory/Binding.v
|
|
proved M1 infra open_rec_bvar_neq theory/Binding.v
|
|
proved M1 infra open_rec_fvs theory/Binding.v
|
|
proved M1 infra open_rec_occurs_false theory/Binding.v
|
|
proved M1 infra plug_comp theory/Reduction.v
|
|
proved M1 infra positions_at theory/Reduction.v
|
|
proved M1 infra positions_comp theory/Reduction.v
|
|
proved M1 infra positions_hole theory/Reduction.v
|
|
proved M1 infra red1_dec theory/Reduction.v
|
|
proved M1 infra root_steps_complete theory/Reduction.v
|
|
proved M1 infra root_steps_in_steps theory/Reduction.v
|
|
proved M1 infra root_steps_sound theory/Reduction.v
|
|
proved M1 infra steps_complete theory/Reduction.v
|
|
proved M1 infra steps_sound theory/Reduction.v
|
|
proved M1 infra steps_sound_red1 theory/Reduction.v
|
|
proved M1 infra subst_fvar_other theory/Binding.v
|
|
proved M1 infra subst_fvar_self theory/Binding.v
|
|
proved M1 infra subst_fvs theory/Binding.v
|
|
proved M1 infra zdecs_complete theory/Reduction.v
|
|
proved M1 infra zdecs_sound theory/Reduction.v
|
|
proved M2 infra Plus_red1_context theory/Metatheory.v
|
|
proved M2 infra Plus_step_trans theory/Metatheory.v
|
|
proved M2 infra Plus_to_Star theory/Closure.v
|
|
proved M2 infra Plus_trans theory/Metatheory.v
|
|
proved M2 infra Star_red1_context theory/Closure.v
|
|
proved M2 infra Star_trans theory/Closure.v
|
|
proved M2 infra check_all_true theory/Random.v
|
|
proved M2 infra check_term_true theory/Random.v
|
|
proved M2 infra close_rec_app theory/Substitution.v
|
|
proved M2 infra close_rec_esub theory/Substitution.v
|
|
proved M2 infra close_rec_lam theory/Substitution.v
|
|
proved M2 infra corpus_complete theory/Tests.v
|
|
proved M2 infra corpus_decides theory/Tests.v
|
|
proved M2 infra corpus_fv_preserved theory/Tests.v
|
|
proved M2 infra corpus_sound theory/Tests.v
|
|
proved M2 infra enumerate_check theory/Enumerate.v
|
|
proved M2 infra enumerate_complete theory/Enumerate.v
|
|
proved M2 infra enumerate_sound theory/Enumerate.v
|
|
proved M2 infra full_comp_aux theory/Metatheory.v
|
|
proved M2 infra fvs_zplug_lift theory/Metatheory.v
|
|
proved M2 infra gen_complete theory/Random.v
|
|
proved M2 infra gen_fv_preserved theory/Random.v
|
|
proved M2 infra gen_list_length theory/Random.v
|
|
proved M2 infra gen_sound theory/Random.v
|
|
proved M2 infra in_comb theory/Enumerate.v
|
|
proved M2 paper lemma_2_1_fv_preserved theory/Metatheory.v
|
|
proved M2 paper lemma_2_2_full_comp theory/Metatheory.v
|
|
proved M2 paper lemma_2_3_beta_sim theory/Metatheory.v
|
|
proved M2 infra occurs_count_false theory/Metatheory.v
|
|
proved M2 infra occurs_count_pos theory/Metatheory.v
|
|
proved M2 infra occurs_count_zero theory/Metatheory.v
|
|
proved M2 infra occurs_count_zfill_plug theory/Metatheory.v
|
|
proved M2 infra occurs_lift_self theory/Metatheory.v
|
|
proved M2 infra open_rec_app theory/Substitution.v
|
|
proved M2 infra open_rec_esub theory/Substitution.v
|
|
proved M2 infra open_rec_lam theory/Substitution.v
|
|
proved M2 infra open_rec_lc theory/Substitution.v
|
|
proved M2 infra open_rec_lc_atom theory/Substitution.v
|
|
proved M2 infra open_rec_zplug_lift theory/Metatheory.v
|
|
proved M2 infra plug_fv_mono theory/Metatheory.v
|
|
proved M2 infra pow2_pos theory/Enumerate.v
|
|
proved M2 infra red1_root_fv theory/Metatheory.v
|
|
proved M2 infra red1_star theory/Closure.v
|
|
proved M2 infra red1r_fv theory/Metatheory.v
|
|
proved M2 infra size_all_terms theory/Enumerate.v
|
|
proved M2 infra star_one_trans theory/Closure.v
|
|
proved M2 infra subst_app theory/Substitution.v
|
|
proved M2 infra subst_esub theory/Substitution.v
|
|
proved M2 infra subst_lam theory/Substitution.v
|
|
proved M2 infra subst_lc_self theory/Substitution.v
|
|
proved M2 infra subst_notin theory/Substitution.v
|
|
proved M2 infra subst_other theory/Substitution.v
|
|
proved M2 infra zdecs_nonempty theory/Metatheory.v
|
|
proved M3 infra R_Gc_disjoint theory/Subsystem.v
|
|
proved M3 infra Star_red_sub_context theory/Subsystem.v
|
|
proved M3 infra es_count_plug_mono theory/Subsystem.v
|
|
proved M3 infra full_comp_aux_sub theory/Subsystem.v
|
|
proved M3 infra occurs_zfill theory/Subsystem.v
|
|
proved M3 infra plus_red_sub_full_comp theory/Subsystem.v
|
|
proved M3 infra red_gc_measure theory/Subsystem.v
|
|
proved M3 infra red_gc_terminates theory/Subsystem.v
|
|
proved M3 infra red_gc_to_red_sub theory/Subsystem.v
|
|
proved M3 infra red_sub_context theory/Subsystem.v
|
|
proved M3 infra red_sub_gc theory/Subsystem.v
|
|
proved M3 infra red_sub_r theory/Subsystem.v
|
|
proved M3 infra red_sub_root_to_red1 theory/Subsystem.v
|
|
proved M3 infra red_sub_to_red1 theory/Subsystem.v
|
|
proved M3 infra star_red_sub_full_comp theory/Subsystem.v
|
|
proved M3 infra zfill_occurs0 theory/Subsystem.v
|
|
proved M4 infra par_context theory/Parallel.v
|
|
proved M4 infra par_red1_iff theory/Parallel.v
|
|
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
|