Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1745 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (228 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (859 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (123 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (77 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (312 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (114 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (32 entries)

Global Index

A

A [axiom, in term_orderings.rpo]
A [axiom, in basis.decidable_set]
A [axiom, in basis.ordered_set]
A [axiom, in basis.decidable_set]
AC [constructor, in term_algebra.term]
ac [library]
acc_and [lemma, in basis.closure]
acc_lex [lemma, in term_orderings.rpo]
acc_nf [lemma, in basis.closure]
acc_one_step [axiom, in term_algebra.equational_theory]
acc_one_step_list [axiom, in term_algebra.equational_theory]
acc_subterms [axiom, in term_algebra.equational_theory]
acc_subterms_1 [axiom, in term_algebra.equational_theory]
acc_subterms_3 [axiom, in term_algebra.equational_theory]
acc_trans [lemma, in basis.closure]
acc_with_subterm [axiom, in term_algebra.equational_theory]
acc_with_subterm_subterms [axiom, in term_algebra.equational_theory]
ACU [module, in unification.unification]
ACU.F.is_coherent [definition, in unification.unification]
ACU.F.LU [constructor, in unification.unification]
ACU.F.Make.Import.acu [definition, in unification.unification]
ACU.F.Make.Import.acu_is_ac_on_unit_nf [lemma, in unification.unification]
ACU.F.Make.Import.ac_const [lemma, in unification.unification]
ACU.F.Make.Import.clash [lemma, in unification.unification]
ACU.F.Make.Import.left_unit [constructor, in unification.unification]
ACU.F.Make.Import.mutate_c [lemma, in unification.unification]
ACU.F.Make.Import.mutate_cu [lemma, in unification.unification]
ACU.F.Make.Import.mutate_cu_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_c_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free_lu [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free_lu_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free_ru [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free_ru_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free_u [lemma, in unification.unification]
ACU.F.Make.Import.mutate_free_u_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu_lu [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu_lu_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu_ru [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu_ru_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu_u [lemma, in unification.unification]
ACU.F.Make.Import.mutate_lu_u_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_ru [lemma, in unification.unification]
ACU.F.Make.Import.mutate_ru_ru [lemma, in unification.unification]
ACU.F.Make.Import.mutate_ru_ru_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_ru_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_ru_u [lemma, in unification.unification]
ACU.F.Make.Import.mutate_ru_u_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_u [lemma, in unification.unification]
ACU.F.Make.Import.mutate_u_sound [lemma, in unification.unification]
ACU.F.Make.Import.mutate_u_u [lemma, in unification.unification]
ACU.F.Make.Import.mutate_u_u_sound [lemma, in unification.unification]
ACU.F.Make.Import.no_need_of_instance [lemma, in unification.unification]
ACU.F.Make.Import.right_unit [constructor, in unification.unification]
ACU.F.Make.Import.unit_for_AC [lemma, in unification.unification]
ACU.F.Make.Import.unit_for_C [lemma, in unification.unification]
ACU.F.Make.Import.unit_nf [definition, in unification.unification]
ACU.F.Make.Import.unit_nf_is_idempotent [lemma, in unification.unification]
ACU.F.Make.Import.unit_nf_is_sound [lemma, in unification.unification]
ACU.F.Make.Import.unit_nf_nothing [lemma, in unification.unification]
ACU.F.Make.Import.unit_one_step_at_top [inductive, in unification.unification]
ACU.F.Make.Import.unit_th [definition, in unification.unification]
ACU.F.Make.Import.unit_th_is_unit_nf_eq [lemma, in unification.unification]
ACU.F.Make.Import.well_formed_unit_nf [lemma, in unification.unification]
ACU.F.unit_theory_type [inductive, in unification.unification]
ac_cf_eq [axiom, in ac_matching.ac]
ac_size_eq [axiom, in ac_matching.ac]
ac_size_ge_one [axiom, in ac_matching.ac]
ac_size_unfold [axiom, in ac_matching.ac]
ac_syntactic [axiom, in list_extensions.list_permut]
ac_top_eq [axiom, in ac_matching.ac]
add_new_var_to_rough_sol [axiom, in ac_matching.matching]
adequacy [lemma, in list_extensions.math_permut]
all_le_def [lemma, in examples.cime_trace.ring_extention]
all_mem_pos_def [lemma, in examples.cime_trace.ring_extention]
apply_subst_const [axiom, in term_algebra.term]
arity [axiom, in term_algebra.term]
arity_type [inductive, in term_algebra.term]


B

build_eq_Term [axiom, in ac_matching.ac]


C

C [constructor, in term_algebra.term]
cardinal_subset [axiom, in list_extensions.list_set]
CaseA [constructor, in basis.closure]
CaseB [constructor, in basis.closure]
cf_eq_ac [axiom, in ac_matching.cf_eq_ac]
cf_eq_ac [library]
closure [library]
comm [axiom, in ac_matching.ac]
comp [inductive, in basis.ordered_set]
compute_red [axiom, in term_algebra.equational_theory]
compute_red_is_correct [axiom, in term_algebra.equational_theory]
cons_permut_mem [axiom, in list_extensions.list_permut]
context_cons [axiom, in term_algebra.equational_theory]
context_in [axiom, in term_algebra.equational_theory]
context_trans_clos_multiset_extension_step_app1 [axiom, in list_extensions.dickson]
Convert [module, in basis.decidable_set]
Convert.A [definition, in basis.decidable_set]
Convert.A [definition, in basis.decidable_set]
Convert.eq_A [definition, in basis.decidable_set]
Convert.eq_A [definition, in basis.decidable_set]
Convert.eq_dec [lemma, in basis.decidable_set]
Convert.eq_proof [lemma, in basis.decidable_set]
cycle_not_acc [lemma, in basis.closure]


D

D [module, in list_extensions.dickson]
decidable_set [library]
dec_nf [lemma, in basis.closure]
Dep_fun [constructor, in list_extensions.more_list]
dep_fun [inductive, in list_extensions.more_list]
dep_fun_tail [definition, in list_extensions.more_list]
dickson [axiom, in list_extensions.dickson]
dickson [library]
dickson_strong [axiom, in list_extensions.dickson]
diff_in_remove [lemma, in list_extensions.more_list]
diff_mem_remove [axiom, in list_extensions.list_permut]
dp [library]
D.Import.Import.EDS [definition, in list_extensions.dickson]
D.Import.Import.EDS [definition, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.appendn_app [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.consn_app [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_multiset_extension_step_app1 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_multiset_extension_step_app2 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_multiset_extension_step_cons [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_trans_clos_multiset_extension_step_app1 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_trans_clos_multiset_extension_step_cons [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_aux1 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_aux2 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_aux3 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_strong [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.greater_case [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.in_appendn [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.A [definition, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.eq_A [definition, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.eq_dec [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.eq_proof [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_acc [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_multiset_extension_step_1 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_multiset_extension_step_2 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_trans_clos_multiset_extension_step_1 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_trans_clos_multiset_extension_step_2 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mem_consn [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult [definition, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure_aux [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure_aux2 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure_aux3 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_extension_step [inductive, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_complete [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_complete_equiv [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_complete_greater [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_sound [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.nil_is_the_smallest [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.permut_appendn [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.permut_consn [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.remove_context_multiset_extension_step_app1 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.remove_context_trans_clos_multiset_extension_step_app1 [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.rmv_case [constructor, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.R_dec_sym [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.R_or_eq_dec [definition, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.R_or_eq_dec_is_sound [lemma, in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.two_cases [lemma, in list_extensions.dickson]
D.Import.Import.Make.LP [definition, in list_extensions.dickson]
D.Import.Import.Make.LP [definition, in list_extensions.dickson]
D.Import.Import.multiset_extension_step [inductive, in list_extensions.dickson]
D.Import.Import.rmv_case [constructor, in list_extensions.dickson]


E

empty_subst_is_id [axiom, in term_algebra.term]
empty_subst_is_id_list [axiom, in term_algebra.term]
EqTh [module, in term_algebra.equational_theory]
EqTh [module, in ac_matching.ac]
EqTh.T.at_top [constructor, in term_algebra.equational_theory]
EqTh.T.axiom [inductive, in term_algebra.equational_theory]
EqTh.T.Const [constructor, in term_algebra.equational_theory]
EqTh.T.constructor [inductive, in term_algebra.equational_theory]
EqTh.T.Def [constructor, in term_algebra.equational_theory]
EqTh.T.defined [inductive, in term_algebra.equational_theory]
EqTh.T.head_step [constructor, in term_algebra.equational_theory]
EqTh.T.instance [constructor, in term_algebra.equational_theory]
EqTh.T.in_context [constructor, in term_algebra.equational_theory]
EqTh.T.Mod [constructor, in term_algebra.equational_theory]
EqTh.T.module [inductive, in term_algebra.equational_theory]
EqTh.T.one_step [inductive, in term_algebra.equational_theory]
EqTh.T.one_step_list [inductive, in term_algebra.equational_theory]
EqTh.T.rwr [definition, in term_algebra.equational_theory]
EqTh.T.rwr_list [definition, in term_algebra.equational_theory]
EqTh.T.tail_step [constructor, in term_algebra.equational_theory]
EqTh.T.VT.A [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_nf_subst [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_one_step [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_one_step_list [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_rwr_subst [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_subterms [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_subterms_1 [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_subterms_3 [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_with_subterm [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_with_subterm_subterms [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.at_top [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.axiom [inductive, in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_head_red [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_head_red_is_correct [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_red [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_red_is_correct [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_red_unfold [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.Const [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.constructor [inductive, in term_algebra.equational_theory]
EqTh.T.VT.Make.context_cons [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.context_in [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.Def [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.defined [inductive, in term_algebra.equational_theory]
EqTh.T.VT.Make.FB_nf_dec [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.F_compute_red [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.general_context [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.general_context_aux [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.head_step [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.instance [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.in_context [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.Mod [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.module [inductive, in term_algebra.equational_theory]
EqTh.T.VT.Make.nf_one_step_subterm [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.nf_rwr_subterm [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.non_overlapping [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.no_need_of_instance_is_modular [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step [inductive, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_apply_subst [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_at_pos [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_context_in [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_in_list [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_list [inductive, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_list_length_eq [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_list_rwr_list [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.overlay [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.o_size [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_apply_subst [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_at_pos [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_closure [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_closure_one_step [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_inv [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list_is_trans [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list_length_eq [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list_trans_clos_one_step_list [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_or_eq [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_or_eq_subst [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_R1_included_in_R2 [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_subst [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_axiom [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_one_step [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_rwr [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_rwr_list [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.R_axiom [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.R_one_step [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.R_rwr [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.split_rel [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.sym_refl [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.tail_step [constructor, in term_algebra.equational_theory]
EqTh.T.VT.Make.term_acc_subst [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.th_eq [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.th_refl [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.th_sym [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.var_acc [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.A [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.A [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.eq_A [definition, in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.eq_dec [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.eq_proof [lemma, in term_algebra.equational_theory]
EqTh.T.VT.Make.wf_size [lemma, in term_algebra.equational_theory]
EqTh.T.VT.non_overlapping [definition, in term_algebra.equational_theory]
EqTh.T.VT.overlay [definition, in term_algebra.equational_theory]
EqTh.T.VT.sym_refl [definition, in term_algebra.equational_theory]
EqTh.T.VT.th_eq [definition, in term_algebra.equational_theory]
equational_extension [library]
equational_theory [library]
Equivalent [constructor, in basis.ordered_set]
equiv_add_context [axiom, in term_orderings.rpo]
equiv_dec [axiom, in term_orderings.rpo]
equiv_equiv [axiom, in term_orderings.rpo]
equiv_in_list [lemma, in list_extensions.equiv_list]
equiv_in_list_2 [lemma, in list_extensions.equiv_list]
equiv_list [library]
equiv_rpo_equiv_1 [axiom, in term_orderings.rpo]
equiv_rpo_equiv_2 [axiom, in term_orderings.rpo]
equiv_rpo_equiv_3 [axiom, in term_orderings.rpo]
equiv_rpo_equiv_4 [axiom, in term_orderings.rpo]
equiv_subst [axiom, in term_orderings.rpo]
equiv_swap [lemma, in list_extensions.equiv_list]
eq_A [axiom, in basis.ordered_set]
eq_A [axiom, in basis.decidable_set]
eq_dec [axiom, in term_orderings.term_o]
eq_dec [axiom, in basis.ordered_set]
eq_dec [axiom, in basis.decidable_set]
eq_dec [axiom, in basis.decidable_set]
eq_dec [axiom, in basis.ordered_set]
eq_proof [axiom, in basis.decidable_set]
eq_proof [axiom, in basis.ordered_set]
eq_term_dec [axiom, in term_algebra.term]
ES [module, in basis.ordered_set]
ES [module, in basis.decidable_set]
exists_dec [lemma, in list_extensions.list_permut]
exists_map12_without_repetition [lemma, in list_extensions.more_list]
exists_map_without_repetition [lemma, in list_extensions.more_list]
exists_subterm_is_a_pos [axiom, in term_algebra.term]
Export [module, in term_algebra.term]


F

F [module, in unification.unification]
FB_nf_dec [axiom, in term_algebra.equational_theory]
find_app [lemma, in list_extensions.more_list]
find_diff [lemma, in list_extensions.more_list]
find_map [lemma, in list_extensions.more_list]
find_mem [lemma, in list_extensions.more_list]
find_not_found [lemma, in list_extensions.more_list]
find_not_mem [lemma, in list_extensions.more_list]
flatten_app [axiom, in ac_matching.ac]
flatten_apply_cf_subst [axiom, in ac_matching.ac]
flatten_build [axiom, in ac_matching.ac]
flatten_build_cons [axiom, in ac_matching.ac]
flatten_build_inside [axiom, in ac_matching.ac]
flatten_cf [axiom, in ac_matching.ac]
flatten_cf_cf [axiom, in ac_matching.ac]
fold_left2 [definition, in list_extensions.more_list]
fold_left_in_acc [lemma, in list_extensions.more_list]
fold_left_in_acc_split [lemma, in list_extensions.more_list]
Free [constructor, in term_algebra.term]
free_unif [library]
fresh_var [axiom, in ac_matching.matching]
fresh_var [axiom, in ac_matching.matching]
fresh_var_spec [axiom, in ac_matching.matching]
fresh_var_spec [axiom, in ac_matching.matching]
F_mapii [definition, in list_extensions.more_list]
F_wf_solve_dec1 [axiom, in ac_matching.matching_algo]
F_wf_solve_dec2 [axiom, in ac_matching.matching_algo]


G

general_context [axiom, in term_algebra.equational_theory]
general_context_aux [axiom, in term_algebra.equational_theory]
Greater_than [constructor, in basis.ordered_set]


I

Import [module, in list_extensions.dickson]
Import [module, in list_extensions.dickson]
Import [module, in ac_matching.cf_eq_ac]
Import [module, in list_extensions.dickson]
Import [module, in ac_matching.matching_well_formed]
Import [module, in term_orderings.term_o]
Import [module, in list_extensions.list_set]
Import [module, in ac_matching.matching_algo]
Import [module, in ac_matching.matching]
Import [module, in ac_matching.ac]
Import [module, in ac_matching.cf_eq_ac]
Import [module, in ac_matching.matching_well_founded]
Import [module, in term_orderings.inner_dp]
Import [module, in list_extensions.list_permut]
Import [module, in ac_matching.matching_sound]
Import [module, in ac_matching.matching_algo]
Import [module, in list_extensions.dickson]
Import [module, in term_orderings.term_o]
Import [module, in term_algebra.term]
Import [module, in ac_matching.matching_well_formed]
Import [module, in term_orderings.rpo]
Import [module, in term_algebra.term]
Import [module, in list_extensions.dickson]
Import [module, in list_extensions.list_sort]
Import [module, in unification.unification]
Import [module, in ac_matching.ac]
Import [module, in ac_matching.ac]
Import [module, in ac_matching.matching_well_founded]
Import [module, in term_orderings.rpo]
Import [module, in list_extensions.list_sort]
Import [module, in term_orderings.rpo]
Import [module, in list_extensions.list_permut]
Import [module, in list_extensions.list_sort]
Import [module, in list_extensions.list_set]
Import [module, in ac_matching.matching]
Import [module, in term_orderings.rpo]
Import [module, in list_extensions.list_set]
Import [module, in term_algebra.term]
Import [module, in list_extensions.list_set]
Import [module, in ac_matching.matching_complete]
Import [module, in ac_matching.matching_complete]
Import [module, in term_orderings.inner_dp]
Import [module, in term_orderings.rpo]
Import [module, in list_extensions.list_sort]
Import [module, in term_algebra.term]
Import [module, in unification.free_unif]
Import [module, in ac_matching.matching_sound]
Import [module, in term_orderings.rpo]
Import [module, in ac_matching.ac]
included_list [definition, in list_extensions.more_list]
included_list_sound [lemma, in list_extensions.more_list]
incl_trans [lemma, in basis.closure]
incl_trans2 [lemma, in basis.closure]
inner_dp [library]
insert_1 [lemma, in list_extensions.more_list]
insert_2 [lemma, in list_extensions.more_list]
inv_trans [lemma, in basis.closure]
In_dec_app [lemma, in list_extensions.more_list]
in_impl_mem [axiom, in list_extensions.list_permut]
in_insert [lemma, in list_extensions.more_list]
in_in_split_set [lemma, in list_extensions.more_list]
In_mem [lemma, in list_extensions.more_list]
in_permut_in [lemma, in list_extensions.list_permut]
in_quick_in [axiom, in list_extensions.list_sort]
in_remove [lemma, in list_extensions.more_list]
in_remove_list [axiom, in list_extensions.list_sort]
in_split_set [lemma, in list_extensions.more_list]
is_a_pos_exists_subterm [axiom, in term_algebra.term]


J

jump_combine [lemma, in examples.cime_trace.ring_extention]
jump_in [lemma, in examples.cime_trace.ring_extention]
jump_length [lemma, in examples.cime_trace.ring_extention]
jump_nil [lemma, in examples.cime_trace.ring_extention]


L

LDS [module, in list_extensions.dickson]
length_add [lemma, in list_extensions.more_list]
length_app [definition, in list_extensions.more_list]
length_flatten_bis [axiom, in ac_matching.ac]
length_flatten_ter [axiom, in ac_matching.ac]
length_map [definition, in list_extensions.more_list]
length_quicksort [axiom, in list_extensions.list_sort]
Less_than [constructor, in basis.ordered_set]
lex [definition, in term_orderings.rpo]
Lex [constructor, in term_orderings.rpo]
lex_trans [lemma, in term_orderings.rpo]
list_contents [definition, in list_extensions.math_permut]
list_exists_app [lemma, in list_extensions.more_list]
list_exists_impl [lemma, in list_extensions.more_list]
list_exists_is_sound [lemma, in list_extensions.more_list]
list_exists_option_is_complete_false [lemma, in list_extensions.more_list]
list_exists_option_is_complete_none [lemma, in list_extensions.more_list]
list_exists_option_is_complete_true [lemma, in list_extensions.more_list]
list_exists_option_is_sound [lemma, in list_extensions.more_list]
list_exists_rest [definition, in list_extensions.more_list]
list_exists_rest_is_sound [lemma, in list_extensions.more_list]
list_forall2_is_sound [lemma, in list_extensions.more_list]
list_forall_app [lemma, in list_extensions.more_list]
list_forall_impl [lemma, in list_extensions.more_list]
list_forall_is_sound [lemma, in list_extensions.more_list]
list_forall_option_is_complete_false [lemma, in list_extensions.more_list]
list_forall_option_is_complete_true [lemma, in list_extensions.more_list]
list_forall_option_is_sound [lemma, in list_extensions.more_list]
list_permut [library]
list_permut_acc [axiom, in list_extensions.dickson]
list_permut_app_app [axiom, in list_extensions.list_permut]
list_permut_flatten [axiom, in ac_matching.ac]
list_permut_multiset_extension_step_1 [axiom, in list_extensions.dickson]
list_permut_multiset_extension_step_2 [axiom, in list_extensions.dickson]
list_permut_occurs_in_term_list [axiom, in ac_matching.matching]
list_rec2 [definition, in list_extensions.more_list]
list_rec3 [definition, in list_extensions.more_list]
list_set [library]
list_size [definition, in list_extensions.more_list]
list_size_app [lemma, in list_extensions.more_list]
list_size_fold [lemma, in list_extensions.more_list]
list_size_size_eq [lemma, in list_extensions.more_list]
list_size_tl_compat [lemma, in list_extensions.more_list]
list_sort [library]
l_assoc [axiom, in ac_matching.ac]


M

Make [module, in ac_matching.cf_eq_ac]
Make [module, in term_algebra.rwr_strategies]
Make [module, in ac_matching.matching]
Make [module, in unification.free_unif]
Make [module, in term_orderings.rpo]
Make [module, in term_orderings.inner_dp]
Make [module, in ac_matching.ac]
Make [module, in ac_matching.matching_complete]
Make [module, in list_extensions.dickson]
Make [module, in list_extensions.list_set]
Make [module, in ac_matching.matching_algo]
Make [module, in list_extensions.list_permut]
Make [module, in unification.unification]
Make [module, in list_extensions.list_sort]
Make [module, in examples.cime_trace.equational_extension]
Make [module, in term_algebra.term]
Make [module, in term_algebra.equational_theory]
Make [module, in ac_matching.matching_sound]
Make [module, in term_orderings.term_o]
Make [module, in ac_matching.matching_well_formed]
Make [module, in ac_matching.matching_well_founded]
MakeDP [module, in term_orderings.dp]
MakeDP.acc_interp_acc [lemma, in term_orderings.dp]
MakeDP.acc_interp_dom [lemma, in term_orderings.dp]
MakeDP.acc_one_step_acc_dp [lemma, in term_orderings.dp]
MakeDP.acc_one_step_acc_mdp [lemma, in term_orderings.dp]
MakeDP.acc_rdp_acc_rmdp [lemma, in term_orderings.dp]
MakeDP.acc_subterms_pi [lemma, in term_orderings.dp]
MakeDP.Case12 [lemma, in term_orderings.dp]
MakeDP.Case3 [lemma, in term_orderings.dp]
MakeDP.Ccase [constructor, in term_orderings.dp]
MakeDP.Comb [definition, in term_orderings.dp]
MakeDP.Constr [constructor, in term_orderings.dp]
MakeDP.constructor_defined_dec [lemma, in term_orderings.dp]
MakeDP.Dcase [constructor, in term_orderings.dp]
MakeDP.Defd [constructor, in term_orderings.dp]
MakeDP.defined_dec [lemma, in term_orderings.dp]
MakeDP.defined_list [definition, in term_orderings.dp]
MakeDP.defined_list_complete [lemma, in term_orderings.dp]
MakeDP.defined_list_sound [lemma, in term_orderings.dp]
MakeDP.defined_subterms [definition, in term_orderings.dp]
MakeDP.defined_subterms_accumulates [lemma, in term_orderings.dp]
MakeDP.defined_subterms_complete [lemma, in term_orderings.dp]
MakeDP.def_dec12 [lemma, in term_orderings.dp]
MakeDP.def_dec123' [lemma, in term_orderings.dp]
MakeDP.def_dec132' [lemma, in term_orderings.dp]
MakeDP.def_dec2' [lemma, in term_orderings.dp]
MakeDP.def_dec3' [lemma, in term_orderings.dp]
MakeDP.def_dec_rules [lemma, in term_orderings.dp]
MakeDP.dp [inductive, in term_orderings.dp]
MakeDP.Dp [constructor, in term_orderings.dp]
MakeDP.dp_criterion [lemma, in term_orderings.dp]
MakeDP.dp_criterion_aux [lemma, in term_orderings.dp]
MakeDP.dp_criterion_lift [lemma, in term_orderings.dp]
MakeDP.Dp_gen_step [constructor, in term_orderings.dp]
MakeDP.dp_incl [lemma, in term_orderings.dp]
MakeDP.dp_list [definition, in term_orderings.dp]
MakeDP.dp_list_complete [lemma, in term_orderings.dp]
MakeDP.dp_mdp [lemma, in term_orderings.dp]
MakeDP.dp_necessary [lemma, in term_orderings.dp]
MakeDP.dp_rule [definition, in term_orderings.dp]
MakeDP.Dp_simple_step [constructor, in term_orderings.dp]
MakeDP.dp_step [definition, in term_orderings.dp]
MakeDP.dp_step_incl [lemma, in term_orderings.dp]
MakeDP.Dummy [lemma, in term_orderings.dp]
MakeDP.Empty_R [inductive, in term_orderings.dp]
MakeDP.Empty_R_reg [lemma, in term_orderings.dp]
MakeDP.Equiv_comb [lemma, in term_orderings.dp]
MakeDP.Equiv_empty [lemma, in term_orderings.dp]
MakeDP.FB12 [lemma, in term_orderings.dp]
MakeDP.FB_Pi [lemma, in term_orderings.dp]
MakeDP.Incomp [lemma, in term_orderings.dp]
MakeDP.Incomp1' [definition, in term_orderings.dp]
MakeDP.Incomp12 [lemma, in term_orderings.dp]
MakeDP.Incomp123' [lemma, in term_orderings.dp]
MakeDP.Incomp13 [lemma, in term_orderings.dp]
MakeDP.Incomp2' [definition, in term_orderings.dp]
MakeDP.Incomp23 [lemma, in term_orderings.dp]
MakeDP.Incomp3' [definition, in term_orderings.dp]
MakeDP.Interp [inductive, in term_orderings.dp]
MakeDP.interp_call [inductive, in term_orderings.dp]
MakeDP.interp_defined [lemma, in term_orderings.dp]
MakeDP.Interp_dom [definition, in term_orderings.dp]
MakeDP.interp_dom_R1 [lemma, in term_orderings.dp]
MakeDP.interp_dom_R1_R2 [lemma, in term_orderings.dp]
MakeDP.interp_dom_R1_R2_rwr [lemma, in term_orderings.dp]
MakeDP.interp_dom_R2 [lemma, in term_orderings.dp]
MakeDP.interp_dom_subst [lemma, in term_orderings.dp]
MakeDP.interp_dom_subterm [lemma, in term_orderings.dp]
MakeDP.Interp_subst [definition, in term_orderings.dp]
MakeDP.interp_unicity [lemma, in term_orderings.dp]
MakeDP.interp_well_defined [lemma, in term_orderings.dp]
MakeDP.interp_well_defined_1 [lemma, in term_orderings.dp]
MakeDP.interp_well_defined_2 [lemma, in term_orderings.dp]
MakeDP.interp_well_defined_3 [lemma, in term_orderings.dp]
MakeDP.is_primary_pi [definition, in term_orderings.dp]
MakeDP.list_rules_empty [lemma, in term_orderings.dp]
MakeDP.mark_term [definition, in term_orderings.dp]
MakeDP.mark_term_bij [lemma, in term_orderings.dp]
MakeDP.Mdp [constructor, in term_orderings.dp]
MakeDP.mdp [inductive, in term_orderings.dp]
MakeDP.mdp_criterion [lemma, in term_orderings.dp]
MakeDP.mdp_criterion_strong [lemma, in term_orderings.dp]
MakeDP.mdp_dp [lemma, in term_orderings.dp]
MakeDP.mdp_necessary [lemma, in term_orderings.dp]
MakeDP.modular_termination [lemma, in term_orderings.dp]
MakeDP.modular_termination_hierarch_lift [lemma, in term_orderings.dp]
MakeDP.modular_termination_indep_lift [lemma, in term_orderings.dp]
MakeDP.modular_termination_indep_list_lift [lemma, in term_orderings.dp]
MakeDP.modular_termination_lift [lemma, in term_orderings.dp]
MakeDP.modular_var [lemma, in term_orderings.dp]
MakeDP.module123' [lemma, in term_orderings.dp]
MakeDP.module132' [lemma, in term_orderings.dp]
MakeDP.Pi [inductive, in term_orderings.dp]
MakeDP.Pi1 [constructor, in term_orderings.dp]
MakeDP.Pi2 [constructor, in term_orderings.dp]
MakeDP.Pi_red [definition, in term_orderings.dp]
MakeDP.Pi_red_list [definition, in term_orderings.dp]
MakeDP.pi_subterm [lemma, in term_orderings.dp]
MakeDP.P_comb [lemma, in term_orderings.dp]
MakeDP.P_empty [lemma, in term_orderings.dp]
MakeDP.rdp_step [inductive, in term_orderings.dp]
MakeDP.rdp_step_incl [lemma, in term_orderings.dp]
MakeDP.rdp_step_rmdp_step [lemma, in term_orderings.dp]
MakeDP.recover_red [lemma, in term_orderings.dp]
MakeDP.Rmdp_gen_step [constructor, in term_orderings.dp]
MakeDP.Rmdp_simple_step [constructor, in term_orderings.dp]
MakeDP.rmdp_step [inductive, in term_orderings.dp]
MakeDP.rmdp_step_rdp_step [lemma, in term_orderings.dp]
MakeDP.rwr_rel [inductive, in term_orderings.dp]
MakeDP.rwr_rel_comb [definition, in term_orderings.dp]
MakeDP.rwr_rel_empty [definition, in term_orderings.dp]
MakeDP.R123_reg' [lemma, in term_orderings.dp]
MakeDP.R123_var' [lemma, in term_orderings.dp]
MakeDP.R12_reg [lemma, in term_orderings.dp]
MakeDP.R12_var [lemma, in term_orderings.dp]
MakeDP.R12_var' [lemma, in term_orderings.dp]
MakeDP.R132_reg' [lemma, in term_orderings.dp]
MakeDP.R132_var' [lemma, in term_orderings.dp]
MakeDP.R13_reg [lemma, in term_orderings.dp]
MakeDP.R13_var [lemma, in term_orderings.dp]
MakeDP.R1_at_top [lemma, in term_orderings.dp]
MakeDP.R1_at_top_aux_1 [lemma, in term_orderings.dp]
MakeDP.R1_at_top_aux_2 [lemma, in term_orderings.dp]
MakeDP.R1_at_top_dp [lemma, in term_orderings.dp]
MakeDP.R1_case [lemma, in term_orderings.dp]
MakeDP.R1_R2_case [lemma, in term_orderings.dp]
MakeDP.R1_R2_case_one_step [lemma, in term_orderings.dp]
MakeDP.R1_R2_red [definition, in term_orderings.dp]
MakeDP.R2_case [lemma, in term_orderings.dp]
MakeDP.R2_var' [lemma, in term_orderings.dp]
MakeDP.R3_var' [lemma, in term_orderings.dp]
MakeDP.R_reg_comb [lemma, in term_orderings.dp]
MakeDP.R_reg_empty [lemma, in term_orderings.dp]
MakeDP.R_var_comb [lemma, in term_orderings.dp]
MakeDP.R_var_empty [lemma, in term_orderings.dp]
MakeDP.split_dp [lemma, in term_orderings.dp]
MakeDP.split_dp_top [lemma, in term_orderings.dp]
MakeDP.split_rdp_step [lemma, in term_orderings.dp]
MakeDP.split_rdp_step_top [lemma, in term_orderings.dp]
MakeDP.subterm_at_pos_dec [definition, in term_orderings.dp]
MakeDP.technical_lemma [lemma, in term_orderings.dp]
MakeDP.technical_lemma_1 [lemma, in term_orderings.dp]
MakeDP.T12 [definition, in term_orderings.dp]
MakeDP.T3 [definition, in term_orderings.dp]
MakeDP.unmark_term [definition, in term_orderings.dp]
MakeDP.Vcase [constructor, in term_orderings.dp]
MakeDP.wf_interp_acc [lemma, in term_orderings.dp]
MakeDP.W12' [lemma, in term_orderings.dp]
MakeDP.x_to_x2_commutes_mark [lemma, in term_orderings.dp]
Make' [module, in term_algebra.term]
Make.A [definition, in unification.free_unif]
Make.A [definition, in unification.free_unif]
Make.acc_P_list [lemma, in term_algebra.rwr_strategies]
Make.Acc_R_list [lemma, in examples.cime_trace.equational_extension]
Make.existsb_app [lemma, in examples.cime_trace.equational_extension]
Make.existsb_term_eq_In [lemma, in examples.cime_trace.equational_extension]
Make.Import.bind [definition, in unification.free_unif]
Make.Import.combine [definition, in unification.free_unif]
Make.Import.combine_cons [lemma, in unification.free_unif]
Make.Import.combine_nil [lemma, in unification.free_unif]
Make.Import.combine_proof [lemma, in unification.free_unif]
Make.Import.exc [inductive, in unification.free_unif]
Make.Import.Import.acc_inner_acc [lemma, in term_orderings.inner_dp]
Make.Import.Import.acc_psi_acc [lemma, in term_orderings.inner_dp]
Make.Import.Import.acc_psi_acc_ooo [lemma, in term_orderings.inner_dp]
Make.Import.Import.idp_criterion [lemma, in term_orderings.inner_dp]
Make.Import.Import.idp_criterion_aux [lemma, in term_orderings.inner_dp]
Make.Import.Import.IDp_gen_step [constructor, in term_orderings.inner_dp]
Make.Import.Import.IDp_simple_step [constructor, in term_orderings.inner_dp]
Make.Import.Import.idp_step [inductive, in term_orderings.inner_dp]
Make.Import.Import.map_psi [lemma, in term_orderings.inner_dp]
Make.Import.Import.nf_var [lemma, in term_orderings.inner_dp]
Make.Import.Import.oo [definition, in term_orderings.inner_dp]
Make.Import.Import.ooo [definition, in term_orderings.inner_dp]
Make.Import.Import.psi [definition, in term_orderings.inner_dp]
Make.Import.Import.Psi [inductive, in term_orderings.inner_dp]
Make.Import.Import.Psi_at_top [constructor, in term_orderings.inner_dp]
Make.Import.Import.psi_char [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_def [lemma, in term_orderings.inner_dp]
Make.Import.Import.psi_id [definition, in term_orderings.inner_dp]
Make.Import.Import.psi_inner_axiom [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_in_context [constructor, in term_orderings.inner_dp]
Make.Import.Import.Psi_in_context_bis [lemma, in term_orderings.inner_dp]
Make.Import.Import.psi_nf [lemma, in term_orderings.inner_dp]
Make.Import.Import.psi_not_inner [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_not_nf [lemma, in term_orderings.inner_dp]
Make.Import.Import.psi_not_nf [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_not_refl [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_psi [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_rwr [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_sim_inner [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_sim_inner_at_top [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_sim_one_step [lemma, in term_orderings.inner_dp]
Make.Import.Import.psi_subst [lemma, in term_orderings.inner_dp]
Make.Import.Import.psi_two_cases [lemma, in term_orderings.inner_dp]
Make.Import.Import.Psi_unique [lemma, in term_orderings.inner_dp]
Make.Import.Import.Rreg' [lemma, in term_orderings.inner_dp]
Make.Import.Import.Rvar' [lemma, in term_orderings.inner_dp]
Make.Import.Import.wf_inner_no_wf [lemma, in term_orderings.inner_dp]
Make.Import.Import.wf_inner_wf [lemma, in term_orderings.inner_dp]
Make.Import.is_a_solution [definition, in unification.free_unif]
Make.Import.Normal [constructor, in unification.free_unif]
Make.Import.Not_appliable [constructor, in unification.free_unif]
Make.Import.No_solution [constructor, in unification.free_unif]
Make.Import.Term_eq_dec.A [definition, in unification.free_unif]
Make.Import.Term_eq_dec.A [definition, in unification.free_unif]
Make.Import.Term_eq_dec.eq_dec [definition, in unification.free_unif]
Make.Import.Term_eq_dec.eq_dec [definition, in unification.free_unif]
Make.Import.unification_problem [inductive, in unification.free_unif]
Make.Import.VSet.apply_subst_outside_dom [lemma, in unification.free_unif]
Make.Import.VSet.coalesce1_decreases [lemma, in unification.free_unif]
Make.Import.VSet.coalesce2_decreases [lemma, in unification.free_unif]
Make.Import.VSet.decompose [definition, in unification.free_unif]
Make.Import.VSet.decompose_is_complete [lemma, in unification.free_unif]
Make.Import.VSet.decompose_is_sound [lemma, in unification.free_unif]
Make.Import.VSet.decompose_nf [lemma, in unification.free_unif]
Make.Import.VSet.decompose_unfold [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_decreases [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_e_unfold_normal [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_e_unfold_not_app [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_e_unfold_no_sol [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_step_decreases [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_step_decreases_e [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_step_e [definition, in unification.free_unif]
Make.Import.VSet.decomposition_step_is_complete [lemma, in unification.free_unif]
Make.Import.VSet.decomposition_step_is_sound [lemma, in unification.free_unif]
Make.Import.VSet.domain_of_subst [definition, in unification.free_unif]
Make.Import.VSet.domain_of_subst_map_subst [lemma, in unification.free_unif]
Make.Import.VSet.EDS [definition, in unification.free_unif]
Make.Import.VSet.exc_pb_ok [inductive, in unification.free_unif]
Make.Import.VSet.find_map_subst [lemma, in unification.free_unif]
Make.Import.VSet.F_decompose [definition, in unification.free_unif]
Make.Import.VSet.Inv_solved_part [definition, in unification.free_unif]
Make.Import.VSet.inv_solved_part [lemma, in unification.free_unif]
Make.Import.VSet.inv_solved_part_e [lemma, in unification.free_unif]
Make.Import.VSet.Inv_solved_part_e [definition, in unification.free_unif]
Make.Import.VSet.inv_solved_part_init [lemma, in unification.free_unif]
Make.Import.VSet.is_a_not_solved_var_dec [lemma, in unification.free_unif]
Make.Import.VSet.is_a_solution_e [definition, in unification.free_unif]
Make.Import.VSet.is_a_solved_var [definition, in unification.free_unif]
Make.Import.VSet.is_a_solved_var_dec [lemma, in unification.free_unif]
Make.Import.VSet.lex_le_lt [lemma, in unification.free_unif]
Make.Import.VSet.lex_le_meq_lt [lemma, in unification.free_unif]
Make.Import.VSet.lex_lt [lemma, in unification.free_unif]
Make.Import.VSet.list_size_mul [definition, in unification.free_unif]
Make.Import.VSet.list_size_mul_app [lemma, in unification.free_unif]
Make.Import.VSet.lt_exc_pb_ok [definition, in unification.free_unif]
Make.Import.VSet.lt_ms [definition, in unification.free_unif]
Make.Import.VSet.lt_mul [definition, in unification.free_unif]
Make.Import.VSet.lt_pb [definition, in unification.free_unif]
Make.Import.VSet.lt_weight_exc_pb_ok [definition, in unification.free_unif]
Make.Import.VSet.measure_for_unif_pb [definition, in unification.free_unif]
Make.Import.VSet.measure_for_unif_pb_swapp_eq [lemma, in unification.free_unif]
Make.Import.VSet.merge1_decreases [lemma, in unification.free_unif]
Make.Import.VSet.merge2_decreases [lemma, in unification.free_unif]
Make.Import.VSet.move_eq_decreases [lemma, in unification.free_unif]
Make.Import.VSet.nb_var_eq_of_unsolved_part [definition, in unification.free_unif]
Make.Import.VSet.not_solved_var [lemma, in unification.free_unif]
Make.Import.VSet.occ_var_is_a_subterm_at_pos [lemma, in unification.free_unif]
Make.Import.VSet.OK [constructor, in unification.free_unif]
Make.Import.VSet.phi1 [definition, in unification.free_unif]
Make.Import.VSet.phi2 [definition, in unification.free_unif]
Make.Import.VSet.phi3 [definition, in unification.free_unif]
Make.Import.VSet.remove_trivial_eq_decreases [lemma, in unification.free_unif]
Make.Import.VSet.set_of_variables [definition, in unification.free_unif]
Make.Import.VSet.set_of_variables_in_range_of_subst [definition, in unification.free_unif]
Make.Import.VSet.set_of_variables_in_unsolved_part [definition, in unification.free_unif]
Make.Import.VSet.set_of_variables_list [definition, in unification.free_unif]
Make.Import.VSet.size_of_solved_part [definition, in unification.free_unif]
Make.Import.VSet.size_of_unsolved_part [definition, in unification.free_unif]
Make.Import.VSet.solved_var_inc_list [lemma, in unification.free_unif]
Make.Import.VSet.solved_var_inc_not_mem [lemma, in unification.free_unif]
Make.Import.VSet.solved_var_inc_not_mem_list [lemma, in unification.free_unif]
Make.Import.VSet.solved_var_inc_not_mem_subst [lemma, in unification.free_unif]
Make.Import.VSet.solved_var_inc_occ_in_subst [lemma, in unification.free_unif]
Make.Import.VSet.solved_var_inc_subst [lemma, in unification.free_unif]
Make.Import.VSet.solved_var_inc_term [lemma, in unification.free_unif]
Make.Import.VSet.solved_var_swapp_eq [lemma, in unification.free_unif]
Make.Import.VSet.VSet_compat [lemma, in unification.free_unif]
Make.Import.VSet.weight_exc_pb_ok [definition, in unification.free_unif]
Make.Import.VSet.wf_lt_exc_pb_ok [lemma, in unification.free_unif]
Make.Import.VSet.wf_lt_ms [lemma, in unification.free_unif]
Make.Import.VSet.wf_lt_pb [lemma, in unification.free_unif]
Make.inner [definition, in term_algebra.rwr_strategies]
Make.In_existsb_term_eq [lemma, in examples.cime_trace.equational_extension]
Make.Monotone [inductive, in examples.cime_trace.equational_extension]
Make.Monotone_c [constructor, in examples.cime_trace.equational_extension]
Make.nf_dec_inner_dec [lemma, in term_algebra.rwr_strategies]
Make.nf_P_step_subterm [lemma, in term_algebra.rwr_strategies]
Make.one_step_nf_inner_step_nf [lemma, in term_algebra.rwr_strategies]
Make.P_acc_subterms [lemma, in term_algebra.rwr_strategies]
Make.P_acc_subterms_1 [lemma, in term_algebra.rwr_strategies]
Make.P_acc_subterms_3 [lemma, in term_algebra.rwr_strategies]
Make.P_acc_with_subterm [lemma, in term_algebra.rwr_strategies]
Make.P_acc_with_subterm_subterms [lemma, in term_algebra.rwr_strategies]
Make.P_at_top [constructor, in term_algebra.rwr_strategies]
Make.P_context_cons [lemma, in term_algebra.rwr_strategies]
Make.P_context_in [lemma, in term_algebra.rwr_strategies]
Make.P_general_context [lemma, in term_algebra.rwr_strategies]
Make.P_general_context_aux [lemma, in term_algebra.rwr_strategies]
Make.P_head_step [constructor, in term_algebra.rwr_strategies]
Make.P_in_context [constructor, in term_algebra.rwr_strategies]
Make.P_list [inductive, in term_algebra.rwr_strategies]
Make.P_list_expand [lemma, in term_algebra.rwr_strategies]
Make.P_list_length_eq [lemma, in term_algebra.rwr_strategies]
Make.P_step [inductive, in term_algebra.rwr_strategies]
Make.P_step_context_in [lemma, in term_algebra.rwr_strategies]
Make.P_step_in_list [lemma, in term_algebra.rwr_strategies]
Make.P_step_one_step [lemma, in term_algebra.rwr_strategies]
Make.P_tail_step [constructor, in term_algebra.rwr_strategies]
Make.RST [inductive, in examples.cime_trace.equational_extension]
Make.RSTSN [lemma, in examples.cime_trace.equational_extension]
Make.RSTSN_symb [lemma, in examples.cime_trace.equational_extension]
Make.RST_c [constructor, in examples.cime_trace.equational_extension]
Make.rwr_inner_or_eq [lemma, in term_algebra.rwr_strategies]
Make.rwr_inner_or_eq_bis [lemma, in term_algebra.rwr_strategies]
Make.rwr_inner_or_eq_subst [lemma, in term_algebra.rwr_strategies]
Make.R_list [definition, in examples.cime_trace.equational_extension]
Make.R_list_Acc [lemma, in examples.cime_trace.equational_extension]
Make.ST [definition, in examples.cime_trace.equational_extension]
Make.STb [definition, in examples.cime_trace.equational_extension]
Make.STb_equiv [lemma, in examples.cime_trace.equational_extension]
Make.STPb [definition, in examples.cime_trace.equational_extension]
Make.STPSN [lemma, in examples.cime_trace.equational_extension]
Make.STP_equiv [lemma, in examples.cime_trace.equational_extension]
Make.STSN [lemma, in examples.cime_trace.equational_extension]
Make.term_eq [definition, in examples.cime_trace.equational_extension]
Make.term_eq_ok [lemma, in examples.cime_trace.equational_extension]
Make.term_eq_refl [lemma, in examples.cime_trace.equational_extension]
Make.trans_clos_P_list_expand [lemma, in term_algebra.rwr_strategies]
Make.trans_clos_P_list_P_list [lemma, in term_algebra.rwr_strategies]
Make.trans_clos_P_list_split [lemma, in term_algebra.rwr_strategies]
Make.trans_clos_P_step_P_list [lemma, in term_algebra.rwr_strategies]
Make.var_P_acc [lemma, in term_algebra.rwr_strategies]
Make.Well_Founded_ST [lemma, in examples.cime_trace.equational_extension]
Make_EQTH_facts [module, in examples.cime_trace.rpo_extension]
Make_EQTH_facts.one_step_list_star_decompose_cons [lemma, in examples.cime_trace.rpo_extension]
Make_EQTH_facts.one_step_list_star_decompose_nil [lemma, in examples.cime_trace.rpo_extension]
Make_EQTH_facts.one_step_list_star_l [lemma, in examples.cime_trace.rpo_extension]
Make_EQTH_facts.one_step_list_star_r [lemma, in examples.cime_trace.rpo_extension]
Make_EQTH_facts.rwr_as_star [lemma, in examples.cime_trace.rpo_extension]
mapi [definition, in list_extensions.more_list]
mapii [definition, in list_extensions.more_list]
mapii_dep [definition, in list_extensions.more_list]
mapii_dep_eq [lemma, in list_extensions.more_list]
mapii_dep_spec [lemma, in list_extensions.more_list]
mapii_dep_unfold [lemma, in list_extensions.more_list]
mapii_spec [lemma, in list_extensions.more_list]
mapi_spec [lemma, in list_extensions.more_list]
map_dep_call [lemma, in list_extensions.more_list]
map_duplicate [lemma, in list_extensions.more_list]
map_eq [lemma, in list_extensions.more_list]
map_id [lemma, in list_extensions.more_list]
matching [axiom, in term_algebra.term]
matching [library]
matching_algo [library]
matching_complete [axiom, in term_algebra.term]
matching_complete [library]
matching_correct [axiom, in term_algebra.term]
matching_is_complete [axiom, in ac_matching.matching_algo]
matching_is_sound [axiom, in ac_matching.matching_algo]
matching_sound [library]
matching_unfold2 [axiom, in term_algebra.term]
matching_well_formed [library]
matching_well_founded [library]
math_permut [library]
mem [definition, in list_extensions.more_list]
mem_dec [axiom, in list_extensions.list_set]
mem_dec [axiom, in list_extensions.list_permut]
mem_insert [axiom, in list_extensions.list_permut]
mem_or_app [axiom, in list_extensions.list_permut]
mem_permut_mem [axiom, in list_extensions.list_permut]
mem_split_set [axiom, in list_extensions.list_permut]
merge [definition, in list_extensions.more_list]
merge_correct [lemma, in list_extensions.more_list]
merge_inv [lemma, in list_extensions.more_list]
more_list [library]
Mul [constructor, in term_orderings.rpo]
multiset_closure [axiom, in list_extensions.dickson]


N

Nat [module, in basis.ordered_set]
Nat.A [definition, in basis.ordered_set]
Nat.A [definition, in basis.ordered_set]
Nat.eq_dec [lemma, in basis.ordered_set]
Nat.o [definition, in basis.ordered_set]
Nat.o_dec [lemma, in basis.ordered_set]
Nat.o_proof [lemma, in basis.ordered_set]
Nat.o_total [lemma, in basis.ordered_set]
nb_occ_app [lemma, in list_extensions.more_list]
nf [definition, in basis.closure]
nf_one_step_subterm [axiom, in term_algebra.equational_theory]
nf_rwr_subterm [axiom, in term_algebra.equational_theory]
none_nb_occ_O [lemma, in list_extensions.more_list]
no_infinite_sequence2 [lemma, in examples.cime_trace.rewriting]
no_need_of_instance_is_modular [axiom, in term_algebra.equational_theory]
nth_error_at_pos [lemma, in list_extensions.more_list]
nth_error_map [lemma, in list_extensions.more_list]
nth_error_nil [lemma, in list_extensions.more_list]
nth_error_ok_in [lemma, in list_extensions.more_list]
nth_error_remove [lemma, in list_extensions.more_list]


O

o [axiom, in basis.ordered_set]
o [axiom, in basis.ordered_set]
OF [module, in term_orderings.term_o]
one_step_apply_subst [axiom, in term_algebra.equational_theory]
one_step_at_pos [axiom, in term_algebra.equational_theory]
one_step_context_in [axiom, in term_algebra.equational_theory]
one_step_in_list [axiom, in term_algebra.equational_theory]
one_step_list_length_eq [axiom, in term_algebra.equational_theory]
one_step_list_rwr_list [axiom, in term_algebra.equational_theory]
ordered_set [library]
OX [module, in term_orderings.term_o]
o_compat [axiom, in basis.ordered_set]
o_dec [axiom, in basis.ordered_set]
o_dec [axiom, in term_orderings.term_o]
o_dec [axiom, in basis.ordered_set]
o_length [definition, in list_extensions.more_list]
o_proof [axiom, in basis.ordered_set]
o_proof [axiom, in term_orderings.term_o]
o_proof [axiom, in basis.ordered_set]
o_total [axiom, in basis.ordered_set]
o_total [axiom, in term_orderings.term_o]
o_total [axiom, in basis.ordered_set]


P

Pcons [constructor, in list_extensions.list_permut]
permut [definition, in list_extensions.math_permut]
permut [inductive, in list_extensions.list_permut]
permutation [definition, in list_extensions.math_permut]
permut_add_inside [axiom, in list_extensions.list_permut]
permut_add_inside [lemma, in list_extensions.list_permut]
permut_app [lemma, in list_extensions.list_permut]
permut_app1 [axiom, in list_extensions.list_permut]
permut_app1 [lemma, in list_extensions.list_permut]
permut_app2 [axiom, in list_extensions.list_permut]
permut_app2 [lemma, in list_extensions.list_permut]
permut_closure [lemma, in list_extensions.math_permut]
permut_cons [axiom, in list_extensions.list_permut]
permut_cons_inside [axiom, in list_extensions.list_permut]
permut_cons_inside [lemma, in list_extensions.list_permut]
permut_dec [axiom, in list_extensions.list_permut]
permut_dec [lemma, in list_extensions.list_permut]
permut_impl [lemma, in list_extensions.list_permut]
permut_inv_left_strong [lemma, in list_extensions.list_permut]
permut_inv_right [lemma, in list_extensions.list_permut]
permut_inv_right_strong [lemma, in list_extensions.list_permut]
permut_length [lemma, in list_extensions.list_permut]
permut_length_1 [lemma, in list_extensions.list_permut]
permut_length_2 [lemma, in list_extensions.list_permut]
permut_list_exists [lemma, in list_extensions.list_permut]
permut_list_forall_exists [lemma, in list_extensions.list_permut]
permut_map [lemma, in list_extensions.list_permut]
permut_nil [lemma, in list_extensions.list_permut]
permut_refl [axiom, in list_extensions.list_permut]
permut_refl [lemma, in list_extensions.list_permut]
permut_rev [lemma, in list_extensions.list_permut]
permut_size [lemma, in list_extensions.list_permut]
permut_strong [lemma, in list_extensions.list_permut]
permut_swapp [lemma, in list_extensions.list_permut]
permut_sym [lemma, in list_extensions.list_permut]
permut_sym [axiom, in list_extensions.list_permut]
permut_trans [axiom, in list_extensions.list_permut]
permut_trans [lemma, in list_extensions.list_permut]
Pnil [constructor, in list_extensions.list_permut]
pos_expr_if_all_pos [lemma, in examples.cime_trace.ring_extention]
pos_expr_if_all_pos' [lemma, in examples.cime_trace.ring_extention]
pos_expr_if_all_pos_aux [lemma, in examples.cime_trace.ring_extention]
pos_expr_if_all_pos_aux' [lemma, in examples.cime_trace.ring_extention]
pos_expr_incr [lemma, in examples.cime_trace.ring_extention]
pos_expr_incr_aux [lemma, in examples.cime_trace.ring_extention]
pos_pol_incr [lemma, in examples.cime_trace.ring_extention]
pos_pol_incr' [lemma, in examples.cime_trace.ring_extention]
Pphi_nil [lemma, in examples.cime_trace.ring_extention]
prec [axiom, in term_orderings.rpo]
Precedence [module, in term_orderings.rpo]
prec_antisym [axiom, in term_orderings.rpo]
prec_dec [axiom, in term_orderings.rpo]
prec_transitive [axiom, in term_orderings.rpo]
product_o [inductive, in basis.closure]
prop_map12_without_repetition [lemma, in list_extensions.more_list]
prop_map_without_repetition [lemma, in list_extensions.more_list]


Q

quicksort [axiom, in list_extensions.list_sort]
quicksort_equation [axiom, in list_extensions.list_sort]
quick_permut [axiom, in list_extensions.list_sort]
quick_permut_bis [axiom, in list_extensions.list_sort]
quick_sorted [axiom, in list_extensions.list_sort]


R

reduce_assoc_list [lemma, in list_extensions.more_list]
refl_trans_clos [inductive, in basis.closure]
remove_equiv_is_sound [axiom, in list_extensions.list_permut]
remove_garbage_subst [axiom, in term_algebra.term]
remove_is_sound [axiom, in list_extensions.list_permut]
replace_at_pos_in_replace_at_pos [axiom, in term_algebra.term]
replace_at_pos_is_replace_at_pos1 [axiom, in term_algebra.term]
replace_at_pos_is_replace_at_pos2 [axiom, in term_algebra.term]
replace_at_pos_list_replace_at_pos_in_subterm [axiom, in term_algebra.term]
replace_at_pos_replace_at_pos [axiom, in term_algebra.term]
replace_at_pos_unfold [axiom, in term_algebra.term]
restrict_domain_ok [axiom, in term_algebra.term]
restrict_domain_ok2 [axiom, in term_algebra.term]
Retoile [definition, in examples.cime_trace.rewriting]
rewriting [library]
ring_extention [library]
RPO [module, in term_orderings.rpo]
rpo [library]
RPO.Import.Import.A [definition, in term_orderings.rpo]
RPO.Import.Import.Eq [constructor, in term_orderings.rpo]
RPO.Import.Import.equiv [inductive, in term_orderings.rpo]
RPO.Import.Import.equiv_list_lex [inductive, in term_orderings.rpo]
RPO.Import.Import.Eq_lex [constructor, in term_orderings.rpo]
RPO.Import.Import.Eq_list_cons [constructor, in term_orderings.rpo]
RPO.Import.Import.Eq_list_nil [constructor, in term_orderings.rpo]
RPO.Import.Import.Eq_mul [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.EDS [definition, in term_orderings.rpo]
RPO.Import.Import.Import.EDS [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Equiv [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.List_eq [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.List_gt [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.List_mul [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Lt [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.A [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_dec [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_equiv [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_list_lex [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_same_length [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_same_size [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_same_top [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_lex [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_list_cons [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_list_nil [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_mul [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.acc_build [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.add_equiv [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.empty_rpo_infos [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Equiv [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_acc_rpo [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_add_context [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_equation [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_is_complete_true [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_is_sound_weak [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_list_fully_evaluates [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_list_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_terminates [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_1 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_2 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_3 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_4 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_subst [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.find_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Found [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval_equation [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval_fully_evaluates [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_eq [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_gt [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_mul [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_mul_step [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.list_permut_map_acc [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Lt [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mem_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mult_eval [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mult_eval_fully_evaluates [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mult_eval_is_sound_weak [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Not_finished [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Not_found [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.prec_eval [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.prec_eval_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_fully_evaluates [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_list_fully_evaluates [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_list_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_is_sound_none [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_is_sound_some [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_list_is_sound [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.result [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_add_context [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_antirefl [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_closure [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_dec [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eq [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_equation [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_complete [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_complete_equivalent [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_complete_less_greater [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_sound_weak [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_terminates [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_inf [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_lex [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_lex_rest [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Rpo_lex_rest [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_lex_same_length [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_remove_equiv_aux [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Rpo_mul_rest [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_rest [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_rest_trans_clos [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_step [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_step_rest [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Rpo_mul_step_rest [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_trans_clos [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_rest [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subst [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subterm [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subterm_equiv [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subterm_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_trans [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size2_lex1_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size2_lex2_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size3_lex1_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size3_lex2_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size3_lex3_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size_direct_subterm_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Subterm [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.term_rec3_mem [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_lex [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_lex_rest [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_mul [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_mul_rest [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_gt [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_gt_rest [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.trans_clos_subterm_rpo [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.two_cases_rpo [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.var_case2 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.well_formed_equiv [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.well_formed_list_is_well_formed_list [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo_lex_rest [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo_mul_rest [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo_rest [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size2 [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size2_trans [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size3 [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size3_trans [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2 [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex1 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex1_bis [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex2 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex2_bis [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3 [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex1 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex1_bis [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex2 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex3 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.A [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.A [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_A [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_A [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_dec [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_dec [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_proof [definition, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.wf_size [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.wf_size2 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.wf_size3 [lemma, in term_orderings.rpo]
RPO.Import.Import.Import.rpo [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.rpo_eq [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.rpo_lex [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.rpo_mul [inductive, in term_orderings.rpo]
RPO.Import.Import.Import.Subterm [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Top_eq_lex [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Top_eq_mul [constructor, in term_orderings.rpo]
RPO.Import.Import.Import.Top_gt [constructor, in term_orderings.rpo]
rpo_add_context [axiom, in term_orderings.rpo]
rpo_closure [axiom, in term_orderings.rpo]
rpo_dec [axiom, in term_orderings.rpo]
rpo_extension [library]
rpo_facts [module, in examples.cime_trace.rpo_extension]
rpo_facts.A [definition, in examples.cime_trace.rpo_extension]
rpo_facts.apply_subst_in [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.equiv_add_context [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.equiv_in_list [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.equiv_refl [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.equiv_subst [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.equiv_sym [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.equiv_trans [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.In_map_l [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.map_map_fst [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.map_map_snd [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.one_R_in_rpo [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.one_R_in_rpo_eq [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_add_context [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_in_list [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_subst [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_trans [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.rpo_in_list [lemma, in examples.cime_trace.rpo_extension]
rpo_facts.wf_prec_implies_wf_R [lemma, in examples.cime_trace.rpo_extension]
rpo_subst [axiom, in term_orderings.rpo]
rpo_trans [axiom, in term_orderings.rpo]
rwr_apply_subst [axiom, in term_algebra.equational_theory]
rwr_at_pos [axiom, in term_algebra.equational_theory]
rwr_closure [axiom, in term_algebra.equational_theory]
rwr_closure_one_step [axiom, in term_algebra.equational_theory]
rwr_inv [axiom, in term_algebra.equational_theory]
rwr_list_is_trans [axiom, in term_algebra.equational_theory]
rwr_list_length_eq [axiom, in term_algebra.equational_theory]
rwr_list_trans_clos_one_step_list [axiom, in term_algebra.equational_theory]
rwr_or_eq [axiom, in term_algebra.equational_theory]
rwr_or_eq_subst [axiom, in term_algebra.equational_theory]
rwr_R1_included_in_R2 [axiom, in term_algebra.equational_theory]
rwr_strategies [library]
R1_included_in_R2_axiom [axiom, in term_algebra.equational_theory]
R1_included_in_R2_one_step [axiom, in term_algebra.equational_theory]
R1_included_in_R2_rwr [axiom, in term_algebra.equational_theory]
R1_included_in_R2_rwr_list [axiom, in term_algebra.equational_theory]
R2 [inductive, in examples.cime_trace.rewriting]
R2_intro [constructor, in examples.cime_trace.rewriting]
r_assoc [axiom, in ac_matching.ac]
R_axiom [axiom, in term_algebra.equational_theory]
R_one_step [axiom, in term_algebra.equational_theory]
R_rwr [axiom, in term_algebra.equational_theory]
r_trans [constructor, in basis.closure]


S

S [module, in ac_matching.matching_sound]
S [module, in ac_matching.matching]
S [module, in ac_matching.matching_complete]
S [module, in ac_matching.matching_well_formed]
S [module, in ac_matching.ac]
S [module, in ac_matching.cf_eq_ac]
S [module, in basis.ordered_set]
S [module, in list_extensions.list_permut]
S [module, in ac_matching.matching_well_founded]
S [module, in ac_matching.matching_algo]
S [module, in basis.decidable_set]
S [module, in list_extensions.list_set]
Signature [module, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.apply_subst [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.direct_subterm [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.EDS [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.EDS [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.is_a_pos [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.apply_subst [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.apply_subst_const [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.direct_subterm [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.EDS [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.EDS [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.empty_subst_is_id [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.empty_subst_is_id_list [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.eq_term_dec [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.exists_subterm_is_a_pos [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.F_matching [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.is_a_pos [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.is_a_pos_exists_subterm [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.map_subst [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_call1 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_call2 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_call3 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_complete [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_correct [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_correct_aux [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_unfold [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_unfold2 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.o_list_size [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.remove_garbage_subst [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_in_replace_at_pos [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_is_replace_at_pos1 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_is_replace_at_pos2 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_list_replace_at_pos_in_subterm [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_replace_at_pos [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_unfold [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.restrict_domain [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.restrict_domain_ok [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.restrict_domain_ok2 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_direct_subterm [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_ge_one [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_subterm_at_pos [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_unfold [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.substitution [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp_is_subst_comp [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp_is_subst_comp_aux1 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp_is_subst_comp_aux2 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_eq_vars [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_at_pos [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_at_pos_dec [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_in_instantiated_term [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_in_subterm [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_in_subterm2 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_subterm [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_direct_subterm [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_subterm [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term_list_app [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term_unfold [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.Term [constructor, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term [inductive, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec2 [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec3 [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec4 [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec7 [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec8 [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_term_dec [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.Var [constructor, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_in_subterm [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_in_subterm2 [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_list_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_list_unfold [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_apply_subst [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_fold [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_subst [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_unfold [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.wf_size [lemma, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.map_subst [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.replace_at_pos [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.replace_at_pos_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.restrict_domain [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.size [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.substitution [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.subst_comp [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.subterm_at_pos [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.symb_in_term [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.symb_in_term_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Term [constructor, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.term [inductive, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Var [constructor, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.var_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.var_list_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.well_formed [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.well_formed_list [definition, in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.well_formed_subst [definition, in term_algebra.term]
size_direct_subterm [axiom, in term_algebra.term]
size_ge_one [axiom, in term_algebra.term]
size_size [axiom, in ac_matching.ac]
size_size_aux3 [axiom, in ac_matching.ac]
size_subterm_at_pos [axiom, in term_algebra.term]
size_unfold [axiom, in term_algebra.term]
SN_incl [lemma, in examples.cime_trace.rewriting]
solve_is_complete [axiom, in ac_matching.matching_complete]
solve_is_sound [axiom, in ac_matching.matching_sound]
some_nb_occ_Sn [lemma, in list_extensions.more_list]
Sort [module, in list_extensions.list_sort]
sorted_tl_sorted [axiom, in list_extensions.list_sort]
Sort.Import.Import.EDS [definition, in list_extensions.list_sort]
Sort.Import.Import.EDS [definition, in list_extensions.list_sort]
Sort.Import.Import.is_sorted [inductive, in list_extensions.list_sort]
Sort.Import.Import.is_sorted_cons1 [constructor, in list_extensions.list_sort]
Sort.Import.Import.is_sorted_cons2 [constructor, in list_extensions.list_sort]
Sort.Import.Import.is_sorted_nil [constructor, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.EDS [definition, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.EDS [definition, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.in_quicksort_cons [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.in_quick_in [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.in_remove_list [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted [inductive, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted_cons1 [constructor, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted_cons2 [constructor, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted_nil [constructor, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.length_quicksort [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.partition_list_permut1 [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_permut [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_permut_bis [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted_aux1 [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted_aux3 [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted_aux4 [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.sorted_cons_min [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.sorted_tl_sorted [lemma, in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.sort_is_unique [lemma, in list_extensions.list_sort]
sort_is_unique [axiom, in list_extensions.list_sort]
split_all [definition, in list_extensions.list_permut]
split_all_is_sound [lemma, in list_extensions.list_permut]
split_list [lemma, in list_extensions.more_list]
split_map [lemma, in list_extensions.more_list]
split_rel [axiom, in term_algebra.equational_theory]
star [inductive, in examples.cime_trace.terminaison]
star_R [lemma, in examples.cime_trace.terminaison]
star_refl [constructor, in examples.cime_trace.terminaison]
star_step [constructor, in examples.cime_trace.terminaison]
star_trans [lemma, in examples.cime_trace.terminaison]
status [axiom, in term_orderings.rpo]
status_type [inductive, in term_orderings.rpo]
strict_pos_expr_if_all_pos [lemma, in examples.cime_trace.ring_extention]
strict_pos_expr_if_all_pos' [lemma, in examples.cime_trace.ring_extention]
strict_pos_expr_if_all_pos_aux [lemma, in examples.cime_trace.ring_extention]
strict_pos_expr_if_all_pos_aux' [lemma, in examples.cime_trace.ring_extention]
subst_comp_is_subst_comp [axiom, in term_algebra.term]
subst_comp_is_subst_comp_aux1 [axiom, in term_algebra.term]
subst_eq_vars [axiom, in term_algebra.term]
subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [axiom, in term_algebra.term]
subterm_at_pos_dec [axiom, in term_algebra.term]
subterm_in_instantiated_term [axiom, in term_algebra.term]
subterm_in_subterm [axiom, in term_algebra.term]
subterm_in_subterm2 [axiom, in term_algebra.term]
subterm_subterm [axiom, in term_algebra.term]
symb_in_direct_subterm [axiom, in term_algebra.term]
symb_in_subterm [axiom, in term_algebra.term]
symb_in_term_list_app [axiom, in term_algebra.term]
symb_in_term_unfold [axiom, in term_algebra.term]
S.Import.ac_elementary_solve [definition, in ac_matching.matching]
S.Import.ac_elementary_solve_term_term_term [definition, in ac_matching.matching]
S.Import.ac_elementary_solve_term_var_without_val_term [definition, in ac_matching.matching]
S.Import.ac_elementary_solve_term_var_with_part_val_term [definition, in ac_matching.matching]
S.Import.ac_elementary_solve_term_var_with_val_term [definition, in ac_matching.matching]
S.Import.build_well_formed_matching_problem_list [definition, in ac_matching.matching_algo]
S.Import.clean_sol [definition, in ac_matching.matching_algo]
S.Import.extract_solution [definition, in ac_matching.matching_algo]
S.Import.F_wf_solve [definition, in ac_matching.matching_algo]
S.Import.Import.cardinal [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_comm [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_prf [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_12 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_eq_set [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_subset [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union_inter_12 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.empty [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_mem_mem [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_dec [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_list_permut_support [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_refl [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_sym [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_trans [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_union [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_1_list [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_2_list [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.included_filter_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.included_remove_red [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_12 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_12_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_1_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_2_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.make_set [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.mem [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.mem_dec [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.not_mem_dec [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.not_mem_eq [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.remove_red_included [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.set_diff [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.singleton [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.strict_subset_set_diff [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_cardinal_not_eq_not_eq_set [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_compat [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_compat_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_compat_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_dec [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_filter [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_inter_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_inter_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_set_diff [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_subset_union [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_union_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_union_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.t [inductive, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union [definition, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_assoc [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_comm [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_compat_eq_set [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_compat_subset_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_compat_subset_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_empty_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_empty_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_1 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_12 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_12_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_1_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_2 [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_2_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_add_without_red [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_filter_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_nil [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_not_in [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_permut [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove_not_common [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove_not_common_aux [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove_red [lemma, in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_singleton [lemma, in list_extensions.list_set]
S.Import.Import.mem [definition, in list_extensions.list_set]
S.Import.Import.subset [definition, in list_extensions.list_set]
S.Import.Import.t [inductive, in list_extensions.list_set]
S.Import.Import.without_red [definition, in list_extensions.list_set]
S.Import.init_pb [definition, in ac_matching.matching_algo]
S.Import.is_rough_sol [definition, in ac_matching.matching]
S.Import.is_sol [definition, in ac_matching.matching]
S.Import.is_well_formed_sol [definition, in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve [definition, in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_term_term [definition, in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_var_without_val_term [definition, in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_var_with_part_val_term [definition, in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_var_with_val_term [definition, in ac_matching.matching]
S.Import.Make.Import.ac_size_build_eq [lemma, in ac_matching.matching_well_founded]
S.Import.Make.Import.ac_size_build_lt [lemma, in ac_matching.matching_well_founded]
S.Import.Make.Import.ac_size_build_lt_args [lemma, in ac_matching.matching_well_founded]
S.Import.Make.Import.ac_syntactic [lemma, in list_extensions.list_permut]
S.Import.Make.Import.ac_syntactic_aux [lemma, in list_extensions.list_permut]
S.Import.Make.Import.add_a_subterm [lemma, in ac_matching.matching_sound]
S.Import.Make.Import.add_a_subterm_subst [lemma, in ac_matching.matching_sound]
S.Import.Make.Import.add_new_var_to_rough_sol [lemma, in ac_matching.matching]
S.Import.Make.Import.add_new_var_to_subst [lemma, in ac_matching.matching]
S.Import.Make.Import.associativity [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.build_well_formed_matching_problem_list [definition, in ac_matching.matching_algo]
S.Import.Make.Import.cf_eq_ac [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.clean_sol [definition, in ac_matching.matching_algo]
S.Import.Make.Import.commutativity [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.cons_permut_mem [lemma, in list_extensions.list_permut]
S.Import.Make.Import.diff_mem_remove [lemma, in list_extensions.list_permut]
S.Import.Make.Import.extract_solution [definition, in ac_matching.matching_algo]
S.Import.Make.Import.extract_solution_in_partly_solved_part [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.extract_solution_in_solved_part [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.extract_solution_unfold [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.F_wf_solve [definition, in ac_matching.matching_algo]
S.Import.Make.Import.F_wf_solve_dec1 [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.F_wf_solve_dec2 [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.init_pb [definition, in ac_matching.matching_algo]
S.Import.Make.Import.in_impl_mem [lemma, in list_extensions.list_permut]
S.Import.Make.Import.is_rough_sol [definition, in ac_matching.matching]
S.Import.Make.Import.is_sol [definition, in ac_matching.matching]
S.Import.Make.Import.is_well_formed_sol [definition, in ac_matching.matching]
S.Import.Make.Import.is_wf_sol [definition, in ac_matching.matching_algo]
S.Import.Make.Import.is_wf_wf_sol [definition, in ac_matching.matching_algo]
S.Import.Make.Import.list_permut_app_app [lemma, in list_extensions.list_permut]
S.Import.Make.Import.list_permut_occurs_in_term_list [lemma, in ac_matching.matching]
S.Import.Make.Import.matching [definition, in ac_matching.matching_algo]
S.Import.Make.Import.matching_is_complete [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.matching_is_sound [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.matching_problem [inductive, in ac_matching.matching]
S.Import.Make.Import.matching_step1_is_complete [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.matching_step1_is_sound [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.matching_step2_is_complete [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.matching_step2_is_sound [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.mem [definition, in list_extensions.list_permut]
S.Import.Make.Import.mem_dec [lemma, in list_extensions.list_permut]
S.Import.Make.Import.mem_insert [lemma, in list_extensions.list_permut]
S.Import.Make.Import.mem_or_app [lemma, in list_extensions.list_permut]
S.Import.Make.Import.mem_permut_mem [lemma, in list_extensions.list_permut]
S.Import.Make.Import.mem_split_set [lemma, in list_extensions.list_permut]
S.Import.Make.Import.middle_commutativity [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.new_var_occ_in_solved_part [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.occurs_in_pb [definition, in ac_matching.matching]
S.Import.Make.Import.occurs_in_term [definition, in ac_matching.matching]
S.Import.Make.Import.occurs_in_term_list [definition, in ac_matching.matching]
S.Import.Make.Import.o_lpb [definition, in ac_matching.matching_algo]
S.Import.Make.Import.partly_solved_term [inductive, in ac_matching.matching]
S.Import.Make.Import.pb_weight [definition, in ac_matching.matching_well_founded]
S.Import.Make.Import.permut_add_inside [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_app1 [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_app2 [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_cons [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_cons_inside [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_dec [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_refl [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_sym [lemma, in list_extensions.list_permut]
S.Import.Make.Import.permut_trans [lemma, in list_extensions.list_permut]
S.Import.Make.Import.remove_a_subterm [lemma, in ac_matching.matching_complete]
S.Import.Make.Import.remove_equiv_is_sound [lemma, in list_extensions.list_permut]
S.Import.Make.Import.remove_is_sound [lemma, in list_extensions.list_permut]
S.Import.Make.Import.remove_several_subterms [lemma, in ac_matching.matching_complete]
S.Import.Make.Import.remove_several_subterms_bis [lemma, in ac_matching.matching_complete]
S.Import.Make.Import.remove_several_subterms_bis_nil [lemma, in ac_matching.matching_complete]
S.Import.Make.Import.solve [definition, in ac_matching.matching]
S.Import.Make.Import.solve_is_complete [lemma, in ac_matching.matching_complete]
S.Import.Make.Import.solve_is_sound [lemma, in ac_matching.matching_sound]
S.Import.Make.Import.split_cf [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.swap_left [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.swap_right [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.syntactic_dec [lemma, in ac_matching.cf_eq_ac]
S.Import.Make.Import.variable_preservation [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.W [constructor, in ac_matching.matching_algo]
S.Import.Make.Import.weight_is_weight [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.well_formed_init_pb [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.well_formed_matching_problem [inductive, in ac_matching.matching_algo]
S.Import.Make.Import.well_formed_pb [definition, in ac_matching.matching]
S.Import.Make.Import.well_formed_solve [lemma, in ac_matching.matching_well_formed]
S.Import.Make.Import.well_founded_o_lpb [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.well_founded_solve [lemma, in ac_matching.matching_well_founded]
S.Import.Make.Import.well_sorted_partly_solved_part [definition, in ac_matching.matching]
S.Import.Make.Import.wfpb_weight [definition, in ac_matching.matching_algo]
S.Import.Make.Import.wf_projection [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve [definition, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_cons [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_is_complete [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_is_sound [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop [definition, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_end [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_is_complete [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_is_sound [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_unfold [lemma, in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_nil [lemma, in ac_matching.matching_algo]
S.Import.matching [definition, in ac_matching.matching_algo]
S.Import.matching_problem [inductive, in ac_matching.matching]
S.Import.mem [definition, in list_extensions.list_permut]
S.Import.occurs_in_pb [definition, in ac_matching.matching]
S.Import.occurs_in_term [definition, in ac_matching.matching]
S.Import.occurs_in_term_list [definition, in ac_matching.matching]
S.Import.o_lpb [definition, in ac_matching.matching_algo]
S.Import.partly_solved_term [inductive, in ac_matching.matching]
S.Import.pb_weight [definition, in ac_matching.matching_well_founded]
S.Import.solve [definition, in ac_matching.matching]
S.Import.TO.A [definition, in ac_matching.ac]
S.Import.TO.Import.ac [definition, in ac_matching.ac]
S.Import.TO.Import.ac_one_step_at_top [inductive, in ac_matching.ac]
S.Import.TO.Import.ac_size [definition, in ac_matching.ac]
S.Import.TO.Import.apply_cf_subst [definition, in ac_matching.ac]
S.Import.TO.Import.a_axiom [constructor, in ac_matching.ac]
S.Import.TO.Import.build [definition, in ac_matching.ac]
S.Import.TO.Import.canonical_form [definition, in ac_matching.ac]
S.Import.TO.Import.c_axiom [constructor, in ac_matching.ac]
S.Import.TO.Import.flatten [definition, in ac_matching.ac]
S.Import.TO.Import.Make.A [definition, in ac_matching.ac]
S.Import.TO.Import.Make.A [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac_one_step_at_top [inductive, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac_one_step_at_top_top_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac_one_step_top_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac_top_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.a_axiom [constructor, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.comm [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.c_axiom [constructor, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_cf_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_at_top_cf_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_at_top_size_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_cf_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_size_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size_ge_one [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size_unfold [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.apply_cf_subst [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.apply_cf_subst_is_sound [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.build [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.build_eq_Term [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.canonical_form [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_app [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_apply_cf_subst [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_build [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_build_cons [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_build_inside [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_cf [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_cf_cf [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.is_subst_canonical_form [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.is_subst_cf_is_subst_cf [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.length_flatten [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.length_flatten_bis [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.length_flatten_ter [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.list_permut_flatten [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.size_size [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.size_size_aux2 [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.size_size_aux3 [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.sym_refl_ac_one_step_at_top_cf_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.sym_refl_ac_one_step_at_top_size_eq [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_alien [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_apply_subst [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_build [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_build_cons [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_build_inside [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_fold [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_is_well_formed_cf [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_is_well_formed_cf_conv [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_length [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_sorted [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subst [definition, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subst_is_well_formed_cf_subst [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subst_is_well_formed_cf_subst_aux [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subterms [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_unfold [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.l_assoc [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.no_need_of_instance [lemma, in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.r_assoc [lemma, in ac_matching.ac]
S.Import.TO.Import.well_formed_cf [definition, in ac_matching.ac]
S.Import.TO.Import.well_formed_cf_subst [definition, in ac_matching.ac]
S.Import.W [constructor, in ac_matching.matching_algo]
S.Import.well_formed_matching_problem [inductive, in ac_matching.matching_algo]
S.Import.well_formed_pb [definition, in ac_matching.matching]
S.Import.well_sorted_partly_solved_part [definition, in ac_matching.matching]
S.Import.wfpb_weight [definition, in ac_matching.matching_algo]
S.Import.wf_solve [definition, in ac_matching.matching_algo]
S.Import.wf_solve_loop [definition, in ac_matching.matching_algo]


T

T [module, in term_algebra.equational_theory]
tail_in [lemma, in examples.cime_trace.ring_extention]
tail_prop [lemma, in list_extensions.more_list]
tail_set [lemma, in list_extensions.more_list]
Term [module, in term_algebra.term]
term [library]
terminaison [library]
termineR2 [lemma, in examples.cime_trace.rewriting]
termineR2aux [lemma, in examples.cime_trace.rewriting]
termine_gt_compat [lemma, in examples.cime_trace.rewriting]
termine_incl [lemma, in examples.cime_trace.rewriting]
term_acc_subst [axiom, in term_algebra.equational_theory]
Term_equiv_dec [module, in term_orderings.rpo]
Term_eq_dec [module, in unification.free_unif]
term_o [library]
Term_ordering [module, in term_orderings.term_o]
Term_ordering.Import.OF.A [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.A [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.A [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.A [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.A [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.A [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.A [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.eq_dec [lemma, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_anti_sym [lemma, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_dec [lemma, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_proof [lemma, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_term_list [definition, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_term_list_is_o_term_list [lemma, in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_total [lemma, in term_orderings.term_o]
Term_ordering.Import.OF.OX.o [definition, in term_orderings.term_o]
term_rec2 [axiom, in term_algebra.term]
term_rec3 [axiom, in term_algebra.term]
term_rec4 [axiom, in term_algebra.term]
term_rec7 [axiom, in term_algebra.term]
term_rec8 [axiom, in term_algebra.term]
term_term_dec [axiom, in term_algebra.term]
th_refl [axiom, in term_algebra.equational_theory]
th_sym [axiom, in term_algebra.equational_theory]
TO [module, in ac_matching.ac]
trans_clos [inductive, in basis.closure]
trans_clos_is_clos [lemma, in basis.closure]
trans_clos_is_trans [lemma, in basis.closure]
trans_inversion [lemma, in basis.closure]
t_clos [constructor, in basis.closure]
t_step [constructor, in basis.closure]
t_trans [constructor, in basis.closure]


U

Uncomparable [constructor, in basis.ordered_set]
unification [library]
unit_theory [axiom, in unification.unification]
unit_theory_is_coherent [axiom, in unification.unification]


V

var_acc [axiom, in term_algebra.equational_theory]
var_in_subterm [axiom, in term_algebra.term]
var_in_subterm2 [axiom, in term_algebra.term]
var_list_unfold [axiom, in term_algebra.term]
VSet [module, in unification.free_unif]
VSet [module, in term_algebra.term]
VSet [module, in term_algebra.term]
VT [module, in term_algebra.equational_theory]
VT [module, in term_algebra.equational_theory]


W

well_formed_apply_subst [axiom, in term_algebra.term]
well_formed_cf_alien [axiom, in ac_matching.ac]
well_formed_cf_apply_subst [axiom, in ac_matching.ac]
well_formed_cf_build [axiom, in ac_matching.ac]
well_formed_cf_build_cons [axiom, in ac_matching.ac]
well_formed_cf_build_inside [axiom, in ac_matching.ac]
well_formed_cf_length [axiom, in ac_matching.ac]
well_formed_cf_sorted [axiom, in ac_matching.ac]
well_formed_cf_subterms [axiom, in ac_matching.ac]
well_formed_cf_unfold [axiom, in ac_matching.ac]
well_formed_fold [axiom, in term_algebra.term]
well_formed_init_pb [axiom, in ac_matching.matching_algo]
well_formed_solve [axiom, in ac_matching.matching_well_formed]
well_formed_unfold [axiom, in term_algebra.term]
well_founded_o_lpb [axiom, in ac_matching.matching_algo]
well_founded_solve [axiom, in ac_matching.matching_well_founded]
wf_length [lemma, in list_extensions.more_list]
wf_lex [lemma, in term_orderings.rpo]
wf_rpo [axiom, in term_orderings.rpo]
wf_trans [lemma, in basis.closure]



Axiom Index

A

A [in term_orderings.rpo]
A [in basis.decidable_set]
A [in basis.ordered_set]
A [in basis.decidable_set]
acc_one_step [in term_algebra.equational_theory]
acc_one_step_list [in term_algebra.equational_theory]
acc_subterms [in term_algebra.equational_theory]
acc_subterms_1 [in term_algebra.equational_theory]
acc_subterms_3 [in term_algebra.equational_theory]
acc_with_subterm [in term_algebra.equational_theory]
acc_with_subterm_subterms [in term_algebra.equational_theory]
ac_cf_eq [in ac_matching.ac]
ac_size_eq [in ac_matching.ac]
ac_size_ge_one [in ac_matching.ac]
ac_size_unfold [in ac_matching.ac]
ac_syntactic [in list_extensions.list_permut]
ac_top_eq [in ac_matching.ac]
add_new_var_to_rough_sol [in ac_matching.matching]
apply_subst_const [in term_algebra.term]
arity [in term_algebra.term]


B

build_eq_Term [in ac_matching.ac]


C

cardinal_subset [in list_extensions.list_set]
cf_eq_ac [in ac_matching.cf_eq_ac]
comm [in ac_matching.ac]
compute_red [in term_algebra.equational_theory]
compute_red_is_correct [in term_algebra.equational_theory]
cons_permut_mem [in list_extensions.list_permut]
context_cons [in term_algebra.equational_theory]
context_in [in term_algebra.equational_theory]
context_trans_clos_multiset_extension_step_app1 [in list_extensions.dickson]


D

dickson [in list_extensions.dickson]
dickson_strong [in list_extensions.dickson]
diff_mem_remove [in list_extensions.list_permut]


E

empty_subst_is_id [in term_algebra.term]
empty_subst_is_id_list [in term_algebra.term]
equiv_add_context [in term_orderings.rpo]
equiv_dec [in term_orderings.rpo]
equiv_equiv [in term_orderings.rpo]
equiv_rpo_equiv_1 [in term_orderings.rpo]
equiv_rpo_equiv_2 [in term_orderings.rpo]
equiv_rpo_equiv_3 [in term_orderings.rpo]
equiv_rpo_equiv_4 [in term_orderings.rpo]
equiv_subst [in term_orderings.rpo]
eq_A [in basis.ordered_set]
eq_A [in basis.decidable_set]
eq_dec [in term_orderings.term_o]
eq_dec [in basis.ordered_set]
eq_dec [in basis.decidable_set]
eq_dec [in basis.decidable_set]
eq_dec [in basis.ordered_set]
eq_proof [in basis.decidable_set]
eq_proof [in basis.ordered_set]
eq_term_dec [in term_algebra.term]
exists_subterm_is_a_pos [in term_algebra.term]


F

FB_nf_dec [in term_algebra.equational_theory]
flatten_app [in ac_matching.ac]
flatten_apply_cf_subst [in ac_matching.ac]
flatten_build [in ac_matching.ac]
flatten_build_cons [in ac_matching.ac]
flatten_build_inside [in ac_matching.ac]
flatten_cf [in ac_matching.ac]
flatten_cf_cf [in ac_matching.ac]
fresh_var [in ac_matching.matching]
fresh_var [in ac_matching.matching]
fresh_var_spec [in ac_matching.matching]
fresh_var_spec [in ac_matching.matching]
F_wf_solve_dec1 [in ac_matching.matching_algo]
F_wf_solve_dec2 [in ac_matching.matching_algo]


G

general_context [in term_algebra.equational_theory]
general_context_aux [in term_algebra.equational_theory]


I

in_impl_mem [in list_extensions.list_permut]
in_quick_in [in list_extensions.list_sort]
in_remove_list [in list_extensions.list_sort]
is_a_pos_exists_subterm [in term_algebra.term]


L

length_flatten_bis [in ac_matching.ac]
length_flatten_ter [in ac_matching.ac]
length_quicksort [in list_extensions.list_sort]
list_permut_acc [in list_extensions.dickson]
list_permut_app_app [in list_extensions.list_permut]
list_permut_flatten [in ac_matching.ac]
list_permut_multiset_extension_step_1 [in list_extensions.dickson]
list_permut_multiset_extension_step_2 [in list_extensions.dickson]
list_permut_occurs_in_term_list [in ac_matching.matching]
l_assoc [in ac_matching.ac]


M

matching [in term_algebra.term]
matching_complete [in term_algebra.term]
matching_correct [in term_algebra.term]
matching_is_complete [in ac_matching.matching_algo]
matching_is_sound [in ac_matching.matching_algo]
matching_unfold2 [in term_algebra.term]
mem_dec [in list_extensions.list_set]
mem_dec [in list_extensions.list_permut]
mem_insert [in list_extensions.list_permut]
mem_or_app [in list_extensions.list_permut]
mem_permut_mem [in list_extensions.list_permut]
mem_split_set [in list_extensions.list_permut]
multiset_closure [in list_extensions.dickson]


N

nf_one_step_subterm [in term_algebra.equational_theory]
nf_rwr_subterm [in term_algebra.equational_theory]
no_need_of_instance_is_modular [in term_algebra.equational_theory]


O

o [in basis.ordered_set]
o [in basis.ordered_set]
one_step_apply_subst [in term_algebra.equational_theory]
one_step_at_pos [in term_algebra.equational_theory]
one_step_context_in [in term_algebra.equational_theory]
one_step_in_list [in term_algebra.equational_theory]
one_step_list_length_eq [in term_algebra.equational_theory]
one_step_list_rwr_list [in term_algebra.equational_theory]
o_compat [in basis.ordered_set]
o_dec [in basis.ordered_set]
o_dec [in term_orderings.term_o]
o_dec [in basis.ordered_set]
o_proof [in basis.ordered_set]
o_proof [in term_orderings.term_o]
o_proof [in basis.ordered_set]
o_total [in basis.ordered_set]
o_total [in term_orderings.term_o]
o_total [in basis.ordered_set]


P

permut_add_inside [in list_extensions.list_permut]
permut_app1 [in list_extensions.list_permut]
permut_app2 [in list_extensions.list_permut]
permut_cons [in list_extensions.list_permut]
permut_cons_inside [in list_extensions.list_permut]
permut_dec [in list_extensions.list_permut]
permut_refl [in list_extensions.list_permut]
permut_sym [in list_extensions.list_permut]
permut_trans [in list_extensions.list_permut]
prec [in term_orderings.rpo]
prec_antisym [in term_orderings.rpo]
prec_dec [in term_orderings.rpo]
prec_transitive [in term_orderings.rpo]


Q

quicksort [in list_extensions.list_sort]
quicksort_equation [in list_extensions.list_sort]
quick_permut [in list_extensions.list_sort]
quick_permut_bis [in list_extensions.list_sort]
quick_sorted [in list_extensions.list_sort]


R

remove_equiv_is_sound [in list_extensions.list_permut]
remove_garbage_subst [in term_algebra.term]
remove_is_sound [in list_extensions.list_permut]
replace_at_pos_in_replace_at_pos [in term_algebra.term]
replace_at_pos_is_replace_at_pos1 [in term_algebra.term]
replace_at_pos_is_replace_at_pos2 [in term_algebra.term]
replace_at_pos_list_replace_at_pos_in_subterm [in term_algebra.term]
replace_at_pos_replace_at_pos [in term_algebra.term]
replace_at_pos_unfold [in term_algebra.term]
restrict_domain_ok [in term_algebra.term]
restrict_domain_ok2 [in term_algebra.term]
rpo_add_context [in term_orderings.rpo]
rpo_closure [in term_orderings.rpo]
rpo_dec [in term_orderings.rpo]
rpo_subst [in term_orderings.rpo]
rpo_trans [in term_orderings.rpo]
rwr_apply_subst [in term_algebra.equational_theory]
rwr_at_pos [in term_algebra.equational_theory]
rwr_closure [in term_algebra.equational_theory]
rwr_closure_one_step [in term_algebra.equational_theory]
rwr_inv [in term_algebra.equational_theory]
rwr_list_is_trans [in term_algebra.equational_theory]
rwr_list_length_eq [in term_algebra.equational_theory]
rwr_list_trans_clos_one_step_list [in term_algebra.equational_theory]
rwr_or_eq [in term_algebra.equational_theory]
rwr_or_eq_subst [in term_algebra.equational_theory]
rwr_R1_included_in_R2 [in term_algebra.equational_theory]
R1_included_in_R2_axiom [in term_algebra.equational_theory]
R1_included_in_R2_one_step [in term_algebra.equational_theory]
R1_included_in_R2_rwr [in term_algebra.equational_theory]
R1_included_in_R2_rwr_list [in term_algebra.equational_theory]
r_assoc [in ac_matching.ac]
R_axiom [in term_algebra.equational_theory]
R_one_step [in term_algebra.equational_theory]
R_rwr [in term_algebra.equational_theory]


S

size_direct_subterm [in term_algebra.term]
size_ge_one [in term_algebra.term]
size_size [in ac_matching.ac]
size_size_aux3 [in ac_matching.ac]
size_subterm_at_pos [in term_algebra.term]
size_unfold [in term_algebra.term]
solve_is_complete [in ac_matching.matching_complete]
solve_is_sound [in ac_matching.matching_sound]
sorted_tl_sorted [in list_extensions.list_sort]
sort_is_unique [in list_extensions.list_sort]
split_rel [in term_algebra.equational_theory]
status [in term_orderings.rpo]
subst_comp_is_subst_comp [in term_algebra.term]
subst_comp_is_subst_comp_aux1 [in term_algebra.term]
subst_eq_vars [in term_algebra.term]
subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [in term_algebra.term]
subterm_at_pos_dec [in term_algebra.term]
subterm_in_instantiated_term [in term_algebra.term]
subterm_in_subterm [in term_algebra.term]
subterm_in_subterm2 [in term_algebra.term]
subterm_subterm [in term_algebra.term]
symb_in_direct_subterm [in term_algebra.term]
symb_in_subterm [in term_algebra.term]
symb_in_term_list_app [in term_algebra.term]
symb_in_term_unfold [in term_algebra.term]


T

term_acc_subst [in term_algebra.equational_theory]
term_rec2 [in term_algebra.term]
term_rec3 [in term_algebra.term]
term_rec4 [in term_algebra.term]
term_rec7 [in term_algebra.term]
term_rec8 [in term_algebra.term]
term_term_dec [in term_algebra.term]
th_refl [in term_algebra.equational_theory]
th_sym [in term_algebra.equational_theory]


U

unit_theory [in unification.unification]
unit_theory_is_coherent [in unification.unification]


V

var_acc [in term_algebra.equational_theory]
var_in_subterm [in term_algebra.term]
var_in_subterm2 [in term_algebra.term]
var_list_unfold [in term_algebra.term]


W

well_formed_apply_subst [in term_algebra.term]
well_formed_cf_alien [in ac_matching.ac]
well_formed_cf_apply_subst [in ac_matching.ac]
well_formed_cf_build [in ac_matching.ac]
well_formed_cf_build_cons [in ac_matching.ac]
well_formed_cf_build_inside [in ac_matching.ac]
well_formed_cf_length [in ac_matching.ac]
well_formed_cf_sorted [in ac_matching.ac]
well_formed_cf_subterms [in ac_matching.ac]
well_formed_cf_unfold [in ac_matching.ac]
well_formed_fold [in term_algebra.term]
well_formed_init_pb [in ac_matching.matching_algo]
well_formed_solve [in ac_matching.matching_well_formed]
well_formed_unfold [in term_algebra.term]
well_founded_o_lpb [in ac_matching.matching_algo]
well_founded_solve [in ac_matching.matching_well_founded]
wf_rpo [in term_orderings.rpo]



Lemma Index

A

acc_and [in basis.closure]
acc_lex [in term_orderings.rpo]
acc_nf [in basis.closure]
acc_trans [in basis.closure]
ACU.F.Make.Import.acu_is_ac_on_unit_nf [in unification.unification]
ACU.F.Make.Import.ac_const [in unification.unification]
ACU.F.Make.Import.clash [in unification.unification]
ACU.F.Make.Import.mutate_c [in unification.unification]
ACU.F.Make.Import.mutate_cu [in unification.unification]
ACU.F.Make.Import.mutate_cu_sound [in unification.unification]
ACU.F.Make.Import.mutate_c_sound [in unification.unification]
ACU.F.Make.Import.mutate_free [in unification.unification]
ACU.F.Make.Import.mutate_free_lu [in unification.unification]
ACU.F.Make.Import.mutate_free_lu_sound [in unification.unification]
ACU.F.Make.Import.mutate_free_ru [in unification.unification]
ACU.F.Make.Import.mutate_free_ru_sound [in unification.unification]
ACU.F.Make.Import.mutate_free_sound [in unification.unification]
ACU.F.Make.Import.mutate_free_u [in unification.unification]
ACU.F.Make.Import.mutate_free_u_sound [in unification.unification]
ACU.F.Make.Import.mutate_lu [in unification.unification]
ACU.F.Make.Import.mutate_lu_lu [in unification.unification]
ACU.F.Make.Import.mutate_lu_lu_sound [in unification.unification]
ACU.F.Make.Import.mutate_lu_ru [in unification.unification]
ACU.F.Make.Import.mutate_lu_ru_sound [in unification.unification]
ACU.F.Make.Import.mutate_lu_sound [in unification.unification]
ACU.F.Make.Import.mutate_lu_u [in unification.unification]
ACU.F.Make.Import.mutate_lu_u_sound [in unification.unification]
ACU.F.Make.Import.mutate_ru [in unification.unification]
ACU.F.Make.Import.mutate_ru_ru [in unification.unification]
ACU.F.Make.Import.mutate_ru_ru_sound [in unification.unification]
ACU.F.Make.Import.mutate_ru_sound [in unification.unification]
ACU.F.Make.Import.mutate_ru_u [in unification.unification]
ACU.F.Make.Import.mutate_ru_u_sound [in unification.unification]
ACU.F.Make.Import.mutate_u [in unification.unification]
ACU.F.Make.Import.mutate_u_sound [in unification.unification]
ACU.F.Make.Import.mutate_u_u [in unification.unification]
ACU.F.Make.Import.mutate_u_u_sound [in unification.unification]
ACU.F.Make.Import.no_need_of_instance [in unification.unification]
ACU.F.Make.Import.unit_for_AC [in unification.unification]
ACU.F.Make.Import.unit_for_C [in unification.unification]
ACU.F.Make.Import.unit_nf_is_idempotent [in unification.unification]
ACU.F.Make.Import.unit_nf_is_sound [in unification.unification]
ACU.F.Make.Import.unit_nf_nothing [in unification.unification]
ACU.F.Make.Import.unit_th_is_unit_nf_eq [in unification.unification]
ACU.F.Make.Import.well_formed_unit_nf [in unification.unification]
adequacy [in list_extensions.math_permut]
all_le_def [in examples.cime_trace.ring_extention]
all_mem_pos_def [in examples.cime_trace.ring_extention]


C

Convert.eq_dec [in basis.decidable_set]
Convert.eq_proof [in basis.decidable_set]
cycle_not_acc [in basis.closure]


D

dec_nf [in basis.closure]
diff_in_remove [in list_extensions.more_list]
D.Import.Import.Make.Import.Import.Import.appendn_app [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.consn_app [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_multiset_extension_step_app1 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_multiset_extension_step_app2 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_multiset_extension_step_cons [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_trans_clos_multiset_extension_step_app1 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.context_trans_clos_multiset_extension_step_cons [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_aux1 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_aux2 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_aux3 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.dickson_strong [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.greater_case [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.in_appendn [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.eq_dec [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.eq_proof [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_acc [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_multiset_extension_step_1 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_multiset_extension_step_2 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_trans_clos_multiset_extension_step_1 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.list_permut_trans_clos_multiset_extension_step_2 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mem_consn [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure_aux [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure_aux2 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.multiset_closure_aux3 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_complete [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_complete_equiv [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_complete_greater [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult_is_sound [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.nil_is_the_smallest [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.permut_appendn [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.permut_consn [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.remove_context_multiset_extension_step_app1 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.remove_context_trans_clos_multiset_extension_step_app1 [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.R_dec_sym [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.R_or_eq_dec_is_sound [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.two_cases [in list_extensions.dickson]


E

EqTh.T.VT.Make.acc_nf_subst [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_one_step [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_one_step_list [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_rwr_subst [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_subterms [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_subterms_1 [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_subterms_3 [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_with_subterm [in term_algebra.equational_theory]
EqTh.T.VT.Make.acc_with_subterm_subterms [in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_head_red_is_correct [in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_red_is_correct [in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_red_unfold [in term_algebra.equational_theory]
EqTh.T.VT.Make.context_cons [in term_algebra.equational_theory]
EqTh.T.VT.Make.context_in [in term_algebra.equational_theory]
EqTh.T.VT.Make.FB_nf_dec [in term_algebra.equational_theory]
EqTh.T.VT.Make.general_context [in term_algebra.equational_theory]
EqTh.T.VT.Make.general_context_aux [in term_algebra.equational_theory]
EqTh.T.VT.Make.nf_one_step_subterm [in term_algebra.equational_theory]
EqTh.T.VT.Make.nf_rwr_subterm [in term_algebra.equational_theory]
EqTh.T.VT.Make.no_need_of_instance_is_modular [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_apply_subst [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_at_pos [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_context_in [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_in_list [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_list_length_eq [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_list_rwr_list [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_apply_subst [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_at_pos [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_closure [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_closure_one_step [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_inv [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list_is_trans [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list_length_eq [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list_trans_clos_one_step_list [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_or_eq [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_or_eq_subst [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_R1_included_in_R2 [in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_axiom [in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_one_step [in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_rwr [in term_algebra.equational_theory]
EqTh.T.VT.Make.R1_included_in_R2_rwr_list [in term_algebra.equational_theory]
EqTh.T.VT.Make.R_axiom [in term_algebra.equational_theory]
EqTh.T.VT.Make.R_one_step [in term_algebra.equational_theory]
EqTh.T.VT.Make.R_rwr [in term_algebra.equational_theory]
EqTh.T.VT.Make.split_rel [in term_algebra.equational_theory]
EqTh.T.VT.Make.term_acc_subst [in term_algebra.equational_theory]
EqTh.T.VT.Make.th_refl [in term_algebra.equational_theory]
EqTh.T.VT.Make.th_sym [in term_algebra.equational_theory]
EqTh.T.VT.Make.var_acc [in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.eq_dec [in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.eq_proof [in term_algebra.equational_theory]
EqTh.T.VT.Make.wf_size [in term_algebra.equational_theory]
equiv_in_list [in list_extensions.equiv_list]
equiv_in_list_2 [in list_extensions.equiv_list]
equiv_swap [in list_extensions.equiv_list]
exists_dec [in list_extensions.list_permut]
exists_map12_without_repetition [in list_extensions.more_list]
exists_map_without_repetition [in list_extensions.more_list]


F

find_app [in list_extensions.more_list]
find_diff [in list_extensions.more_list]
find_map [in list_extensions.more_list]
find_mem [in list_extensions.more_list]
find_not_found [in list_extensions.more_list]
find_not_mem [in list_extensions.more_list]
fold_left_in_acc [in list_extensions.more_list]
fold_left_in_acc_split [in list_extensions.more_list]


I

included_list_sound [in list_extensions.more_list]
incl_trans [in basis.closure]
incl_trans2 [in basis.closure]
insert_1 [in list_extensions.more_list]
insert_2 [in list_extensions.more_list]
inv_trans [in basis.closure]
In_dec_app [in list_extensions.more_list]
in_insert [in list_extensions.more_list]
in_in_split_set [in list_extensions.more_list]
In_mem [in list_extensions.more_list]
in_permut_in [in list_extensions.list_permut]
in_remove [in list_extensions.more_list]
in_split_set [in list_extensions.more_list]


J

jump_combine [in examples.cime_trace.ring_extention]
jump_in [in examples.cime_trace.ring_extention]
jump_length [in examples.cime_trace.ring_extention]
jump_nil [in examples.cime_trace.ring_extention]


L

length_add [in list_extensions.more_list]
lex_trans [in term_orderings.rpo]
list_exists_app [in list_extensions.more_list]
list_exists_impl [in list_extensions.more_list]
list_exists_is_sound [in list_extensions.more_list]
list_exists_option_is_complete_false [in list_extensions.more_list]
list_exists_option_is_complete_none [in list_extensions.more_list]
list_exists_option_is_complete_true [in list_extensions.more_list]
list_exists_option_is_sound [in list_extensions.more_list]
list_exists_rest_is_sound [in list_extensions.more_list]
list_forall2_is_sound [in list_extensions.more_list]
list_forall_app [in list_extensions.more_list]
list_forall_impl [in list_extensions.more_list]
list_forall_is_sound [in list_extensions.more_list]
list_forall_option_is_complete_false [in list_extensions.more_list]
list_forall_option_is_complete_true [in list_extensions.more_list]
list_forall_option_is_sound [in list_extensions.more_list]
list_size_app [in list_extensions.more_list]
list_size_fold [in list_extensions.more_list]
list_size_size_eq [in list_extensions.more_list]
list_size_tl_compat [in list_extensions.more_list]


M

MakeDP.acc_interp_acc [in term_orderings.dp]
MakeDP.acc_interp_dom [in term_orderings.dp]
MakeDP.acc_one_step_acc_dp [in term_orderings.dp]
MakeDP.acc_one_step_acc_mdp [in term_orderings.dp]
MakeDP.acc_rdp_acc_rmdp [in term_orderings.dp]
MakeDP.acc_subterms_pi [in term_orderings.dp]
MakeDP.Case12 [in term_orderings.dp]
MakeDP.Case3 [in term_orderings.dp]
MakeDP.constructor_defined_dec [in term_orderings.dp]
MakeDP.defined_dec [in term_orderings.dp]
MakeDP.defined_list_complete [in term_orderings.dp]
MakeDP.defined_list_sound [in term_orderings.dp]
MakeDP.defined_subterms_accumulates [in term_orderings.dp]
MakeDP.defined_subterms_complete [in term_orderings.dp]
MakeDP.def_dec12 [in term_orderings.dp]
MakeDP.def_dec123' [in term_orderings.dp]
MakeDP.def_dec132' [in term_orderings.dp]
MakeDP.def_dec2' [in term_orderings.dp]
MakeDP.def_dec3' [in term_orderings.dp]
MakeDP.def_dec_rules [in term_orderings.dp]
MakeDP.dp_criterion [in term_orderings.dp]
MakeDP.dp_criterion_aux [in term_orderings.dp]
MakeDP.dp_criterion_lift [in term_orderings.dp]
MakeDP.dp_incl [in term_orderings.dp]
MakeDP.dp_list_complete [in term_orderings.dp]
MakeDP.dp_mdp [in term_orderings.dp]
MakeDP.dp_necessary [in term_orderings.dp]
MakeDP.dp_step_incl [in term_orderings.dp]
MakeDP.Dummy [in term_orderings.dp]
MakeDP.Empty_R_reg [in term_orderings.dp]
MakeDP.Equiv_comb [in term_orderings.dp]
MakeDP.Equiv_empty [in term_orderings.dp]
MakeDP.FB12 [in term_orderings.dp]
MakeDP.FB_Pi [in term_orderings.dp]
MakeDP.Incomp [in term_orderings.dp]
MakeDP.Incomp12 [in term_orderings.dp]
MakeDP.Incomp123' [in term_orderings.dp]
MakeDP.Incomp13 [in term_orderings.dp]
MakeDP.Incomp23 [in term_orderings.dp]
MakeDP.interp_defined [in term_orderings.dp]
MakeDP.interp_dom_R1 [in term_orderings.dp]
MakeDP.interp_dom_R1_R2 [in term_orderings.dp]
MakeDP.interp_dom_R1_R2_rwr [in term_orderings.dp]
MakeDP.interp_dom_R2 [in term_orderings.dp]
MakeDP.interp_dom_subst [in term_orderings.dp]
MakeDP.interp_dom_subterm [in term_orderings.dp]
MakeDP.interp_unicity [in term_orderings.dp]
MakeDP.interp_well_defined [in term_orderings.dp]
MakeDP.interp_well_defined_1 [in term_orderings.dp]
MakeDP.interp_well_defined_2 [in term_orderings.dp]
MakeDP.interp_well_defined_3 [in term_orderings.dp]
MakeDP.list_rules_empty [in term_orderings.dp]
MakeDP.mark_term_bij [in term_orderings.dp]
MakeDP.mdp_criterion [in term_orderings.dp]
MakeDP.mdp_criterion_strong [in term_orderings.dp]
MakeDP.mdp_dp [in term_orderings.dp]
MakeDP.mdp_necessary [in term_orderings.dp]
MakeDP.modular_termination [in term_orderings.dp]
MakeDP.modular_termination_hierarch_lift [in term_orderings.dp]
MakeDP.modular_termination_indep_lift [in term_orderings.dp]
MakeDP.modular_termination_indep_list_lift [in term_orderings.dp]
MakeDP.modular_termination_lift [in term_orderings.dp]
MakeDP.modular_var [in term_orderings.dp]
MakeDP.module123' [in term_orderings.dp]
MakeDP.module132' [in term_orderings.dp]
MakeDP.pi_subterm [in term_orderings.dp]
MakeDP.P_comb [in term_orderings.dp]
MakeDP.P_empty [in term_orderings.dp]
MakeDP.rdp_step_incl [in term_orderings.dp]
MakeDP.rdp_step_rmdp_step [in term_orderings.dp]
MakeDP.recover_red [in term_orderings.dp]
MakeDP.rmdp_step_rdp_step [in term_orderings.dp]
MakeDP.R123_reg' [in term_orderings.dp]
MakeDP.R123_var' [in term_orderings.dp]
MakeDP.R12_reg [in term_orderings.dp]
MakeDP.R12_var [in term_orderings.dp]
MakeDP.R12_var' [in term_orderings.dp]
MakeDP.R132_reg' [in term_orderings.dp]
MakeDP.R132_var' [in term_orderings.dp]
MakeDP.R13_reg [in term_orderings.dp]
MakeDP.R13_var [in term_orderings.dp]
MakeDP.R1_at_top [in term_orderings.dp]
MakeDP.R1_at_top_aux_1 [in term_orderings.dp]
MakeDP.R1_at_top_aux_2 [in term_orderings.dp]
MakeDP.R1_at_top_dp [in term_orderings.dp]
MakeDP.R1_case [in term_orderings.dp]
MakeDP.R1_R2_case [in term_orderings.dp]
MakeDP.R1_R2_case_one_step [in term_orderings.dp]
MakeDP.R2_case [in term_orderings.dp]
MakeDP.R2_var' [in term_orderings.dp]
MakeDP.R3_var' [in term_orderings.dp]
MakeDP.R_reg_comb [in term_orderings.dp]
MakeDP.R_reg_empty [in term_orderings.dp]
MakeDP.R_var_comb [in term_orderings.dp]
MakeDP.R_var_empty [in term_orderings.dp]
MakeDP.split_dp [in term_orderings.dp]
MakeDP.split_dp_top [in term_orderings.dp]
MakeDP.split_rdp_step [in term_orderings.dp]
MakeDP.split_rdp_step_top [in term_orderings.dp]
MakeDP.technical_lemma [in term_orderings.dp]
MakeDP.technical_lemma_1 [in term_orderings.dp]
MakeDP.wf_interp_acc [in term_orderings.dp]
MakeDP.W12' [in term_orderings.dp]
MakeDP.x_to_x2_commutes_mark [in term_orderings.dp]
Make.acc_P_list [in term_algebra.rwr_strategies]
Make.Acc_R_list [in examples.cime_trace.equational_extension]
Make.existsb_app [in examples.cime_trace.equational_extension]
Make.existsb_term_eq_In [in examples.cime_trace.equational_extension]
Make.Import.combine_cons [in unification.free_unif]
Make.Import.combine_nil [in unification.free_unif]
Make.Import.combine_proof [in unification.free_unif]
Make.Import.Import.acc_inner_acc [in term_orderings.inner_dp]
Make.Import.Import.acc_psi_acc [in term_orderings.inner_dp]
Make.Import.Import.acc_psi_acc_ooo [in term_orderings.inner_dp]
Make.Import.Import.idp_criterion [in term_orderings.inner_dp]
Make.Import.Import.idp_criterion_aux [in term_orderings.inner_dp]
Make.Import.Import.map_psi [in term_orderings.inner_dp]
Make.Import.Import.nf_var [in term_orderings.inner_dp]
Make.Import.Import.psi_char [in term_orderings.inner_dp]
Make.Import.Import.Psi_def [in term_orderings.inner_dp]
Make.Import.Import.psi_inner_axiom [in term_orderings.inner_dp]
Make.Import.Import.Psi_in_context_bis [in term_orderings.inner_dp]
Make.Import.Import.psi_nf [in term_orderings.inner_dp]
Make.Import.Import.psi_not_inner [in term_orderings.inner_dp]
Make.Import.Import.Psi_not_nf [in term_orderings.inner_dp]
Make.Import.Import.psi_not_nf [in term_orderings.inner_dp]
Make.Import.Import.Psi_not_refl [in term_orderings.inner_dp]
Make.Import.Import.Psi_psi [in term_orderings.inner_dp]
Make.Import.Import.Psi_rwr [in term_orderings.inner_dp]
Make.Import.Import.Psi_sim_inner [in term_orderings.inner_dp]
Make.Import.Import.Psi_sim_inner_at_top [in term_orderings.inner_dp]
Make.Import.Import.Psi_sim_one_step [in term_orderings.inner_dp]
Make.Import.Import.psi_subst [in term_orderings.inner_dp]
Make.Import.Import.psi_two_cases [in term_orderings.inner_dp]
Make.Import.Import.Psi_unique [in term_orderings.inner_dp]
Make.Import.Import.Rreg' [in term_orderings.inner_dp]
Make.Import.Import.Rvar' [in term_orderings.inner_dp]
Make.Import.Import.wf_inner_no_wf [in term_orderings.inner_dp]
Make.Import.Import.wf_inner_wf [in term_orderings.inner_dp]
Make.Import.VSet.apply_subst_outside_dom [in unification.free_unif]
Make.Import.VSet.coalesce1_decreases [in unification.free_unif]
Make.Import.VSet.coalesce2_decreases [in unification.free_unif]
Make.Import.VSet.decompose_is_complete [in unification.free_unif]
Make.Import.VSet.decompose_is_sound [in unification.free_unif]
Make.Import.VSet.decompose_nf [in unification.free_unif]
Make.Import.VSet.decompose_unfold [in unification.free_unif]
Make.Import.VSet.decomposition_decreases [in unification.free_unif]
Make.Import.VSet.decomposition_e_unfold_normal [in unification.free_unif]
Make.Import.VSet.decomposition_e_unfold_not_app [in unification.free_unif]
Make.Import.VSet.decomposition_e_unfold_no_sol [in unification.free_unif]
Make.Import.VSet.decomposition_step_decreases [in unification.free_unif]
Make.Import.VSet.decomposition_step_decreases_e [in unification.free_unif]
Make.Import.VSet.decomposition_step_is_complete [in unification.free_unif]
Make.Import.VSet.decomposition_step_is_sound [in unification.free_unif]
Make.Import.VSet.domain_of_subst_map_subst [in unification.free_unif]
Make.Import.VSet.find_map_subst [in unification.free_unif]
Make.Import.VSet.inv_solved_part [in unification.free_unif]
Make.Import.VSet.inv_solved_part_e [in unification.free_unif]
Make.Import.VSet.inv_solved_part_init [in unification.free_unif]
Make.Import.VSet.is_a_not_solved_var_dec [in unification.free_unif]
Make.Import.VSet.is_a_solved_var_dec [in unification.free_unif]
Make.Import.VSet.lex_le_lt [in unification.free_unif]
Make.Import.VSet.lex_le_meq_lt [in unification.free_unif]
Make.Import.VSet.lex_lt [in unification.free_unif]
Make.Import.VSet.list_size_mul_app [in unification.free_unif]
Make.Import.VSet.measure_for_unif_pb_swapp_eq [in unification.free_unif]
Make.Import.VSet.merge1_decreases [in unification.free_unif]
Make.Import.VSet.merge2_decreases [in unification.free_unif]
Make.Import.VSet.move_eq_decreases [in unification.free_unif]
Make.Import.VSet.not_solved_var [in unification.free_unif]
Make.Import.VSet.occ_var_is_a_subterm_at_pos [in unification.free_unif]
Make.Import.VSet.remove_trivial_eq_decreases [in unification.free_unif]
Make.Import.VSet.solved_var_inc_list [in unification.free_unif]
Make.Import.VSet.solved_var_inc_not_mem [in unification.free_unif]
Make.Import.VSet.solved_var_inc_not_mem_list [in unification.free_unif]
Make.Import.VSet.solved_var_inc_not_mem_subst [in unification.free_unif]
Make.Import.VSet.solved_var_inc_occ_in_subst [in unification.free_unif]
Make.Import.VSet.solved_var_inc_subst [in unification.free_unif]
Make.Import.VSet.solved_var_inc_term [in unification.free_unif]
Make.Import.VSet.solved_var_swapp_eq [in unification.free_unif]
Make.Import.VSet.VSet_compat [in unification.free_unif]
Make.Import.VSet.wf_lt_exc_pb_ok [in unification.free_unif]
Make.Import.VSet.wf_lt_ms [in unification.free_unif]
Make.Import.VSet.wf_lt_pb [in unification.free_unif]
Make.In_existsb_term_eq [in examples.cime_trace.equational_extension]
Make.nf_dec_inner_dec [in term_algebra.rwr_strategies]
Make.nf_P_step_subterm [in term_algebra.rwr_strategies]
Make.one_step_nf_inner_step_nf [in term_algebra.rwr_strategies]
Make.P_acc_subterms [in term_algebra.rwr_strategies]
Make.P_acc_subterms_1 [in term_algebra.rwr_strategies]
Make.P_acc_subterms_3 [in term_algebra.rwr_strategies]
Make.P_acc_with_subterm [in term_algebra.rwr_strategies]
Make.P_acc_with_subterm_subterms [in term_algebra.rwr_strategies]
Make.P_context_cons [in term_algebra.rwr_strategies]
Make.P_context_in [in term_algebra.rwr_strategies]
Make.P_general_context [in term_algebra.rwr_strategies]
Make.P_general_context_aux [in term_algebra.rwr_strategies]
Make.P_list_expand [in term_algebra.rwr_strategies]
Make.P_list_length_eq [in term_algebra.rwr_strategies]
Make.P_step_context_in [in term_algebra.rwr_strategies]
Make.P_step_in_list [in term_algebra.rwr_strategies]
Make.P_step_one_step [in term_algebra.rwr_strategies]
Make.RSTSN [in examples.cime_trace.equational_extension]
Make.RSTSN_symb [in examples.cime_trace.equational_extension]
Make.rwr_inner_or_eq [in term_algebra.rwr_strategies]
Make.rwr_inner_or_eq_bis [in term_algebra.rwr_strategies]
Make.rwr_inner_or_eq_subst [in term_algebra.rwr_strategies]
Make.R_list_Acc [in examples.cime_trace.equational_extension]
Make.STb_equiv [in examples.cime_trace.equational_extension]
Make.STPSN [in examples.cime_trace.equational_extension]
Make.STP_equiv [in examples.cime_trace.equational_extension]
Make.STSN [in examples.cime_trace.equational_extension]
Make.term_eq_ok [in examples.cime_trace.equational_extension]
Make.term_eq_refl [in examples.cime_trace.equational_extension]
Make.trans_clos_P_list_expand [in term_algebra.rwr_strategies]
Make.trans_clos_P_list_P_list [in term_algebra.rwr_strategies]
Make.trans_clos_P_list_split [in term_algebra.rwr_strategies]
Make.trans_clos_P_step_P_list [in term_algebra.rwr_strategies]
Make.var_P_acc [in term_algebra.rwr_strategies]
Make.Well_Founded_ST [in examples.cime_trace.equational_extension]
Make_EQTH_facts.one_step_list_star_decompose_cons [in examples.cime_trace.rpo_extension]
Make_EQTH_facts.one_step_list_star_decompose_nil [in examples.cime_trace.rpo_extension]
Make_EQTH_facts.one_step_list_star_l [in examples.cime_trace.rpo_extension]
Make_EQTH_facts.one_step_list_star_r [in examples.cime_trace.rpo_extension]
Make_EQTH_facts.rwr_as_star [in examples.cime_trace.rpo_extension]
mapii_dep_eq [in list_extensions.more_list]
mapii_dep_spec [in list_extensions.more_list]
mapii_dep_unfold [in list_extensions.more_list]
mapii_spec [in list_extensions.more_list]
mapi_spec [in list_extensions.more_list]
map_dep_call [in list_extensions.more_list]
map_duplicate [in list_extensions.more_list]
map_eq [in list_extensions.more_list]
map_id [in list_extensions.more_list]
merge_correct [in list_extensions.more_list]
merge_inv [in list_extensions.more_list]


N

Nat.eq_dec [in basis.ordered_set]
Nat.o_dec [in basis.ordered_set]
Nat.o_proof [in basis.ordered_set]
Nat.o_total [in basis.ordered_set]
nb_occ_app [in list_extensions.more_list]
none_nb_occ_O [in list_extensions.more_list]
no_infinite_sequence2 [in examples.cime_trace.rewriting]
nth_error_at_pos [in list_extensions.more_list]
nth_error_map [in list_extensions.more_list]
nth_error_nil [in list_extensions.more_list]
nth_error_ok_in [in list_extensions.more_list]
nth_error_remove [in list_extensions.more_list]


P

permut_add_inside [in list_extensions.list_permut]
permut_app [in list_extensions.list_permut]
permut_app1 [in list_extensions.list_permut]
permut_app2 [in list_extensions.list_permut]
permut_closure [in list_extensions.math_permut]
permut_cons_inside [in list_extensions.list_permut]
permut_dec [in list_extensions.list_permut]
permut_impl [in list_extensions.list_permut]
permut_inv_left_strong [in list_extensions.list_permut]
permut_inv_right [in list_extensions.list_permut]
permut_inv_right_strong [in list_extensions.list_permut]
permut_length [in list_extensions.list_permut]
permut_length_1 [in list_extensions.list_permut]
permut_length_2 [in list_extensions.list_permut]
permut_list_exists [in list_extensions.list_permut]
permut_list_forall_exists [in list_extensions.list_permut]
permut_map [in list_extensions.list_permut]
permut_nil [in list_extensions.list_permut]
permut_refl [in list_extensions.list_permut]
permut_rev [in list_extensions.list_permut]
permut_size [in list_extensions.list_permut]
permut_strong [in list_extensions.list_permut]
permut_swapp [in list_extensions.list_permut]
permut_sym [in list_extensions.list_permut]
permut_trans [in list_extensions.list_permut]
pos_expr_if_all_pos [in examples.cime_trace.ring_extention]
pos_expr_if_all_pos' [in examples.cime_trace.ring_extention]
pos_expr_if_all_pos_aux [in examples.cime_trace.ring_extention]
pos_expr_if_all_pos_aux' [in examples.cime_trace.ring_extention]
pos_expr_incr [in examples.cime_trace.ring_extention]
pos_expr_incr_aux [in examples.cime_trace.ring_extention]
pos_pol_incr [in examples.cime_trace.ring_extention]
pos_pol_incr' [in examples.cime_trace.ring_extention]
Pphi_nil [in examples.cime_trace.ring_extention]
prop_map12_without_repetition [in list_extensions.more_list]
prop_map_without_repetition [in list_extensions.more_list]


R

reduce_assoc_list [in list_extensions.more_list]
RPO.Import.Import.Import.Make.Import.Import.equiv_dec [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_equiv [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_same_length [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_same_size [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_same_top [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.acc_build [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_acc_rpo [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_add_context [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_equation [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_is_complete_true [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_is_sound_weak [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_list_fully_evaluates [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_list_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval_terminates [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_1 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_2 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_3 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_rpo_equiv_4 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_subst [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.find_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval_equation [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval_fully_evaluates [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.list_permut_map_acc [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mem_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mult_eval_fully_evaluates [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mult_eval_is_sound_weak [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.prec_eval_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_fully_evaluates [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_list_fully_evaluates [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_eval_list_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_is_sound_none [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_is_sound_some [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.remove_equiv_list_is_sound [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_add_context [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_antirefl [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_closure [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_dec [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_equation [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_complete [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_complete_equivalent [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_complete_less_greater [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_is_sound_weak [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval_terminates [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_lex_same_length [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_remove_equiv_aux [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_rest_trans_clos [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_trans_clos [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subst [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subterm [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subterm_equiv [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_subterm_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_trans [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size2_lex1_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size2_lex2_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size3_lex1_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size3_lex2_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size3_lex3_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.size_direct_subterm_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.term_rec3_mem [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.trans_clos_subterm_rpo [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.two_cases_rpo [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.var_case2 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.well_formed_equiv [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.well_formed_list_is_well_formed_list [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo_lex_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo_mul_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.wf_rpo_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size2_trans [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size3_trans [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex1 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex1_bis [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex2 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2_lex2_bis [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex1 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex1_bis [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex2 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3_lex3 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.wf_size [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.wf_size2 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.wf_size3 [in term_orderings.rpo]
rpo_facts.apply_subst_in [in examples.cime_trace.rpo_extension]
rpo_facts.equiv_add_context [in examples.cime_trace.rpo_extension]
rpo_facts.equiv_in_list [in examples.cime_trace.rpo_extension]
rpo_facts.equiv_refl [in examples.cime_trace.rpo_extension]
rpo_facts.equiv_subst [in examples.cime_trace.rpo_extension]
rpo_facts.equiv_sym [in examples.cime_trace.rpo_extension]
rpo_facts.equiv_trans [in examples.cime_trace.rpo_extension]
rpo_facts.In_map_l [in examples.cime_trace.rpo_extension]
rpo_facts.map_map_fst [in examples.cime_trace.rpo_extension]
rpo_facts.map_map_snd [in examples.cime_trace.rpo_extension]
rpo_facts.one_R_in_rpo [in examples.cime_trace.rpo_extension]
rpo_facts.one_R_in_rpo_eq [in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_add_context [in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_in_list [in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_subst [in examples.cime_trace.rpo_extension]
rpo_facts.rpo_eq_trans [in examples.cime_trace.rpo_extension]
rpo_facts.rpo_in_list [in examples.cime_trace.rpo_extension]
rpo_facts.wf_prec_implies_wf_R [in examples.cime_trace.rpo_extension]


S

Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.apply_subst_const [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.empty_subst_is_id [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.empty_subst_is_id_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.exists_subterm_is_a_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.is_a_pos_exists_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_call1 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_call2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_call3 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_complete [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_correct [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_correct_aux [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_unfold [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching_unfold2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.remove_garbage_subst [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_in_replace_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_is_replace_at_pos1 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_is_replace_at_pos2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_list_replace_at_pos_in_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_replace_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_unfold [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.restrict_domain_ok [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.restrict_domain_ok2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_ge_one [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_subterm_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp_is_subst_comp [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp_is_subst_comp_aux1 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp_is_subst_comp_aux2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_eq_vars [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_at_pos_dec [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_in_instantiated_term [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_in_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_in_subterm2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_direct_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term_list_app [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term_unfold [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_in_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_in_subterm2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_list_unfold [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_apply_subst [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_fold [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_unfold [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.wf_size [in term_algebra.term]
SN_incl [in examples.cime_trace.rewriting]
some_nb_occ_Sn [in list_extensions.more_list]
Sort.Import.Import.Make.Import.Import.in_quicksort_cons [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.in_quick_in [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.in_remove_list [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.length_quicksort [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.partition_list_permut1 [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_permut [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_permut_bis [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted_aux1 [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted_aux3 [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.quick_sorted_aux4 [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.sorted_cons_min [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.sorted_tl_sorted [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.sort_is_unique [in list_extensions.list_sort]
split_all_is_sound [in list_extensions.list_permut]
split_list [in list_extensions.more_list]
split_map [in list_extensions.more_list]
star_R [in examples.cime_trace.terminaison]
star_trans [in examples.cime_trace.terminaison]
strict_pos_expr_if_all_pos [in examples.cime_trace.ring_extention]
strict_pos_expr_if_all_pos' [in examples.cime_trace.ring_extention]
strict_pos_expr_if_all_pos_aux [in examples.cime_trace.ring_extention]
strict_pos_expr_if_all_pos_aux' [in examples.cime_trace.ring_extention]
S.Import.Import.Make.Import.Import.add_comm [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_prf [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_12 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_eq_set [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_subset [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union_inter_12 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal_union_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_mem_mem [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_dec [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_list_permut_support [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_refl [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_sym [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set_trans [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_union [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_1_list [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter_2_list [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.included_filter_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.included_remove_red [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_12 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_12_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_1_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter_2_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.mem_dec [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.not_mem_eq [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.remove_red_included [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.strict_subset_set_diff [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_cardinal_not_eq_not_eq_set [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_compat [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_compat_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_compat_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_dec [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_filter [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_inter_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_inter_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_set_diff [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_subset_union [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_union_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset_union_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_assoc [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_comm [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_compat_eq_set [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_compat_subset_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_compat_subset_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_empty_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_empty_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_1 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_12 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_12_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_1_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_2 [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union_2_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_add_without_red [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_filter_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_nil [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_not_in [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_permut [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove_not_common [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove_not_common_aux [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_remove_red [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.without_red_singleton [in list_extensions.list_set]
S.Import.Make.Import.ac_size_build_eq [in ac_matching.matching_well_founded]
S.Import.Make.Import.ac_size_build_lt [in ac_matching.matching_well_founded]
S.Import.Make.Import.ac_size_build_lt_args [in ac_matching.matching_well_founded]
S.Import.Make.Import.ac_syntactic [in list_extensions.list_permut]
S.Import.Make.Import.ac_syntactic_aux [in list_extensions.list_permut]
S.Import.Make.Import.add_a_subterm [in ac_matching.matching_sound]
S.Import.Make.Import.add_a_subterm_subst [in ac_matching.matching_sound]
S.Import.Make.Import.add_new_var_to_rough_sol [in ac_matching.matching]
S.Import.Make.Import.add_new_var_to_subst [in ac_matching.matching]
S.Import.Make.Import.associativity [in ac_matching.cf_eq_ac]
S.Import.Make.Import.cf_eq_ac [in ac_matching.cf_eq_ac]
S.Import.Make.Import.commutativity [in ac_matching.cf_eq_ac]
S.Import.Make.Import.cons_permut_mem [in list_extensions.list_permut]
S.Import.Make.Import.diff_mem_remove [in list_extensions.list_permut]
S.Import.Make.Import.extract_solution_in_partly_solved_part [in ac_matching.matching_algo]
S.Import.Make.Import.extract_solution_in_solved_part [in ac_matching.matching_algo]
S.Import.Make.Import.extract_solution_unfold [in ac_matching.matching_algo]
S.Import.Make.Import.F_wf_solve_dec1 [in ac_matching.matching_algo]
S.Import.Make.Import.F_wf_solve_dec2 [in ac_matching.matching_algo]
S.Import.Make.Import.in_impl_mem [in list_extensions.list_permut]
S.Import.Make.Import.list_permut_app_app [in list_extensions.list_permut]
S.Import.Make.Import.list_permut_occurs_in_term_list [in ac_matching.matching]
S.Import.Make.Import.matching_is_complete [in ac_matching.matching_algo]
S.Import.Make.Import.matching_is_sound [in ac_matching.matching_algo]
S.Import.Make.Import.matching_step1_is_complete [in ac_matching.matching_algo]
S.Import.Make.Import.matching_step1_is_sound [in ac_matching.matching_algo]
S.Import.Make.Import.matching_step2_is_complete [in ac_matching.matching_algo]
S.Import.Make.Import.matching_step2_is_sound [in ac_matching.matching_algo]
S.Import.Make.Import.mem_dec [in list_extensions.list_permut]
S.Import.Make.Import.mem_insert [in list_extensions.list_permut]
S.Import.Make.Import.mem_or_app [in list_extensions.list_permut]
S.Import.Make.Import.mem_permut_mem [in list_extensions.list_permut]
S.Import.Make.Import.mem_split_set [in list_extensions.list_permut]
S.Import.Make.Import.middle_commutativity [in ac_matching.cf_eq_ac]
S.Import.Make.Import.new_var_occ_in_solved_part [in ac_matching.matching_algo]
S.Import.Make.Import.permut_add_inside [in list_extensions.list_permut]
S.Import.Make.Import.permut_app1 [in list_extensions.list_permut]
S.Import.Make.Import.permut_app2 [in list_extensions.list_permut]
S.Import.Make.Import.permut_cons [in list_extensions.list_permut]
S.Import.Make.Import.permut_cons_inside [in list_extensions.list_permut]
S.Import.Make.Import.permut_dec [in list_extensions.list_permut]
S.Import.Make.Import.permut_refl [in list_extensions.list_permut]
S.Import.Make.Import.permut_sym [in list_extensions.list_permut]
S.Import.Make.Import.permut_trans [in list_extensions.list_permut]
S.Import.Make.Import.remove_a_subterm [in ac_matching.matching_complete]
S.Import.Make.Import.remove_equiv_is_sound [in list_extensions.list_permut]
S.Import.Make.Import.remove_is_sound [in list_extensions.list_permut]
S.Import.Make.Import.remove_several_subterms [in ac_matching.matching_complete]
S.Import.Make.Import.remove_several_subterms_bis [in ac_matching.matching_complete]
S.Import.Make.Import.remove_several_subterms_bis_nil [in ac_matching.matching_complete]
S.Import.Make.Import.solve_is_complete [in ac_matching.matching_complete]
S.Import.Make.Import.solve_is_sound [in ac_matching.matching_sound]
S.Import.Make.Import.split_cf [in ac_matching.cf_eq_ac]
S.Import.Make.Import.swap_left [in ac_matching.cf_eq_ac]
S.Import.Make.Import.swap_right [in ac_matching.cf_eq_ac]
S.Import.Make.Import.syntactic_dec [in ac_matching.cf_eq_ac]
S.Import.Make.Import.variable_preservation [in ac_matching.matching_algo]
S.Import.Make.Import.weight_is_weight [in ac_matching.matching_algo]
S.Import.Make.Import.well_formed_init_pb [in ac_matching.matching_algo]
S.Import.Make.Import.well_formed_solve [in ac_matching.matching_well_formed]
S.Import.Make.Import.well_founded_o_lpb [in ac_matching.matching_algo]
S.Import.Make.Import.well_founded_solve [in ac_matching.matching_well_founded]
S.Import.Make.Import.wf_projection [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_cons [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_is_complete [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_is_sound [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_end [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_is_complete [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_is_sound [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop_unfold [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_nil [in ac_matching.matching_algo]
S.Import.TO.Import.Make.EqTh.Import.ac_one_step_at_top_top_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac_one_step_top_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac_top_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.comm [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_cf_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_at_top_cf_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_at_top_size_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_cf_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_one_step_size_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size_ge_one [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size_unfold [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.apply_cf_subst_is_sound [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.build_eq_Term [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_app [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_apply_cf_subst [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_build [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_build_cons [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_build_inside [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_cf [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten_cf_cf [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.is_subst_cf_is_subst_cf [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.length_flatten [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.length_flatten_bis [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.length_flatten_ter [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.list_permut_flatten [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.size_size [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.size_size_aux2 [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.size_size_aux3 [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.sym_refl_ac_one_step_at_top_cf_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.sym_refl_ac_one_step_at_top_size_eq [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_alien [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_apply_subst [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_build [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_build_cons [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_build_inside [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_fold [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_is_well_formed_cf [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_is_well_formed_cf_conv [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_length [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_sorted [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subst_is_well_formed_cf_subst [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subst_is_well_formed_cf_subst_aux [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subterms [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_unfold [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.l_assoc [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.no_need_of_instance [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.r_assoc [in ac_matching.ac]


T

tail_in [in examples.cime_trace.ring_extention]
tail_prop [in list_extensions.more_list]
tail_set [in list_extensions.more_list]
termineR2 [in examples.cime_trace.rewriting]
termineR2aux [in examples.cime_trace.rewriting]
termine_gt_compat [in examples.cime_trace.rewriting]
termine_incl [in examples.cime_trace.rewriting]
Term_ordering.Import.OF.OX.Make.Import.eq_dec [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_anti_sym [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_dec [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_proof [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_term_list_is_o_term_list [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_total [in term_orderings.term_o]
trans_clos_is_clos [in basis.closure]
trans_clos_is_trans [in basis.closure]
trans_inversion [in basis.closure]


W

wf_length [in list_extensions.more_list]
wf_lex [in term_orderings.rpo]
wf_trans [in basis.closure]



Constructor Index

A

AC [in term_algebra.term]
ACU.F.LU [in unification.unification]
ACU.F.Make.Import.left_unit [in unification.unification]
ACU.F.Make.Import.right_unit [in unification.unification]


C

C [in term_algebra.term]
CaseA [in basis.closure]
CaseB [in basis.closure]


D

Dep_fun [in list_extensions.more_list]
D.Import.Import.Make.Import.Import.Import.rmv_case [in list_extensions.dickson]
D.Import.Import.rmv_case [in list_extensions.dickson]


E

EqTh.T.at_top [in term_algebra.equational_theory]
EqTh.T.Const [in term_algebra.equational_theory]
EqTh.T.Def [in term_algebra.equational_theory]
EqTh.T.head_step [in term_algebra.equational_theory]
EqTh.T.instance [in term_algebra.equational_theory]
EqTh.T.in_context [in term_algebra.equational_theory]
EqTh.T.Mod [in term_algebra.equational_theory]
EqTh.T.tail_step [in term_algebra.equational_theory]
EqTh.T.VT.Make.at_top [in term_algebra.equational_theory]
EqTh.T.VT.Make.Const [in term_algebra.equational_theory]
EqTh.T.VT.Make.Def [in term_algebra.equational_theory]
EqTh.T.VT.Make.head_step [in term_algebra.equational_theory]
EqTh.T.VT.Make.instance [in term_algebra.equational_theory]
EqTh.T.VT.Make.in_context [in term_algebra.equational_theory]
EqTh.T.VT.Make.Mod [in term_algebra.equational_theory]
EqTh.T.VT.Make.tail_step [in term_algebra.equational_theory]
Equivalent [in basis.ordered_set]


F

Free [in term_algebra.term]


G

Greater_than [in basis.ordered_set]


L

Less_than [in basis.ordered_set]
Lex [in term_orderings.rpo]


M

MakeDP.Ccase [in term_orderings.dp]
MakeDP.Constr [in term_orderings.dp]
MakeDP.Dcase [in term_orderings.dp]
MakeDP.Defd [in term_orderings.dp]
MakeDP.Dp [in term_orderings.dp]
MakeDP.Dp_gen_step [in term_orderings.dp]
MakeDP.Dp_simple_step [in term_orderings.dp]
MakeDP.Mdp [in term_orderings.dp]
MakeDP.Pi1 [in term_orderings.dp]
MakeDP.Pi2 [in term_orderings.dp]
MakeDP.Rmdp_gen_step [in term_orderings.dp]
MakeDP.Rmdp_simple_step [in term_orderings.dp]
MakeDP.Vcase [in term_orderings.dp]
Make.Import.Import.IDp_gen_step [in term_orderings.inner_dp]
Make.Import.Import.IDp_simple_step [in term_orderings.inner_dp]
Make.Import.Import.Psi_at_top [in term_orderings.inner_dp]
Make.Import.Import.Psi_in_context [in term_orderings.inner_dp]
Make.Import.Normal [in unification.free_unif]
Make.Import.Not_appliable [in unification.free_unif]
Make.Import.No_solution [in unification.free_unif]
Make.Import.VSet.OK [in unification.free_unif]
Make.Monotone_c [in examples.cime_trace.equational_extension]
Make.P_at_top [in term_algebra.rwr_strategies]
Make.P_head_step [in term_algebra.rwr_strategies]
Make.P_in_context [in term_algebra.rwr_strategies]
Make.P_tail_step [in term_algebra.rwr_strategies]
Make.RST_c [in examples.cime_trace.equational_extension]
Mul [in term_orderings.rpo]


P

Pcons [in list_extensions.list_permut]
Pnil [in list_extensions.list_permut]


R

RPO.Import.Import.Eq [in term_orderings.rpo]
RPO.Import.Import.Eq_lex [in term_orderings.rpo]
RPO.Import.Import.Eq_list_cons [in term_orderings.rpo]
RPO.Import.Import.Eq_list_nil [in term_orderings.rpo]
RPO.Import.Import.Eq_mul [in term_orderings.rpo]
RPO.Import.Import.Import.Equiv [in term_orderings.rpo]
RPO.Import.Import.Import.List_eq [in term_orderings.rpo]
RPO.Import.Import.Import.List_gt [in term_orderings.rpo]
RPO.Import.Import.Import.List_mul [in term_orderings.rpo]
RPO.Import.Import.Import.Lt [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_lex [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_list_cons [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_list_nil [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Eq_mul [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Equiv [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Found [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_eq [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_gt [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_mul [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.List_mul_step [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Lt [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Not_finished [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Not_found [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Rpo_lex_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Rpo_mul_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Rpo_mul_step_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Subterm [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_lex [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_lex_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_mul [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_eq_mul_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_gt [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.Top_gt_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Subterm [in term_orderings.rpo]
RPO.Import.Import.Import.Top_eq_lex [in term_orderings.rpo]
RPO.Import.Import.Import.Top_eq_mul [in term_orderings.rpo]
RPO.Import.Import.Import.Top_gt [in term_orderings.rpo]
R2_intro [in examples.cime_trace.rewriting]
r_trans [in basis.closure]


S

Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.Term [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.Var [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Term [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Var [in term_algebra.term]
Sort.Import.Import.is_sorted_cons1 [in list_extensions.list_sort]
Sort.Import.Import.is_sorted_cons2 [in list_extensions.list_sort]
Sort.Import.Import.is_sorted_nil [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted_cons1 [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted_cons2 [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted_nil [in list_extensions.list_sort]
star_refl [in examples.cime_trace.terminaison]
star_step [in examples.cime_trace.terminaison]
S.Import.Make.Import.W [in ac_matching.matching_algo]
S.Import.TO.Import.a_axiom [in ac_matching.ac]
S.Import.TO.Import.c_axiom [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.a_axiom [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.c_axiom [in ac_matching.ac]
S.Import.W [in ac_matching.matching_algo]


T

t_clos [in basis.closure]
t_step [in basis.closure]
t_trans [in basis.closure]


U

Uncomparable [in basis.ordered_set]



Inductive Index

A

ACU.F.Make.Import.unit_one_step_at_top [in unification.unification]
ACU.F.unit_theory_type [in unification.unification]
arity_type [in term_algebra.term]


C

comp [in basis.ordered_set]


D

dep_fun [in list_extensions.more_list]
D.Import.Import.Make.Import.Import.Import.multiset_extension_step [in list_extensions.dickson]
D.Import.Import.multiset_extension_step [in list_extensions.dickson]


E

EqTh.T.axiom [in term_algebra.equational_theory]
EqTh.T.constructor [in term_algebra.equational_theory]
EqTh.T.defined [in term_algebra.equational_theory]
EqTh.T.module [in term_algebra.equational_theory]
EqTh.T.one_step [in term_algebra.equational_theory]
EqTh.T.one_step_list [in term_algebra.equational_theory]
EqTh.T.VT.Make.axiom [in term_algebra.equational_theory]
EqTh.T.VT.Make.constructor [in term_algebra.equational_theory]
EqTh.T.VT.Make.defined [in term_algebra.equational_theory]
EqTh.T.VT.Make.module [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step [in term_algebra.equational_theory]
EqTh.T.VT.Make.one_step_list [in term_algebra.equational_theory]


M

MakeDP.dp [in term_orderings.dp]
MakeDP.Empty_R [in term_orderings.dp]
MakeDP.Interp [in term_orderings.dp]
MakeDP.interp_call [in term_orderings.dp]
MakeDP.mdp [in term_orderings.dp]
MakeDP.Pi [in term_orderings.dp]
MakeDP.rdp_step [in term_orderings.dp]
MakeDP.rmdp_step [in term_orderings.dp]
MakeDP.rwr_rel [in term_orderings.dp]
Make.Import.exc [in unification.free_unif]
Make.Import.Import.idp_step [in term_orderings.inner_dp]
Make.Import.Import.Psi [in term_orderings.inner_dp]
Make.Import.unification_problem [in unification.free_unif]
Make.Import.VSet.exc_pb_ok [in unification.free_unif]
Make.Monotone [in examples.cime_trace.equational_extension]
Make.P_list [in term_algebra.rwr_strategies]
Make.P_step [in term_algebra.rwr_strategies]
Make.RST [in examples.cime_trace.equational_extension]


P

permut [in list_extensions.list_permut]
product_o [in basis.closure]


R

refl_trans_clos [in basis.closure]
RPO.Import.Import.equiv [in term_orderings.rpo]
RPO.Import.Import.equiv_list_lex [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.equiv_list_lex [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.result [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eq [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_inf [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_lex [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_lex_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_step [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_mul_step_rest [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_rest [in term_orderings.rpo]
RPO.Import.Import.Import.rpo [in term_orderings.rpo]
RPO.Import.Import.Import.rpo_eq [in term_orderings.rpo]
RPO.Import.Import.Import.rpo_lex [in term_orderings.rpo]
RPO.Import.Import.Import.rpo_mul [in term_orderings.rpo]
R2 [in examples.cime_trace.rewriting]


S

Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.term [in term_algebra.term]
Sort.Import.Import.is_sorted [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.is_sorted [in list_extensions.list_sort]
star [in examples.cime_trace.terminaison]
status_type [in term_orderings.rpo]
S.Import.Import.Make.Import.Import.t [in list_extensions.list_set]
S.Import.Import.t [in list_extensions.list_set]
S.Import.Make.Import.matching_problem [in ac_matching.matching]
S.Import.Make.Import.partly_solved_term [in ac_matching.matching]
S.Import.Make.Import.well_formed_matching_problem [in ac_matching.matching_algo]
S.Import.matching_problem [in ac_matching.matching]
S.Import.partly_solved_term [in ac_matching.matching]
S.Import.TO.Import.ac_one_step_at_top [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac_one_step_at_top [in ac_matching.ac]
S.Import.well_formed_matching_problem [in ac_matching.matching_algo]


T

trans_clos [in basis.closure]



Definition Index

A

ACU.F.is_coherent [in unification.unification]
ACU.F.Make.Import.acu [in unification.unification]
ACU.F.Make.Import.unit_nf [in unification.unification]
ACU.F.Make.Import.unit_th [in unification.unification]


C

Convert.A [in basis.decidable_set]
Convert.A [in basis.decidable_set]
Convert.eq_A [in basis.decidable_set]
Convert.eq_A [in basis.decidable_set]


D

dep_fun_tail [in list_extensions.more_list]
D.Import.Import.EDS [in list_extensions.dickson]
D.Import.Import.EDS [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.A [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.LDS.eq_A [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.mult [in list_extensions.dickson]
D.Import.Import.Make.Import.Import.Import.R_or_eq_dec [in list_extensions.dickson]
D.Import.Import.Make.LP [in list_extensions.dickson]
D.Import.Import.Make.LP [in list_extensions.dickson]


E

EqTh.T.rwr [in term_algebra.equational_theory]
EqTh.T.rwr_list [in term_algebra.equational_theory]
EqTh.T.VT.A [in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_head_red [in term_algebra.equational_theory]
EqTh.T.VT.Make.compute_red [in term_algebra.equational_theory]
EqTh.T.VT.Make.F_compute_red [in term_algebra.equational_theory]
EqTh.T.VT.Make.non_overlapping [in term_algebra.equational_theory]
EqTh.T.VT.Make.overlay [in term_algebra.equational_theory]
EqTh.T.VT.Make.o_size [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_list [in term_algebra.equational_theory]
EqTh.T.VT.Make.rwr_subst [in term_algebra.equational_theory]
EqTh.T.VT.Make.sym_refl [in term_algebra.equational_theory]
EqTh.T.VT.Make.th_eq [in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.A [in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.A [in term_algebra.equational_theory]
EqTh.T.VT.Make.VT.eq_A [in term_algebra.equational_theory]
EqTh.T.VT.non_overlapping [in term_algebra.equational_theory]
EqTh.T.VT.overlay [in term_algebra.equational_theory]
EqTh.T.VT.sym_refl [in term_algebra.equational_theory]
EqTh.T.VT.th_eq [in term_algebra.equational_theory]


F

fold_left2 [in list_extensions.more_list]
F_mapii [in list_extensions.more_list]


I

included_list [in list_extensions.more_list]


L

length_app [in list_extensions.more_list]
length_map [in list_extensions.more_list]
lex [in term_orderings.rpo]
list_contents [in list_extensions.math_permut]
list_exists_rest [in list_extensions.more_list]
list_rec2 [in list_extensions.more_list]
list_rec3 [in list_extensions.more_list]
list_size [in list_extensions.more_list]


M

MakeDP.Comb [in term_orderings.dp]
MakeDP.defined_list [in term_orderings.dp]
MakeDP.defined_subterms [in term_orderings.dp]
MakeDP.dp_list [in term_orderings.dp]
MakeDP.dp_rule [in term_orderings.dp]
MakeDP.dp_step [in term_orderings.dp]
MakeDP.Incomp1' [in term_orderings.dp]
MakeDP.Incomp2' [in term_orderings.dp]
MakeDP.Incomp3' [in term_orderings.dp]
MakeDP.Interp_dom [in term_orderings.dp]
MakeDP.Interp_subst [in term_orderings.dp]
MakeDP.is_primary_pi [in term_orderings.dp]
MakeDP.mark_term [in term_orderings.dp]
MakeDP.Pi_red [in term_orderings.dp]
MakeDP.Pi_red_list [in term_orderings.dp]
MakeDP.rwr_rel_comb [in term_orderings.dp]
MakeDP.rwr_rel_empty [in term_orderings.dp]
MakeDP.R1_R2_red [in term_orderings.dp]
MakeDP.subterm_at_pos_dec [in term_orderings.dp]
MakeDP.T12 [in term_orderings.dp]
MakeDP.T3 [in term_orderings.dp]
MakeDP.unmark_term [in term_orderings.dp]
Make.A [in unification.free_unif]
Make.A [in unification.free_unif]
Make.Import.bind [in unification.free_unif]
Make.Import.combine [in unification.free_unif]
Make.Import.Import.oo [in term_orderings.inner_dp]
Make.Import.Import.ooo [in term_orderings.inner_dp]
Make.Import.Import.psi [in term_orderings.inner_dp]
Make.Import.Import.psi_id [in term_orderings.inner_dp]
Make.Import.is_a_solution [in unification.free_unif]
Make.Import.Term_eq_dec.A [in unification.free_unif]
Make.Import.Term_eq_dec.A [in unification.free_unif]
Make.Import.Term_eq_dec.eq_dec [in unification.free_unif]
Make.Import.Term_eq_dec.eq_dec [in unification.free_unif]
Make.Import.VSet.decompose [in unification.free_unif]
Make.Import.VSet.decomposition_step_e [in unification.free_unif]
Make.Import.VSet.domain_of_subst [in unification.free_unif]
Make.Import.VSet.EDS [in unification.free_unif]
Make.Import.VSet.F_decompose [in unification.free_unif]
Make.Import.VSet.Inv_solved_part [in unification.free_unif]
Make.Import.VSet.Inv_solved_part_e [in unification.free_unif]
Make.Import.VSet.is_a_solution_e [in unification.free_unif]
Make.Import.VSet.is_a_solved_var [in unification.free_unif]
Make.Import.VSet.list_size_mul [in unification.free_unif]
Make.Import.VSet.lt_exc_pb_ok [in unification.free_unif]
Make.Import.VSet.lt_ms [in unification.free_unif]
Make.Import.VSet.lt_mul [in unification.free_unif]
Make.Import.VSet.lt_pb [in unification.free_unif]
Make.Import.VSet.lt_weight_exc_pb_ok [in unification.free_unif]
Make.Import.VSet.measure_for_unif_pb [in unification.free_unif]
Make.Import.VSet.nb_var_eq_of_unsolved_part [in unification.free_unif]
Make.Import.VSet.phi1 [in unification.free_unif]
Make.Import.VSet.phi2 [in unification.free_unif]
Make.Import.VSet.phi3 [in unification.free_unif]
Make.Import.VSet.set_of_variables [in unification.free_unif]
Make.Import.VSet.set_of_variables_in_range_of_subst [in unification.free_unif]
Make.Import.VSet.set_of_variables_in_unsolved_part [in unification.free_unif]
Make.Import.VSet.set_of_variables_list [in unification.free_unif]
Make.Import.VSet.size_of_solved_part [in unification.free_unif]
Make.Import.VSet.size_of_unsolved_part [in unification.free_unif]
Make.Import.VSet.weight_exc_pb_ok [in unification.free_unif]
Make.inner [in term_algebra.rwr_strategies]
Make.R_list [in examples.cime_trace.equational_extension]
Make.ST [in examples.cime_trace.equational_extension]
Make.STb [in examples.cime_trace.equational_extension]
Make.STPb [in examples.cime_trace.equational_extension]
Make.term_eq [in examples.cime_trace.equational_extension]
mapi [in list_extensions.more_list]
mapii [in list_extensions.more_list]
mapii_dep [in list_extensions.more_list]
mem [in list_extensions.more_list]
merge [in list_extensions.more_list]


N

Nat.A [in basis.ordered_set]
Nat.A [in basis.ordered_set]
Nat.o [in basis.ordered_set]
nf [in basis.closure]


O

o_length [in list_extensions.more_list]


P

permut [in list_extensions.math_permut]
permutation [in list_extensions.math_permut]


R

Retoile [in examples.cime_trace.rewriting]
RPO.Import.Import.A [in term_orderings.rpo]
RPO.Import.Import.Import.EDS [in term_orderings.rpo]
RPO.Import.Import.Import.EDS [in term_orderings.rpo]
RPO.Import.Import.Import.Make.A [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.add_equiv [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.empty_rpo_infos [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.equiv_eval [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.lexico_eval [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.mult_eval [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.prec_eval [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Import.rpo_eval [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size2 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.o_size3 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size2 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.size3 [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.A [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.A [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_A [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_A [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_dec [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_dec [in term_orderings.rpo]
RPO.Import.Import.Import.Make.Import.Import.Term_equiv_dec.eq_proof [in term_orderings.rpo]
rpo_facts.A [in examples.cime_trace.rpo_extension]


S

Signature.Export.Term.Import.Import.VSet.apply_subst [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.direct_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.EDS [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.EDS [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.is_a_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.apply_subst [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.direct_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.EDS [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.EDS [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.eq_term_dec [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.F_matching [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.is_a_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.map_subst [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.matching [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.o_list_size [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.replace_at_pos_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.restrict_domain [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_direct_subterm [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.size_unfold [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.substitution [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subst_comp [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.subterm_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.symb_in_term_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec2 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec3 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec4 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec7 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_rec8 [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.term_term_dec [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.var_list_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.Make'.Import.Import.VSet.well_formed_subst [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.map_subst [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.replace_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.replace_at_pos_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.restrict_domain [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.size [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.substitution [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.subst_comp [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.subterm_at_pos [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.symb_in_term [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.symb_in_term_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.var_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.var_list_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.well_formed [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.well_formed_list [in term_algebra.term]
Signature.Export.Term.Import.Import.VSet.well_formed_subst [in term_algebra.term]
Sort.Import.Import.EDS [in list_extensions.list_sort]
Sort.Import.Import.EDS [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.EDS [in list_extensions.list_sort]
Sort.Import.Import.Make.Import.Import.EDS [in list_extensions.list_sort]
split_all [in list_extensions.list_permut]
S.Import.ac_elementary_solve [in ac_matching.matching]
S.Import.ac_elementary_solve_term_term_term [in ac_matching.matching]
S.Import.ac_elementary_solve_term_var_without_val_term [in ac_matching.matching]
S.Import.ac_elementary_solve_term_var_with_part_val_term [in ac_matching.matching]
S.Import.ac_elementary_solve_term_var_with_val_term [in ac_matching.matching]
S.Import.build_well_formed_matching_problem_list [in ac_matching.matching_algo]
S.Import.clean_sol [in ac_matching.matching_algo]
S.Import.extract_solution [in ac_matching.matching_algo]
S.Import.F_wf_solve [in ac_matching.matching_algo]
S.Import.Import.cardinal [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.add [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.cardinal [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.empty [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.eq_set [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.filter [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.inter [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.make_set [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.mem [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.not_mem_dec [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.set_diff [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.singleton [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.subset [in list_extensions.list_set]
S.Import.Import.Make.Import.Import.union [in list_extensions.list_set]
S.Import.Import.mem [in list_extensions.list_set]
S.Import.Import.subset [in list_extensions.list_set]
S.Import.Import.without_red [in list_extensions.list_set]
S.Import.init_pb [in ac_matching.matching_algo]
S.Import.is_rough_sol [in ac_matching.matching]
S.Import.is_sol [in ac_matching.matching]
S.Import.is_well_formed_sol [in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve [in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_term_term [in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_var_without_val_term [in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_var_with_part_val_term [in ac_matching.matching]
S.Import.Make.Import.ac_elementary_solve_term_var_with_val_term [in ac_matching.matching]
S.Import.Make.Import.build_well_formed_matching_problem_list [in ac_matching.matching_algo]
S.Import.Make.Import.clean_sol [in ac_matching.matching_algo]
S.Import.Make.Import.extract_solution [in ac_matching.matching_algo]
S.Import.Make.Import.F_wf_solve [in ac_matching.matching_algo]
S.Import.Make.Import.init_pb [in ac_matching.matching_algo]
S.Import.Make.Import.is_rough_sol [in ac_matching.matching]
S.Import.Make.Import.is_sol [in ac_matching.matching]
S.Import.Make.Import.is_well_formed_sol [in ac_matching.matching]
S.Import.Make.Import.is_wf_sol [in ac_matching.matching_algo]
S.Import.Make.Import.is_wf_wf_sol [in ac_matching.matching_algo]
S.Import.Make.Import.matching [in ac_matching.matching_algo]
S.Import.Make.Import.mem [in list_extensions.list_permut]
S.Import.Make.Import.occurs_in_pb [in ac_matching.matching]
S.Import.Make.Import.occurs_in_term [in ac_matching.matching]
S.Import.Make.Import.occurs_in_term_list [in ac_matching.matching]
S.Import.Make.Import.o_lpb [in ac_matching.matching_algo]
S.Import.Make.Import.pb_weight [in ac_matching.matching_well_founded]
S.Import.Make.Import.solve [in ac_matching.matching]
S.Import.Make.Import.well_formed_pb [in ac_matching.matching]
S.Import.Make.Import.well_sorted_partly_solved_part [in ac_matching.matching]
S.Import.Make.Import.wfpb_weight [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve [in ac_matching.matching_algo]
S.Import.Make.Import.wf_solve_loop [in ac_matching.matching_algo]
S.Import.matching [in ac_matching.matching_algo]
S.Import.mem [in list_extensions.list_permut]
S.Import.occurs_in_pb [in ac_matching.matching]
S.Import.occurs_in_term [in ac_matching.matching]
S.Import.occurs_in_term_list [in ac_matching.matching]
S.Import.o_lpb [in ac_matching.matching_algo]
S.Import.pb_weight [in ac_matching.matching_well_founded]
S.Import.solve [in ac_matching.matching]
S.Import.TO.A [in ac_matching.ac]
S.Import.TO.Import.ac [in ac_matching.ac]
S.Import.TO.Import.ac_size [in ac_matching.ac]
S.Import.TO.Import.apply_cf_subst [in ac_matching.ac]
S.Import.TO.Import.build [in ac_matching.ac]
S.Import.TO.Import.canonical_form [in ac_matching.ac]
S.Import.TO.Import.flatten [in ac_matching.ac]
S.Import.TO.Import.Make.A [in ac_matching.ac]
S.Import.TO.Import.Make.A [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.ac [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.ac_size [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.apply_cf_subst [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.build [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.canonical_form [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.flatten [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.is_subst_canonical_form [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf [in ac_matching.ac]
S.Import.TO.Import.Make.EqTh.Import.Import.well_formed_cf_subst [in ac_matching.ac]
S.Import.TO.Import.well_formed_cf [in ac_matching.ac]
S.Import.TO.Import.well_formed_cf_subst [in ac_matching.ac]
S.Import.well_formed_pb [in ac_matching.matching]
S.Import.well_sorted_partly_solved_part [in ac_matching.matching]
S.Import.wfpb_weight [in ac_matching.matching_algo]
S.Import.wf_solve [in ac_matching.matching_algo]
S.Import.wf_solve_loop [in ac_matching.matching_algo]


T

Term_ordering.Import.OF.A [in term_orderings.term_o]
Term_ordering.Import.OF.OX.A [in term_orderings.term_o]
Term_ordering.Import.OF.OX.A [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.A [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.A [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.A [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.A [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o [in term_orderings.term_o]
Term_ordering.Import.OF.OX.Make.Import.o_term_list [in term_orderings.term_o]
Term_ordering.Import.OF.OX.o [in term_orderings.term_o]



Module Index

A

ACU [in unification.unification]


C

Convert [in basis.decidable_set]


D

D [in list_extensions.dickson]


E

EqTh [in term_algebra.equational_theory]
EqTh [in ac_matching.ac]
ES [in basis.ordered_set]
ES [in basis.decidable_set]
Export [in term_algebra.term]


F

F [in unification.unification]


I

Import [in list_extensions.dickson]
Import [in list_extensions.dickson]
Import [in ac_matching.cf_eq_ac]
Import [in list_extensions.dickson]
Import [in ac_matching.matching_well_formed]
Import [in term_orderings.term_o]
Import [in list_extensions.list_set]
Import [in ac_matching.matching_algo]
Import [in ac_matching.matching]
Import [in ac_matching.ac]
Import [in ac_matching.cf_eq_ac]
Import [in ac_matching.matching_well_founded]
Import [in term_orderings.inner_dp]
Import [in list_extensions.list_permut]
Import [in ac_matching.matching_sound]
Import [in ac_matching.matching_algo]
Import [in list_extensions.dickson]
Import [in term_orderings.term_o]
Import [in term_algebra.term]
Import [in ac_matching.matching_well_formed]
Import [in term_orderings.rpo]
Import [in term_algebra.term]
Import [in list_extensions.dickson]
Import [in list_extensions.list_sort]
Import [in unification.unification]
Import [in ac_matching.ac]
Import [in ac_matching.ac]
Import [in ac_matching.matching_well_founded]
Import [in term_orderings.rpo]
Import [in list_extensions.list_sort]
Import [in term_orderings.rpo]
Import [in list_extensions.list_permut]
Import [in list_extensions.list_sort]
Import [in list_extensions.list_set]
Import [in ac_matching.matching]
Import [in term_orderings.rpo]
Import [in list_extensions.list_set]
Import [in term_algebra.term]
Import [in list_extensions.list_set]
Import [in ac_matching.matching_complete]
Import [in ac_matching.matching_complete]
Import [in term_orderings.inner_dp]
Import [in term_orderings.rpo]
Import [in list_extensions.list_sort]
Import [in term_algebra.term]
Import [in unification.free_unif]
Import [in ac_matching.matching_sound]
Import [in term_orderings.rpo]
Import [in ac_matching.ac]


L

LDS [in list_extensions.dickson]


M

Make [in ac_matching.cf_eq_ac]
Make [in term_algebra.rwr_strategies]
Make [in ac_matching.matching]
Make [in unification.free_unif]
Make [in term_orderings.rpo]
Make [in term_orderings.inner_dp]
Make [in ac_matching.ac]
Make [in ac_matching.matching_complete]
Make [in list_extensions.dickson]
Make [in list_extensions.list_set]
Make [in ac_matching.matching_algo]
Make [in list_extensions.list_permut]
Make [in unification.unification]
Make [in list_extensions.list_sort]
Make [in examples.cime_trace.equational_extension]
Make [in term_algebra.term]
Make [in term_algebra.equational_theory]
Make [in ac_matching.matching_sound]
Make [in term_orderings.term_o]
Make [in ac_matching.matching_well_formed]
Make [in ac_matching.matching_well_founded]
MakeDP [in term_orderings.dp]
Make' [in term_algebra.term]
Make_EQTH_facts [in examples.cime_trace.rpo_extension]


N

Nat [in basis.ordered_set]


O

OF [in term_orderings.term_o]
OX [in term_orderings.term_o]


P

Precedence [in term_orderings.rpo]


R

RPO [in term_orderings.rpo]
rpo_facts [in examples.cime_trace.rpo_extension]


S

S [in ac_matching.matching_sound]
S [in ac_matching.matching]
S [in ac_matching.matching_complete]
S [in ac_matching.matching_well_formed]
S [in ac_matching.ac]
S [in ac_matching.cf_eq_ac]
S [in basis.ordered_set]
S [in list_extensions.list_permut]
S [in ac_matching.matching_well_founded]
S [in ac_matching.matching_algo]
S [in basis.decidable_set]
S [in list_extensions.list_set]
Signature [in term_algebra.term]
Sort [in list_extensions.list_sort]


T

T [in term_algebra.equational_theory]
Term [in term_algebra.term]
Term_equiv_dec [in term_orderings.rpo]
Term_eq_dec [in unification.free_unif]
Term_ordering [in term_orderings.term_o]
TO [in ac_matching.ac]


V

VSet [in unification.free_unif]
VSet [in term_algebra.term]
VSet [in term_algebra.term]
VT [in term_algebra.equational_theory]
VT [in term_algebra.equational_theory]



Library Index

A

ac


C

cf_eq_ac
closure


D

decidable_set
dickson
dp


E

equational_extension
equational_theory
equiv_list


F

free_unif


I

inner_dp


L

list_permut
list_set
list_sort


M

matching
matching_algo
matching_complete
matching_sound
matching_well_formed
matching_well_founded
math_permut
more_list


O

ordered_set


R

rewriting
ring_extention
rpo
rpo_extension
rwr_strategies


T

term
terminaison
term_o


U

unification



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1745 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (228 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (859 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (123 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (77 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (312 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (114 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (32 entries)

This page has been generated by coqdoc