| 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 | _ | other | (504 entries) |
| Notation 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 | _ | other | (8 entries) |
| Variable 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 | _ | other | (25 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 | _ | other | (9 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 | _ | other | (233 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 | _ | other | (6 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 | _ | other | (62 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 | _ | other | (13 entries) |
| Projection 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 | _ | other | (8 entries) |
| Instance 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 | _ | other | (29 entries) |
| Section 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 | _ | other | (21 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 | _ | other | (88 entries) |
| Record 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 | _ | other | (2 entries) |
Global Index
A
accn [inductive, in Recipes.Autosubst_lib.ARS]accnH [constructor, in Recipes_neutralization.Recipes_NF]
accnH [constructor, in Recipes.Autosubst_lib.ARS]
accnL [constructor, in Recipes_neutralization.Recipes_NF]
accnL [constructor, in Recipes.Autosubst_lib.ARS]
accn_ind' [definition, in Recipes_neutralization.Recipes_NF]
accn_inv [lemma, in Recipes.Autosubst_lib.ARS]
accn_ind' [definition, in Recipes.Autosubst_lib.ARS]
accn_sind [definition, in Recipes.Autosubst_lib.ARS]
accn_ind [definition, in Recipes.Autosubst_lib.ARS]
acc_if_wt [lemma, in Recipes_neutralization.Recipes_NF]
admissible_compose [lemma, in Recipes_neutralization.Recipes]
admissible_hsubst [lemma, in Recipes_neutralization.Recipes]
admissible_subst_up2 [lemma, in Recipes_neutralization.Recipes]
admissible_subst_var01 [lemma, in Recipes_neutralization.Recipes]
admissible_subst_ext [lemma, in Recipes_neutralization.Recipes]
admissible_ids [lemma, in Recipes_neutralization.Recipes]
admissible_neu [lemma, in Recipes_neutralization.Recipes]
admissible_subst_rw [lemma, in Recipes_neutralization.Recipes]
admissible_subst2 [definition, in Recipes_neutralization.Recipes]
admissible_subst [definition, in Recipes_neutralization.Recipes]
And [constructor, in Recipes_neutralization.Recipes]
and_expansion [lemma, in Recipes_neutralization.Recipes_SN]
App [constructor, in Recipes_neutralization.Recipes]
Arr [constructor, in Recipes_neutralization.Recipes]
ARS [library]
AST [section, in Recipes_neutralization.Recipes]
AutosubstSsr [library]
AutosubstTypeClasses [section, in Recipes_neutralization.Recipes]
B
beta_expansion [lemma, in Recipes_neutralization.Recipes_SN]C
cand [definition, in Recipes_neutralization.Recipes_SN]choose_last_n_hsubst [lemma, in Recipes_neutralization.My_autosubst]
choose_last_n_subst [lemma, in Recipes_neutralization.My_autosubst]
church_rosser [lemma, in Recipes_neutralization.Recipes]
classical_step [lemma, in Recipes_neutralization.Recipes_NF]
closed [definition, in Recipes_neutralization.My_autosubst]
closed_subst [lemma, in Recipes_neutralization.My_autosubst]
cofinal [definition, in Recipes.Autosubst_lib.ARS]
CoFinal [section, in Recipes.Autosubst_lib.ARS]
cofinal_normalizing [lemma, in Recipes.Autosubst_lib.ARS]
CoFinal.e [variable, in Recipes.Autosubst_lib.ARS]
CoFinal.rho [variable, in Recipes.Autosubst_lib.ARS]
CoFinal.T [variable, in Recipes.Autosubst_lib.ARS]
CoFinal.tri [variable, in Recipes.Autosubst_lib.ARS]
com [definition, in Recipes.Autosubst_lib.ARS]
Commutation [section, in Recipes.Autosubst_lib.ARS]
Commutation.T [variable, in Recipes.Autosubst_lib.ARS]
ComputationN [section, in Recipes.Autosubst_lib.ARS]
ComputationN.classical [variable, in Recipes.Autosubst_lib.ARS]
ComputationN.e [variable, in Recipes.Autosubst_lib.ARS]
ComputationN.norm [variable, in Recipes.Autosubst_lib.ARS]
ComputationN.rho [variable, in Recipes.Autosubst_lib.ARS]
ComputationN.sound [variable, in Recipes.Autosubst_lib.ARS]
ComputationN.T [variable, in Recipes.Autosubst_lib.ARS]
com_lift [lemma, in Recipes.Autosubst_lib.ARS]
com_strip [lemma, in Recipes.Autosubst_lib.ARS]
confluence [lemma, in Recipes_neutralization.Recipes]
confluent [definition, in Recipes.Autosubst_lib.ARS]
confluent_stable [lemma, in Recipes.Autosubst_lib.ARS]
confluent_cr [lemma, in Recipes.Autosubst_lib.ARS]
conv [inductive, in Recipes.Autosubst_lib.ARS]
convES [lemma, in Recipes.Autosubst_lib.ARS]
convESi [lemma, in Recipes.Autosubst_lib.ARS]
convR [constructor, in Recipes.Autosubst_lib.ARS]
convSE [constructor, in Recipes.Autosubst_lib.ARS]
convSEi [constructor, in Recipes.Autosubst_lib.ARS]
conv_neu [lemma, in Recipes_neutralization.Recipes_neutralization]
conv_closure [lemma, in Recipes.Autosubst_lib.ARS]
conv_hom [lemma, in Recipes.Autosubst_lib.ARS]
conv_img [lemma, in Recipes.Autosubst_lib.ARS]
conv_sym [lemma, in Recipes.Autosubst_lib.ARS]
conv_trans [lemma, in Recipes.Autosubst_lib.ARS]
conv_sind [definition, in Recipes.Autosubst_lib.ARS]
conv_ind [definition, in Recipes.Autosubst_lib.ARS]
conv1 [lemma, in Recipes.Autosubst_lib.ARS]
conv1i [lemma, in Recipes.Autosubst_lib.ARS]
CR [definition, in Recipes.Autosubst_lib.ARS]
cr_method [lemma, in Recipes.Autosubst_lib.ARS]
cr_conv_normal [lemma, in Recipes.Autosubst_lib.ARS]
cr_star_normal [lemma, in Recipes.Autosubst_lib.ARS]
ctx [definition, in Recipes_neutralization.Recipes]
D
Definitions [section, in Recipes.Autosubst_lib.ARS]Definitions.e [variable, in Recipes.Autosubst_lib.ARS]
Definitions.T [variable, in Recipes.Autosubst_lib.ARS]
dest [projection, in Recipes_neutralization.Recipes_NF]
dest_nf [projection, in Recipes_neutralization.Recipes_NF]
diamond [definition, in Recipes.Autosubst_lib.ARS]
diamond_confluent [lemma, in Recipes.Autosubst_lib.ARS]
E
EqDec [section, in Recipes_neutralization.Recipes]eq_nrho [projection, in Recipes_neutralization.Recipes_NF]
eq_star [lemma, in Recipes.Autosubst_lib.ARS]
eval [definition, in Recipes_neutralization.Recipes_NF]
evaln [definition, in Recipes.Autosubst_lib.ARS]
evalnP [lemma, in Recipes_neutralization.Recipes_NF]
evalnP [lemma, in Recipes.Autosubst_lib.ARS]
evaln_sound [lemma, in Recipes_neutralization.Recipes_NF]
evaln_sound [lemma, in Recipes.Autosubst_lib.ARS]
eval_nf [definition, in Recipes_neutralization.Recipes_NF]
eval_ty [lemma, in Recipes_neutralization.Recipes_NF]
eval_red [lemma, in Recipes_neutralization.Recipes_NF]
eval_nf_sound [lemma, in Recipes_neutralization.Recipes_NF]
eval_sound [lemma, in Recipes_neutralization.Recipes_NF]
eval0 [definition, in Recipes_neutralization.Recipes_NF]
F
FAll [constructor, in Recipes_neutralization.Recipes]FAnd [constructor, in Recipes_neutralization.Recipes]
FEqu [constructor, in Recipes_neutralization.Recipes]
fmla [inductive, in Recipes_neutralization.Recipes]
fmla_eq_dec [lemma, in Recipes_neutralization.Recipes]
fmla_sind [definition, in Recipes_neutralization.Recipes]
fmla_rec [definition, in Recipes_neutralization.Recipes]
fmla_ind [definition, in Recipes_neutralization.Recipes]
fmla_rect [definition, in Recipes_neutralization.Recipes]
FNot [constructor, in Recipes_neutralization.Recipes]
FOr [constructor, in Recipes_neutralization.Recipes]
FPottierIdeas [section, in Recipes_neutralization.My_autosubst]
free_above_n [lemma, in Recipes_neutralization.My_autosubst]
free_above_n_t_old [lemma, in Recipes_neutralization.My_autosubst]
free_above_n_t [lemma, in Recipes_neutralization.My_autosubst]
fv [definition, in Recipes_neutralization.My_autosubst]
fvt_to_fvt_old [lemma, in Recipes_neutralization.My_autosubst]
fv_hsubst_upto_ge_term [lemma, in Recipes_neutralization.My_autosubst]
fv_hsubst_upto_ge [lemma, in Recipes_neutralization.My_autosubst]
fv_hsubst_to_fv_hsubst_old [lemma, in Recipes_neutralization.My_autosubst]
fv_to_fv_old [lemma, in Recipes_neutralization.My_autosubst]
fv_hsubst_old [definition, in Recipes_neutralization.My_autosubst]
fv_t_old [definition, in Recipes_neutralization.My_autosubst]
fv_old [definition, in Recipes_neutralization.My_autosubst]
fv_hsubst [definition, in Recipes_neutralization.My_autosubst]
fv_t [definition, in Recipes_neutralization.My_autosubst]
G
generalize_fv_hsubst [lemma, in Recipes_neutralization.My_autosubst]generalize_fv_subst_term [lemma, in Recipes_neutralization.My_autosubst]
H
has_type_sind [definition, in Recipes_neutralization.Recipes]has_type_ind [definition, in Recipes_neutralization.Recipes]
has_type [inductive, in Recipes_neutralization.Recipes]
HSubstLemmas_reci_term [instance, in Recipes_neutralization.Recipes]
HSubstLemmas_term_reci [instance, in Recipes_neutralization.Recipes]
HSubst_reci_term [instance, in Recipes_neutralization.Recipes]
HSubst_t_reci [instance, in Recipes_neutralization.Recipes]
HSubst_t_fmla [instance, in Recipes_neutralization.Recipes]
I
Ids_reci [instance, in Recipes_neutralization.Recipes]Ids_term [instance, in Recipes_neutralization.Recipes]
Imp [constructor, in Recipes_neutralization.Recipes]
imp_expansion [lemma, in Recipes_neutralization.Recipes_SN]
invplusES [lemma, in Recipes.Autosubst_lib.ARS]
invstarES [lemma, in Recipes.Autosubst_lib.ARS]
inv_nf_hsubst [lemma, in Recipes_neutralization.Recipes_step_lemmas]
inv_star_hsubst [lemma, in Recipes_neutralization.Recipes_step_lemmas]
inv_step_hsubst [lemma, in Recipes_neutralization.Recipes_step_lemmas]
inv_tlam_hsubst [lemma, in Recipes_neutralization.Recipes_step_lemmas]
inv_lam_hsubst [lemma, in Recipes_neutralization.Recipes_step_lemmas]
iterate_iterate [lemma, in Recipes_neutralization.My_autosubst]
iter_succ_rw [lemma, in Recipes_neutralization.Recipes_NF]
J
joinable [definition, in Recipes.Autosubst_lib.ARS]join_conv [lemma, in Recipes.Autosubst_lib.ARS]
L
Lam [constructor, in Recipes_neutralization.Recipes]M
MMapExt_fun [instance, in Recipes.Autosubst_lib.AutosubstSsr]mmapExt_seq [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMapExt_pair [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMapExt_option [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances [section, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.A [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.B [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.C [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapExt_A_C [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapExt_A_B [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapLemmas_A_C [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapLemmas_A_B [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMap_A_C [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMap_A_B [variable, in Recipes.Autosubst_lib.AutosubstSsr]
MMapLemmas_fun [instance, in Recipes.Autosubst_lib.AutosubstSsr]
mmapLemmas_seq [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMapLemmas_pair [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMapLemmas_option [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMap_fun [instance, in Recipes.Autosubst_lib.AutosubstSsr]
mmap_seq [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMap_pair [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MMap_option [instance, in Recipes.Autosubst_lib.AutosubstSsr]
MyComputationN [section, in Recipes_neutralization.Recipes_NF]
MyLemmas [section, in Recipes_neutralization.My_autosubst]
my_evaln [definition, in Recipes_neutralization.Recipes_NF]
my_evaln2 [lemma, in Recipes_neutralization.Recipes_NF]
my_accn_inv [lemma, in Recipes_neutralization.Recipes_NF]
my_accn_sind [definition, in Recipes_neutralization.Recipes_NF]
my_accn_ind [definition, in Recipes_neutralization.Recipes_NF]
my_accn [inductive, in Recipes_neutralization.Recipes_NF]
my_nf [definition, in Recipes_neutralization.Recipes_NF]
My_tactics [library]
My_autosubst [library]
N
NEU [definition, in Recipes_neutralization.Recipes_neutralization]neu [definition, in Recipes_neutralization.Recipes]
neuneu [axiom, in Recipes_neutralization.Recipes_neutralization]
neutral [definition, in Recipes_neutralization.Recipes_neutralization]
Neutralization [section, in Recipes_neutralization.Recipes]
neutralization_soundness [lemma, in Recipes_neutralization.Recipes_neutralization]
neutralize_comm_subst_corr_hsubst [lemma, in Recipes_neutralization.Recipes]
neutralize_comm_subst_corr3 [lemma, in Recipes_neutralization.Recipes]
neutralize_comm_subst_corr2 [lemma, in Recipes_neutralization.Recipes]
neutralize_comm_subst_corr [lemma, in Recipes_neutralization.Recipes]
neutralize_comm_subst [lemma, in Recipes_neutralization.Recipes]
neutral_hsubst_ax [axiom, in Recipes_neutralization.Recipes_neutralization]
neutral_ax_tall [axiom, in Recipes_neutralization.Recipes_neutralization]
neutral_ax_imp [axiom, in Recipes_neutralization.Recipes_neutralization]
neutral_ax_and [axiom, in Recipes_neutralization.Recipes_neutralization]
neutral_ax [axiom, in Recipes_neutralization.Recipes_neutralization]
neutral_hsubst [lemma, in Recipes_neutralization.Recipes_neutralization]
neu_hsubst [lemma, in Recipes_neutralization.Recipes_neutralization]
neu_idempotent_upn [lemma, in Recipes_neutralization.Recipes]
neu_idempotent [lemma, in Recipes_neutralization.Recipes]
NEUσ [definition, in Recipes_neutralization.Recipes_neutralization]
nf [definition, in Recipes.Autosubst_lib.ARS]
nf_neu_2 [lemma, in Recipes_neutralization.Recipes_neutralization]
nf_neu_1 [lemma, in Recipes_neutralization.Recipes_neutralization]
nf_neu [lemma, in Recipes_neutralization.Recipes_neutralization]
nf_accn [lemma, in Recipes_neutralization.Recipes_NF]
nf_nf_2 [lemma, in Recipes_neutralization.Recipes_NF]
nf_nf [lemma, in Recipes_neutralization.Recipes_NF]
nf_var_is_var [lemma, in Recipes_neutralization.Recipes_step_lemmas]
nf_top_is_top [lemma, in Recipes_neutralization.Recipes_step_lemmas]
nf_accn [lemma, in Recipes.Autosubst_lib.ARS]
normal [definition, in Recipes.Autosubst_lib.ARS]
normalizing [definition, in Recipes.Autosubst_lib.ARS]
normall [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_rho_id [lemma, in Recipes_neutralization.Recipes_NF]
normal_hsubst [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_tapp [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_lam [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_tlam [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_var [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_top [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_no_step [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normal_star [lemma, in Recipes.Autosubst_lib.ARS]
normande [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normapp [lemma, in Recipes_neutralization.Recipes_step_lemmas]
normimp [lemma, in Recipes_neutralization.Recipes_step_lemmas]
norm_step [lemma, in Recipes_neutralization.Recipes_NF]
not_mynf_then_reducible [lemma, in Recipes_neutralization.Recipes_NF]
ns [definition, in Recipes_neutralization.Recipes]
P
path [projection, in Recipes_neutralization.Recipes_NF]plus [inductive, in Recipes.Autosubst_lib.ARS]
plusES [lemma, in Recipes.Autosubst_lib.ARS]
plusSE [constructor, in Recipes.Autosubst_lib.ARS]
plus_s_rho_s [lemma, in Recipes_neutralization.Recipes_NF]
plus_tall [lemma, in Recipes_neutralization.Recipes_NF]
plus_tlam [lemma, in Recipes_neutralization.Recipes_NF]
plus_lam [lemma, in Recipes_neutralization.Recipes_NF]
plus_imp [lemma, in Recipes_neutralization.Recipes_NF]
plus_tapp [lemma, in Recipes_neutralization.Recipes_NF]
plus_appr [lemma, in Recipes_neutralization.Recipes_NF]
plus_appl [lemma, in Recipes_neutralization.Recipes_NF]
plus_app [lemma, in Recipes_neutralization.Recipes_NF]
plus_andr [lemma, in Recipes_neutralization.Recipes_NF]
plus_andl [lemma, in Recipes_neutralization.Recipes_NF]
plus_and [lemma, in Recipes_neutralization.Recipes_NF]
Plus_lemmas [section, in Recipes_neutralization.Recipes_NF]
plus_hom [lemma, in Recipes.Autosubst_lib.ARS]
plus_img [lemma, in Recipes.Autosubst_lib.ARS]
plus_trans [lemma, in Recipes.Autosubst_lib.ARS]
plus_trans_star [lemma, in Recipes.Autosubst_lib.ARS]
plus_sind [definition, in Recipes.Autosubst_lib.ARS]
plus_ind [definition, in Recipes.Autosubst_lib.ARS]
plus1 [lemma, in Recipes.Autosubst_lib.ARS]
plus2star [lemma, in Recipes.Autosubst_lib.ARS]
ppets [definition, in Recipes_neutralization.Recipes_NF]
Pred [definition, in Recipes.Autosubst_lib.ARS]
psstep [definition, in Recipes_neutralization.Recipes]
psstep_hsubst [lemma, in Recipes_neutralization.Recipes]
psstep_up [lemma, in Recipes_neutralization.Recipes]
pstep [inductive, in Recipes_neutralization.Recipes]
pstep_compat_beta [lemma, in Recipes_neutralization.Recipes]
pstep_compat_beta0 [lemma, in Recipes_neutralization.Recipes]
pstep_compat_tbeta [lemma, in Recipes_neutralization.Recipes]
pstep_compat [lemma, in Recipes_neutralization.Recipes]
pstep_subst [lemma, in Recipes_neutralization.Recipes]
pstep_substf [lemma, in Recipes_neutralization.Recipes]
pstep_red [lemma, in Recipes_neutralization.Recipes]
pstep_refl [lemma, in Recipes_neutralization.Recipes]
pstep_sind [definition, in Recipes_neutralization.Recipes]
pstep_ind [definition, in Recipes_neutralization.Recipes]
pstep_and [constructor, in Recipes_neutralization.Recipes]
pstep_app [constructor, in Recipes_neutralization.Recipes]
pstep_tapp [constructor, in Recipes_neutralization.Recipes]
pstep_tall [constructor, in Recipes_neutralization.Recipes]
pstep_imp [constructor, in Recipes_neutralization.Recipes]
pstep_tlam [constructor, in Recipes_neutralization.Recipes]
pstep_lam [constructor, in Recipes_neutralization.Recipes]
pstep_tbeta [constructor, in Recipes_neutralization.Recipes]
pstep_beta [constructor, in Recipes_neutralization.Recipes]
pstep_top [constructor, in Recipes_neutralization.Recipes]
pstep_var [constructor, in Recipes_neutralization.Recipes]
p_nc [projection, in Recipes_neutralization.Recipes_SN]
p_cl [projection, in Recipes_neutralization.Recipes_SN]
p_sn [projection, in Recipes_neutralization.Recipes_SN]
R
recipe [inductive, in Recipes_neutralization.Recipes]Recipes [library]
Recipes_NF [library]
Recipes_step_lemmas [library]
Recipes_neutralization [library]
Recipes_SN [library]
recipe_tlam_dec [lemma, in Recipes_neutralization.Recipes_NF]
recipe_lam_dec [lemma, in Recipes_neutralization.Recipes_NF]
recipe_var_dec [lemma, in Recipes_neutralization.Recipes_NF]
recipe_not_tlam [lemma, in Recipes_neutralization.Recipes_NF]
recipe_not_lam [lemma, in Recipes_neutralization.Recipes_NF]
recipe_eq_dec [lemma, in Recipes_neutralization.Recipes]
recipe_sind [definition, in Recipes_neutralization.Recipes]
recipe_rec [definition, in Recipes_neutralization.Recipes]
recipe_ind [definition, in Recipes_neutralization.Recipes]
recipe_rect [definition, in Recipes_neutralization.Recipes]
RED [definition, in Recipes_neutralization.Recipes_SN]
red [definition, in Recipes_neutralization.Recipes]
reducible [record, in Recipes_neutralization.Recipes_SN]
reducible [definition, in Recipes.Autosubst_lib.ARS]
reducible_var [lemma, in Recipes_neutralization.Recipes_SN]
reducible_sn [lemma, in Recipes_neutralization.Recipes_SN]
RED_cl_star [lemma, in Recipes_neutralization.Recipes_SN]
RED_var [lemma, in Recipes_neutralization.Recipes_SN]
RED_nc [lemma, in Recipes_neutralization.Recipes_SN]
RED_cl [lemma, in Recipes_neutralization.Recipes_SN]
RED_sn [lemma, in Recipes_neutralization.Recipes_SN]
red_reducible [lemma, in Recipes_neutralization.Recipes_SN]
red_beta01 [lemma, in Recipes_neutralization.Recipes]
red_beta [lemma, in Recipes_neutralization.Recipes]
red_compat [lemma, in Recipes_neutralization.Recipes]
red_hsubst [lemma, in Recipes_neutralization.Recipes]
red_subst [lemma, in Recipes_neutralization.Recipes]
red_tall [lemma, in Recipes_neutralization.Recipes]
red_tlam [lemma, in Recipes_neutralization.Recipes]
red_lam [lemma, in Recipes_neutralization.Recipes]
red_imp [lemma, in Recipes_neutralization.Recipes]
red_tapp [lemma, in Recipes_neutralization.Recipes]
red_and [lemma, in Recipes_neutralization.Recipes]
red_app [lemma, in Recipes_neutralization.Recipes]
red_top [lemma, in Recipes_neutralization.Recipes]
red_tall_inv [lemma, in Recipes_neutralization.Recipes_step_lemmas]
red_imp_inv [lemma, in Recipes_neutralization.Recipes_step_lemmas]
red_and_inv [lemma, in Recipes_neutralization.Recipes_step_lemmas]
REDσ [definition, in Recipes_neutralization.Recipes_SN]
Rel [definition, in Recipes.Autosubst_lib.ARS]
Rename_reci [instance, in Recipes_neutralization.Recipes]
Rename_flma [instance, in Recipes_neutralization.Recipes]
Rename_term [instance, in Recipes_neutralization.Recipes]
rho [definition, in Recipes_neutralization.Recipes_NF]
rho [definition, in Recipes_neutralization.Recipes]
rho_len [projection, in Recipes_neutralization.Recipes_NF]
rho_wt [definition, in Recipes_neutralization.Recipes_NF]
rho_triangle [lemma, in Recipes_neutralization.Recipes]
RNF [record, in Recipes_neutralization.Recipes_NF]
S
simple [definition, in Recipes_neutralization.Recipes_SN]sn [inductive, in Recipes.Autosubst_lib.ARS]
sneu [definition, in Recipes_neutralization.Recipes]
sneu_idempotent [lemma, in Recipes_neutralization.Recipes_SN]
SNI [constructor, in Recipes.Autosubst_lib.ARS]
sn_wn [lemma, in Recipes_neutralization.Recipes_NF]
sn_is_acc [lemma, in Recipes_neutralization.Recipes_NF]
sn_hsubst [lemma, in Recipes_neutralization.Recipes_SN]
sn_subst [lemma, in Recipes_neutralization.Recipes_SN]
sn_tclosed [lemma, in Recipes_neutralization.Recipes_SN]
sn_closed [lemma, in Recipes_neutralization.Recipes_SN]
sn_eq_nsn_if_odd [lemma, in Recipes_neutralization.Recipes]
sn_wn [lemma, in Recipes.Autosubst_lib.ARS]
sn_preimage [lemma, in Recipes.Autosubst_lib.ARS]
sn_sind [definition, in Recipes.Autosubst_lib.ARS]
sn_rec [definition, in Recipes.Autosubst_lib.ARS]
sn_ind [definition, in Recipes.Autosubst_lib.ARS]
sn_rect [definition, in Recipes.Autosubst_lib.ARS]
soundness [lemma, in Recipes_neutralization.Recipes_SN]
sound_step_n [lemma, in Recipes_neutralization.Recipes_NF]
sound_step [lemma, in Recipes_neutralization.Recipes_NF]
sred [definition, in Recipes_neutralization.Recipes]
sred_hup [lemma, in Recipes_neutralization.Recipes]
sred_up [lemma, in Recipes_neutralization.Recipes]
star [inductive, in Recipes.Autosubst_lib.ARS]
starES [lemma, in Recipes.Autosubst_lib.ARS]
starR [constructor, in Recipes.Autosubst_lib.ARS]
starSE [constructor, in Recipes.Autosubst_lib.ARS]
StarStep [section, in Recipes_neutralization.Recipes]
StarStep.ChurchRosser [section, in Recipes_neutralization.Recipes]
_ ===>> _ [notation, in Recipes_neutralization.Recipes]
star_interpolation [lemma, in Recipes.Autosubst_lib.ARS]
star_monotone [lemma, in Recipes.Autosubst_lib.ARS]
star_closure [lemma, in Recipes.Autosubst_lib.ARS]
star_hom [lemma, in Recipes.Autosubst_lib.ARS]
star_img [lemma, in Recipes.Autosubst_lib.ARS]
star_conv [lemma, in Recipes.Autosubst_lib.ARS]
star_trans [lemma, in Recipes.Autosubst_lib.ARS]
star_sind [definition, in Recipes.Autosubst_lib.ARS]
star_ind [definition, in Recipes.Autosubst_lib.ARS]
star1 [lemma, in Recipes.Autosubst_lib.ARS]
star2plus [lemma, in Recipes.Autosubst_lib.ARS]
step [inductive, in Recipes_neutralization.Recipes]
Step [section, in Recipes_neutralization.Recipes]
step_neu_2 [lemma, in Recipes_neutralization.Recipes_neutralization]
step_neu_1 [lemma, in Recipes_neutralization.Recipes_neutralization]
step_neu [lemma, in Recipes_neutralization.Recipes_neutralization]
step_anti_refl [lemma, in Recipes_neutralization.Recipes_SN]
step_pstep [lemma, in Recipes_neutralization.Recipes]
step_hsubst [lemma, in Recipes_neutralization.Recipes]
step_subst [lemma, in Recipes_neutralization.Recipes]
step_substf [lemma, in Recipes_neutralization.Recipes]
step_sind [definition, in Recipes_neutralization.Recipes]
step_ind [definition, in Recipes_neutralization.Recipes]
step_ctx_tall [constructor, in Recipes_neutralization.Recipes]
step_ctx_tlam [constructor, in Recipes_neutralization.Recipes]
step_ctx_imp [constructor, in Recipes_neutralization.Recipes]
step_ctx_lam [constructor, in Recipes_neutralization.Recipes]
step_ctx_tapp [constructor, in Recipes_neutralization.Recipes]
step_ctx_appr [constructor, in Recipes_neutralization.Recipes]
step_ctx_appl [constructor, in Recipes_neutralization.Recipes]
step_ctx_andr [constructor, in Recipes_neutralization.Recipes]
step_ctx_andl [constructor, in Recipes_neutralization.Recipes]
step_tbeta [constructor, in Recipes_neutralization.Recipes]
step_beta [constructor, in Recipes_neutralization.Recipes]
_ ===> _ [notation, in Recipes_neutralization.Recipes]
strong_normalization_plus [lemma, in Recipes_neutralization.Recipes_SN]
strong_normalization [lemma, in Recipes_neutralization.Recipes_SN]
subject_reduction_red [lemma, in Recipes_neutralization.Recipes]
subject_reduction [lemma, in Recipes_neutralization.Recipes]
SubstHSubstComp_term_reci [instance, in Recipes_neutralization.Recipes]
SubstHSubstComp_reci_term [instance, in Recipes_neutralization.Recipes]
SubstLemmasP [section, in Recipes_neutralization.Recipes]
SubstLemmas_reci [instance, in Recipes_neutralization.Recipes]
SubstLemmas_term [instance, in Recipes_neutralization.Recipes]
Subst_reci [instance, in Recipes_neutralization.Recipes]
Subst_fmla [instance, in Recipes_neutralization.Recipes]
Subst_term [instance, in Recipes_neutralization.Recipes]
T
TAll [constructor, in Recipes_neutralization.Recipes]tall_expansion [lemma, in Recipes_neutralization.Recipes_SN]
TApp [constructor, in Recipes_neutralization.Recipes]
TArr [constructor, in Recipes_neutralization.Recipes]
tbeta_expansion [lemma, in Recipes_neutralization.Recipes_SN]
TCons [constructor, in Recipes_neutralization.Recipes]
term [inductive, in Recipes_neutralization.Recipes]
Termination [section, in Recipes.Autosubst_lib.ARS]
Termination.cr [variable, in Recipes.Autosubst_lib.ARS]
Termination.e [variable, in Recipes.Autosubst_lib.ARS]
Termination.T [variable, in Recipes.Autosubst_lib.ARS]
term_eq_dec [lemma, in Recipes_neutralization.Recipes]
term_sind [definition, in Recipes_neutralization.Recipes]
term_rec [definition, in Recipes_neutralization.Recipes]
term_ind [definition, in Recipes_neutralization.Recipes]
term_rect [definition, in Recipes_neutralization.Recipes]
TLam [constructor, in Recipes_neutralization.Recipes]
TNat [constructor, in Recipes_neutralization.Recipes]
Top [constructor, in Recipes_neutralization.Recipes]
triangle [definition, in Recipes.Autosubst_lib.ARS]
triangle_cofinal [lemma, in Recipes.Autosubst_lib.ARS]
triangle_monotone [lemma, in Recipes.Autosubst_lib.ARS]
triangle_diamond [lemma, in Recipes.Autosubst_lib.ARS]
TVar [constructor, in Recipes_neutralization.Recipes]
type [inductive, in Recipes_neutralization.Recipes]
type_L [lemma, in Recipes_neutralization.Recipes_SN]
type_eq_dec [lemma, in Recipes_neutralization.Recipes]
type_sind [definition, in Recipes_neutralization.Recipes]
type_rec [definition, in Recipes_neutralization.Recipes]
type_ind [definition, in Recipes_neutralization.Recipes]
type_rect [definition, in Recipes_neutralization.Recipes]
TypingDefinitions [section, in Recipes_neutralization.Recipes]
[ _ ⊢ _ :- _ ] [notation, in Recipes_neutralization.Recipes]
TypingLemmas [section, in Recipes_neutralization.Recipes]
TypingLemmas.SubjectReduction [section, in Recipes_neutralization.Recipes]
ty_neu [lemma, in Recipes_neutralization.Recipes]
ty_neu_m [lemma, in Recipes_neutralization.Recipes]
ty_subst [lemma, in Recipes_neutralization.Recipes]
ty_hsubst [lemma, in Recipes_neutralization.Recipes]
ty_weak2 [lemma, in Recipes_neutralization.Recipes]
ty_weak [lemma, in Recipes_neutralization.Recipes]
ty_ren [lemma, in Recipes_neutralization.Recipes]
ty_tapp [constructor, in Recipes_neutralization.Recipes]
ty_app [constructor, in Recipes_neutralization.Recipes]
ty_lam [constructor, in Recipes_neutralization.Recipes]
ty_and [constructor, in Recipes_neutralization.Recipes]
ty_imp [constructor, in Recipes_neutralization.Recipes]
ty_var [constructor, in Recipes_neutralization.Recipes]
ty_tlam [constructor, in Recipes_neutralization.Recipes]
ty_tall [constructor, in Recipes_neutralization.Recipes]
ty_top [constructor, in Recipes_neutralization.Recipes]
U
unique_nf_starstep [lemma, in Recipes_neutralization.Recipes_step_lemmas]unique_nf_step [lemma, in Recipes_neutralization.Recipes_step_lemmas]
unique_nf_antistarstep [lemma, in Recipes_neutralization.Recipes_step_lemmas]
unique_nf_antistep [lemma, in Recipes_neutralization.Recipes_step_lemmas]
upnP [lemma, in Recipes_neutralization.Recipes]
upnPh [lemma, in Recipes_neutralization.Recipes]
upnP_cond [lemma, in Recipes_neutralization.Recipes]
upn_upn_t [lemma, in Recipes_neutralization.My_autosubst]
upn_upn [lemma, in Recipes_neutralization.My_autosubst]
upn2P [lemma, in Recipes_neutralization.Recipes]
V
Var [constructor, in Recipes_neutralization.Recipes]var_eq_dec [lemma, in Recipes_neutralization.Recipes]
Void [constructor, in Recipes_neutralization.Recipes]
W
wf_ext [lemma, in Recipes_neutralization.Recipes]wf_subst_neu [lemma, in Recipes_neutralization.Recipes]
wf_subst [definition, in Recipes_neutralization.Recipes]
wf_ctx [definition, in Recipes_neutralization.Recipes]
wn [definition, in Recipes.Autosubst_lib.ARS]
wn_accn [lemma, in Recipes_neutralization.Recipes_NF]
wn_accn [lemma, in Recipes.Autosubst_lib.ARS]
wt_acc_plus [lemma, in Recipes_neutralization.Recipes_NF]
wt2nf_sig [definition, in Recipes_neutralization.Recipes_NF]
wt2nf_ex [lemma, in Recipes_neutralization.Recipes_NF]
other
_ <=>2 _ (prop_scope) [notation, in Recipes.Autosubst_lib.ARS]_ <=2 _ (prop_scope) [notation, in Recipes.Autosubst_lib.ARS]
[ _ ⊢ _ ] [notation, in Recipes_neutralization.Recipes]
[ _ ⊢ ] [notation, in Recipes_neutralization.Recipes]
[ _ ⊢ _ :- _ ] [notation, in Recipes_neutralization.Recipes]
Notation Index
S
_ ===>> _ [in Recipes_neutralization.Recipes]_ ===> _ [in Recipes_neutralization.Recipes]
T
[ _ ⊢ _ :- _ ] [in Recipes_neutralization.Recipes]other
_ <=>2 _ (prop_scope) [in Recipes.Autosubst_lib.ARS]_ <=2 _ (prop_scope) [in Recipes.Autosubst_lib.ARS]
[ _ ⊢ _ ] [in Recipes_neutralization.Recipes]
[ _ ⊢ ] [in Recipes_neutralization.Recipes]
[ _ ⊢ _ :- _ ] [in Recipes_neutralization.Recipes]
Variable Index
C
CoFinal.e [in Recipes.Autosubst_lib.ARS]CoFinal.rho [in Recipes.Autosubst_lib.ARS]
CoFinal.T [in Recipes.Autosubst_lib.ARS]
CoFinal.tri [in Recipes.Autosubst_lib.ARS]
Commutation.T [in Recipes.Autosubst_lib.ARS]
ComputationN.classical [in Recipes.Autosubst_lib.ARS]
ComputationN.e [in Recipes.Autosubst_lib.ARS]
ComputationN.norm [in Recipes.Autosubst_lib.ARS]
ComputationN.rho [in Recipes.Autosubst_lib.ARS]
ComputationN.sound [in Recipes.Autosubst_lib.ARS]
ComputationN.T [in Recipes.Autosubst_lib.ARS]
D
Definitions.e [in Recipes.Autosubst_lib.ARS]Definitions.T [in Recipes.Autosubst_lib.ARS]
M
MMapInstances.A [in Recipes.Autosubst_lib.AutosubstSsr]MMapInstances.B [in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.C [in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapExt_A_C [in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapExt_A_B [in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapLemmas_A_C [in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMapLemmas_A_B [in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMap_A_C [in Recipes.Autosubst_lib.AutosubstSsr]
MMapInstances.MMap_A_B [in Recipes.Autosubst_lib.AutosubstSsr]
T
Termination.cr [in Recipes.Autosubst_lib.ARS]Termination.e [in Recipes.Autosubst_lib.ARS]
Termination.T [in Recipes.Autosubst_lib.ARS]
Library Index
A
ARSAutosubstSsr
M
My_tacticsMy_autosubst
R
RecipesRecipes_NF
Recipes_step_lemmas
Recipes_neutralization
Recipes_SN
Lemma Index
A
accn_inv [in Recipes.Autosubst_lib.ARS]acc_if_wt [in Recipes_neutralization.Recipes_NF]
admissible_compose [in Recipes_neutralization.Recipes]
admissible_hsubst [in Recipes_neutralization.Recipes]
admissible_subst_up2 [in Recipes_neutralization.Recipes]
admissible_subst_var01 [in Recipes_neutralization.Recipes]
admissible_subst_ext [in Recipes_neutralization.Recipes]
admissible_ids [in Recipes_neutralization.Recipes]
admissible_neu [in Recipes_neutralization.Recipes]
admissible_subst_rw [in Recipes_neutralization.Recipes]
and_expansion [in Recipes_neutralization.Recipes_SN]
B
beta_expansion [in Recipes_neutralization.Recipes_SN]C
choose_last_n_hsubst [in Recipes_neutralization.My_autosubst]choose_last_n_subst [in Recipes_neutralization.My_autosubst]
church_rosser [in Recipes_neutralization.Recipes]
classical_step [in Recipes_neutralization.Recipes_NF]
closed_subst [in Recipes_neutralization.My_autosubst]
cofinal_normalizing [in Recipes.Autosubst_lib.ARS]
com_lift [in Recipes.Autosubst_lib.ARS]
com_strip [in Recipes.Autosubst_lib.ARS]
confluence [in Recipes_neutralization.Recipes]
confluent_stable [in Recipes.Autosubst_lib.ARS]
confluent_cr [in Recipes.Autosubst_lib.ARS]
convES [in Recipes.Autosubst_lib.ARS]
convESi [in Recipes.Autosubst_lib.ARS]
conv_neu [in Recipes_neutralization.Recipes_neutralization]
conv_closure [in Recipes.Autosubst_lib.ARS]
conv_hom [in Recipes.Autosubst_lib.ARS]
conv_img [in Recipes.Autosubst_lib.ARS]
conv_sym [in Recipes.Autosubst_lib.ARS]
conv_trans [in Recipes.Autosubst_lib.ARS]
conv1 [in Recipes.Autosubst_lib.ARS]
conv1i [in Recipes.Autosubst_lib.ARS]
cr_method [in Recipes.Autosubst_lib.ARS]
cr_conv_normal [in Recipes.Autosubst_lib.ARS]
cr_star_normal [in Recipes.Autosubst_lib.ARS]
D
diamond_confluent [in Recipes.Autosubst_lib.ARS]E
eq_star [in Recipes.Autosubst_lib.ARS]evalnP [in Recipes_neutralization.Recipes_NF]
evalnP [in Recipes.Autosubst_lib.ARS]
evaln_sound [in Recipes_neutralization.Recipes_NF]
evaln_sound [in Recipes.Autosubst_lib.ARS]
eval_ty [in Recipes_neutralization.Recipes_NF]
eval_red [in Recipes_neutralization.Recipes_NF]
eval_nf_sound [in Recipes_neutralization.Recipes_NF]
eval_sound [in Recipes_neutralization.Recipes_NF]
F
fmla_eq_dec [in Recipes_neutralization.Recipes]free_above_n [in Recipes_neutralization.My_autosubst]
free_above_n_t_old [in Recipes_neutralization.My_autosubst]
free_above_n_t [in Recipes_neutralization.My_autosubst]
fvt_to_fvt_old [in Recipes_neutralization.My_autosubst]
fv_hsubst_upto_ge_term [in Recipes_neutralization.My_autosubst]
fv_hsubst_upto_ge [in Recipes_neutralization.My_autosubst]
fv_hsubst_to_fv_hsubst_old [in Recipes_neutralization.My_autosubst]
fv_to_fv_old [in Recipes_neutralization.My_autosubst]
G
generalize_fv_hsubst [in Recipes_neutralization.My_autosubst]generalize_fv_subst_term [in Recipes_neutralization.My_autosubst]
I
imp_expansion [in Recipes_neutralization.Recipes_SN]invplusES [in Recipes.Autosubst_lib.ARS]
invstarES [in Recipes.Autosubst_lib.ARS]
inv_nf_hsubst [in Recipes_neutralization.Recipes_step_lemmas]
inv_star_hsubst [in Recipes_neutralization.Recipes_step_lemmas]
inv_step_hsubst [in Recipes_neutralization.Recipes_step_lemmas]
inv_tlam_hsubst [in Recipes_neutralization.Recipes_step_lemmas]
inv_lam_hsubst [in Recipes_neutralization.Recipes_step_lemmas]
iterate_iterate [in Recipes_neutralization.My_autosubst]
iter_succ_rw [in Recipes_neutralization.Recipes_NF]
J
join_conv [in Recipes.Autosubst_lib.ARS]M
my_evaln2 [in Recipes_neutralization.Recipes_NF]my_accn_inv [in Recipes_neutralization.Recipes_NF]
N
neutralization_soundness [in Recipes_neutralization.Recipes_neutralization]neutralize_comm_subst_corr_hsubst [in Recipes_neutralization.Recipes]
neutralize_comm_subst_corr3 [in Recipes_neutralization.Recipes]
neutralize_comm_subst_corr2 [in Recipes_neutralization.Recipes]
neutralize_comm_subst_corr [in Recipes_neutralization.Recipes]
neutralize_comm_subst [in Recipes_neutralization.Recipes]
neutral_hsubst [in Recipes_neutralization.Recipes_neutralization]
neu_hsubst [in Recipes_neutralization.Recipes_neutralization]
neu_idempotent_upn [in Recipes_neutralization.Recipes]
neu_idempotent [in Recipes_neutralization.Recipes]
nf_neu_2 [in Recipes_neutralization.Recipes_neutralization]
nf_neu_1 [in Recipes_neutralization.Recipes_neutralization]
nf_neu [in Recipes_neutralization.Recipes_neutralization]
nf_accn [in Recipes_neutralization.Recipes_NF]
nf_nf_2 [in Recipes_neutralization.Recipes_NF]
nf_nf [in Recipes_neutralization.Recipes_NF]
nf_var_is_var [in Recipes_neutralization.Recipes_step_lemmas]
nf_top_is_top [in Recipes_neutralization.Recipes_step_lemmas]
nf_accn [in Recipes.Autosubst_lib.ARS]
normall [in Recipes_neutralization.Recipes_step_lemmas]
normal_rho_id [in Recipes_neutralization.Recipes_NF]
normal_hsubst [in Recipes_neutralization.Recipes_step_lemmas]
normal_tapp [in Recipes_neutralization.Recipes_step_lemmas]
normal_lam [in Recipes_neutralization.Recipes_step_lemmas]
normal_tlam [in Recipes_neutralization.Recipes_step_lemmas]
normal_var [in Recipes_neutralization.Recipes_step_lemmas]
normal_top [in Recipes_neutralization.Recipes_step_lemmas]
normal_no_step [in Recipes_neutralization.Recipes_step_lemmas]
normal_star [in Recipes.Autosubst_lib.ARS]
normande [in Recipes_neutralization.Recipes_step_lemmas]
normapp [in Recipes_neutralization.Recipes_step_lemmas]
normimp [in Recipes_neutralization.Recipes_step_lemmas]
norm_step [in Recipes_neutralization.Recipes_NF]
not_mynf_then_reducible [in Recipes_neutralization.Recipes_NF]
P
plusES [in Recipes.Autosubst_lib.ARS]plus_s_rho_s [in Recipes_neutralization.Recipes_NF]
plus_tall [in Recipes_neutralization.Recipes_NF]
plus_tlam [in Recipes_neutralization.Recipes_NF]
plus_lam [in Recipes_neutralization.Recipes_NF]
plus_imp [in Recipes_neutralization.Recipes_NF]
plus_tapp [in Recipes_neutralization.Recipes_NF]
plus_appr [in Recipes_neutralization.Recipes_NF]
plus_appl [in Recipes_neutralization.Recipes_NF]
plus_app [in Recipes_neutralization.Recipes_NF]
plus_andr [in Recipes_neutralization.Recipes_NF]
plus_andl [in Recipes_neutralization.Recipes_NF]
plus_and [in Recipes_neutralization.Recipes_NF]
plus_hom [in Recipes.Autosubst_lib.ARS]
plus_img [in Recipes.Autosubst_lib.ARS]
plus_trans [in Recipes.Autosubst_lib.ARS]
plus_trans_star [in Recipes.Autosubst_lib.ARS]
plus1 [in Recipes.Autosubst_lib.ARS]
plus2star [in Recipes.Autosubst_lib.ARS]
psstep_hsubst [in Recipes_neutralization.Recipes]
psstep_up [in Recipes_neutralization.Recipes]
pstep_compat_beta [in Recipes_neutralization.Recipes]
pstep_compat_beta0 [in Recipes_neutralization.Recipes]
pstep_compat_tbeta [in Recipes_neutralization.Recipes]
pstep_compat [in Recipes_neutralization.Recipes]
pstep_subst [in Recipes_neutralization.Recipes]
pstep_substf [in Recipes_neutralization.Recipes]
pstep_red [in Recipes_neutralization.Recipes]
pstep_refl [in Recipes_neutralization.Recipes]
R
recipe_tlam_dec [in Recipes_neutralization.Recipes_NF]recipe_lam_dec [in Recipes_neutralization.Recipes_NF]
recipe_var_dec [in Recipes_neutralization.Recipes_NF]
recipe_not_tlam [in Recipes_neutralization.Recipes_NF]
recipe_not_lam [in Recipes_neutralization.Recipes_NF]
recipe_eq_dec [in Recipes_neutralization.Recipes]
reducible_var [in Recipes_neutralization.Recipes_SN]
reducible_sn [in Recipes_neutralization.Recipes_SN]
RED_cl_star [in Recipes_neutralization.Recipes_SN]
RED_var [in Recipes_neutralization.Recipes_SN]
RED_nc [in Recipes_neutralization.Recipes_SN]
RED_cl [in Recipes_neutralization.Recipes_SN]
RED_sn [in Recipes_neutralization.Recipes_SN]
red_reducible [in Recipes_neutralization.Recipes_SN]
red_beta01 [in Recipes_neutralization.Recipes]
red_beta [in Recipes_neutralization.Recipes]
red_compat [in Recipes_neutralization.Recipes]
red_hsubst [in Recipes_neutralization.Recipes]
red_subst [in Recipes_neutralization.Recipes]
red_tall [in Recipes_neutralization.Recipes]
red_tlam [in Recipes_neutralization.Recipes]
red_lam [in Recipes_neutralization.Recipes]
red_imp [in Recipes_neutralization.Recipes]
red_tapp [in Recipes_neutralization.Recipes]
red_and [in Recipes_neutralization.Recipes]
red_app [in Recipes_neutralization.Recipes]
red_top [in Recipes_neutralization.Recipes]
red_tall_inv [in Recipes_neutralization.Recipes_step_lemmas]
red_imp_inv [in Recipes_neutralization.Recipes_step_lemmas]
red_and_inv [in Recipes_neutralization.Recipes_step_lemmas]
rho_triangle [in Recipes_neutralization.Recipes]
S
sneu_idempotent [in Recipes_neutralization.Recipes_SN]sn_wn [in Recipes_neutralization.Recipes_NF]
sn_is_acc [in Recipes_neutralization.Recipes_NF]
sn_hsubst [in Recipes_neutralization.Recipes_SN]
sn_subst [in Recipes_neutralization.Recipes_SN]
sn_tclosed [in Recipes_neutralization.Recipes_SN]
sn_closed [in Recipes_neutralization.Recipes_SN]
sn_eq_nsn_if_odd [in Recipes_neutralization.Recipes]
sn_wn [in Recipes.Autosubst_lib.ARS]
sn_preimage [in Recipes.Autosubst_lib.ARS]
soundness [in Recipes_neutralization.Recipes_SN]
sound_step_n [in Recipes_neutralization.Recipes_NF]
sound_step [in Recipes_neutralization.Recipes_NF]
sred_hup [in Recipes_neutralization.Recipes]
sred_up [in Recipes_neutralization.Recipes]
starES [in Recipes.Autosubst_lib.ARS]
star_interpolation [in Recipes.Autosubst_lib.ARS]
star_monotone [in Recipes.Autosubst_lib.ARS]
star_closure [in Recipes.Autosubst_lib.ARS]
star_hom [in Recipes.Autosubst_lib.ARS]
star_img [in Recipes.Autosubst_lib.ARS]
star_conv [in Recipes.Autosubst_lib.ARS]
star_trans [in Recipes.Autosubst_lib.ARS]
star1 [in Recipes.Autosubst_lib.ARS]
star2plus [in Recipes.Autosubst_lib.ARS]
step_neu_2 [in Recipes_neutralization.Recipes_neutralization]
step_neu_1 [in Recipes_neutralization.Recipes_neutralization]
step_neu [in Recipes_neutralization.Recipes_neutralization]
step_anti_refl [in Recipes_neutralization.Recipes_SN]
step_pstep [in Recipes_neutralization.Recipes]
step_hsubst [in Recipes_neutralization.Recipes]
step_subst [in Recipes_neutralization.Recipes]
step_substf [in Recipes_neutralization.Recipes]
strong_normalization_plus [in Recipes_neutralization.Recipes_SN]
strong_normalization [in Recipes_neutralization.Recipes_SN]
subject_reduction_red [in Recipes_neutralization.Recipes]
subject_reduction [in Recipes_neutralization.Recipes]
T
tall_expansion [in Recipes_neutralization.Recipes_SN]tbeta_expansion [in Recipes_neutralization.Recipes_SN]
term_eq_dec [in Recipes_neutralization.Recipes]
triangle_cofinal [in Recipes.Autosubst_lib.ARS]
triangle_monotone [in Recipes.Autosubst_lib.ARS]
triangle_diamond [in Recipes.Autosubst_lib.ARS]
type_L [in Recipes_neutralization.Recipes_SN]
type_eq_dec [in Recipes_neutralization.Recipes]
ty_neu [in Recipes_neutralization.Recipes]
ty_neu_m [in Recipes_neutralization.Recipes]
ty_subst [in Recipes_neutralization.Recipes]
ty_hsubst [in Recipes_neutralization.Recipes]
ty_weak2 [in Recipes_neutralization.Recipes]
ty_weak [in Recipes_neutralization.Recipes]
ty_ren [in Recipes_neutralization.Recipes]
U
unique_nf_starstep [in Recipes_neutralization.Recipes_step_lemmas]unique_nf_step [in Recipes_neutralization.Recipes_step_lemmas]
unique_nf_antistarstep [in Recipes_neutralization.Recipes_step_lemmas]
unique_nf_antistep [in Recipes_neutralization.Recipes_step_lemmas]
upnP [in Recipes_neutralization.Recipes]
upnPh [in Recipes_neutralization.Recipes]
upnP_cond [in Recipes_neutralization.Recipes]
upn_upn_t [in Recipes_neutralization.My_autosubst]
upn_upn [in Recipes_neutralization.My_autosubst]
upn2P [in Recipes_neutralization.Recipes]
V
var_eq_dec [in Recipes_neutralization.Recipes]W
wf_ext [in Recipes_neutralization.Recipes]wf_subst_neu [in Recipes_neutralization.Recipes]
wn_accn [in Recipes_neutralization.Recipes_NF]
wn_accn [in Recipes.Autosubst_lib.ARS]
wt_acc_plus [in Recipes_neutralization.Recipes_NF]
wt2nf_ex [in Recipes_neutralization.Recipes_NF]
Axiom Index
N
neuneu [in Recipes_neutralization.Recipes_neutralization]neutral_hsubst_ax [in Recipes_neutralization.Recipes_neutralization]
neutral_ax_tall [in Recipes_neutralization.Recipes_neutralization]
neutral_ax_imp [in Recipes_neutralization.Recipes_neutralization]
neutral_ax_and [in Recipes_neutralization.Recipes_neutralization]
neutral_ax [in Recipes_neutralization.Recipes_neutralization]
Constructor Index
A
accnH [in Recipes_neutralization.Recipes_NF]accnH [in Recipes.Autosubst_lib.ARS]
accnL [in Recipes_neutralization.Recipes_NF]
accnL [in Recipes.Autosubst_lib.ARS]
And [in Recipes_neutralization.Recipes]
App [in Recipes_neutralization.Recipes]
Arr [in Recipes_neutralization.Recipes]
C
convR [in Recipes.Autosubst_lib.ARS]convSE [in Recipes.Autosubst_lib.ARS]
convSEi [in Recipes.Autosubst_lib.ARS]
F
FAll [in Recipes_neutralization.Recipes]FAnd [in Recipes_neutralization.Recipes]
FEqu [in Recipes_neutralization.Recipes]
FNot [in Recipes_neutralization.Recipes]
FOr [in Recipes_neutralization.Recipes]
I
Imp [in Recipes_neutralization.Recipes]L
Lam [in Recipes_neutralization.Recipes]P
plusSE [in Recipes.Autosubst_lib.ARS]pstep_and [in Recipes_neutralization.Recipes]
pstep_app [in Recipes_neutralization.Recipes]
pstep_tapp [in Recipes_neutralization.Recipes]
pstep_tall [in Recipes_neutralization.Recipes]
pstep_imp [in Recipes_neutralization.Recipes]
pstep_tlam [in Recipes_neutralization.Recipes]
pstep_lam [in Recipes_neutralization.Recipes]
pstep_tbeta [in Recipes_neutralization.Recipes]
pstep_beta [in Recipes_neutralization.Recipes]
pstep_top [in Recipes_neutralization.Recipes]
pstep_var [in Recipes_neutralization.Recipes]
S
SNI [in Recipes.Autosubst_lib.ARS]starR [in Recipes.Autosubst_lib.ARS]
starSE [in Recipes.Autosubst_lib.ARS]
step_ctx_tall [in Recipes_neutralization.Recipes]
step_ctx_tlam [in Recipes_neutralization.Recipes]
step_ctx_imp [in Recipes_neutralization.Recipes]
step_ctx_lam [in Recipes_neutralization.Recipes]
step_ctx_tapp [in Recipes_neutralization.Recipes]
step_ctx_appr [in Recipes_neutralization.Recipes]
step_ctx_appl [in Recipes_neutralization.Recipes]
step_ctx_andr [in Recipes_neutralization.Recipes]
step_ctx_andl [in Recipes_neutralization.Recipes]
step_tbeta [in Recipes_neutralization.Recipes]
step_beta [in Recipes_neutralization.Recipes]
T
TAll [in Recipes_neutralization.Recipes]TApp [in Recipes_neutralization.Recipes]
TArr [in Recipes_neutralization.Recipes]
TCons [in Recipes_neutralization.Recipes]
TLam [in Recipes_neutralization.Recipes]
TNat [in Recipes_neutralization.Recipes]
Top [in Recipes_neutralization.Recipes]
TVar [in Recipes_neutralization.Recipes]
ty_tapp [in Recipes_neutralization.Recipes]
ty_app [in Recipes_neutralization.Recipes]
ty_lam [in Recipes_neutralization.Recipes]
ty_and [in Recipes_neutralization.Recipes]
ty_imp [in Recipes_neutralization.Recipes]
ty_var [in Recipes_neutralization.Recipes]
ty_tlam [in Recipes_neutralization.Recipes]
ty_tall [in Recipes_neutralization.Recipes]
ty_top [in Recipes_neutralization.Recipes]
V
Var [in Recipes_neutralization.Recipes]Void [in Recipes_neutralization.Recipes]
Inductive Index
A
accn [in Recipes.Autosubst_lib.ARS]C
conv [in Recipes.Autosubst_lib.ARS]F
fmla [in Recipes_neutralization.Recipes]H
has_type [in Recipes_neutralization.Recipes]M
my_accn [in Recipes_neutralization.Recipes_NF]P
plus [in Recipes.Autosubst_lib.ARS]pstep [in Recipes_neutralization.Recipes]
R
recipe [in Recipes_neutralization.Recipes]S
sn [in Recipes.Autosubst_lib.ARS]star [in Recipes.Autosubst_lib.ARS]
step [in Recipes_neutralization.Recipes]
T
term [in Recipes_neutralization.Recipes]type [in Recipes_neutralization.Recipes]
Projection Index
D
dest [in Recipes_neutralization.Recipes_NF]dest_nf [in Recipes_neutralization.Recipes_NF]
E
eq_nrho [in Recipes_neutralization.Recipes_NF]P
path [in Recipes_neutralization.Recipes_NF]p_nc [in Recipes_neutralization.Recipes_SN]
p_cl [in Recipes_neutralization.Recipes_SN]
p_sn [in Recipes_neutralization.Recipes_SN]
R
rho_len [in Recipes_neutralization.Recipes_NF]Instance Index
H
HSubstLemmas_reci_term [in Recipes_neutralization.Recipes]HSubstLemmas_term_reci [in Recipes_neutralization.Recipes]
HSubst_reci_term [in Recipes_neutralization.Recipes]
HSubst_t_reci [in Recipes_neutralization.Recipes]
HSubst_t_fmla [in Recipes_neutralization.Recipes]
I
Ids_reci [in Recipes_neutralization.Recipes]Ids_term [in Recipes_neutralization.Recipes]
M
MMapExt_fun [in Recipes.Autosubst_lib.AutosubstSsr]mmapExt_seq [in Recipes.Autosubst_lib.AutosubstSsr]
MMapExt_pair [in Recipes.Autosubst_lib.AutosubstSsr]
MMapExt_option [in Recipes.Autosubst_lib.AutosubstSsr]
MMapLemmas_fun [in Recipes.Autosubst_lib.AutosubstSsr]
mmapLemmas_seq [in Recipes.Autosubst_lib.AutosubstSsr]
MMapLemmas_pair [in Recipes.Autosubst_lib.AutosubstSsr]
MMapLemmas_option [in Recipes.Autosubst_lib.AutosubstSsr]
MMap_fun [in Recipes.Autosubst_lib.AutosubstSsr]
mmap_seq [in Recipes.Autosubst_lib.AutosubstSsr]
MMap_pair [in Recipes.Autosubst_lib.AutosubstSsr]
MMap_option [in Recipes.Autosubst_lib.AutosubstSsr]
R
Rename_reci [in Recipes_neutralization.Recipes]Rename_flma [in Recipes_neutralization.Recipes]
Rename_term [in Recipes_neutralization.Recipes]
S
SubstHSubstComp_term_reci [in Recipes_neutralization.Recipes]SubstHSubstComp_reci_term [in Recipes_neutralization.Recipes]
SubstLemmas_reci [in Recipes_neutralization.Recipes]
SubstLemmas_term [in Recipes_neutralization.Recipes]
Subst_reci [in Recipes_neutralization.Recipes]
Subst_fmla [in Recipes_neutralization.Recipes]
Subst_term [in Recipes_neutralization.Recipes]
Section Index
A
AST [in Recipes_neutralization.Recipes]AutosubstTypeClasses [in Recipes_neutralization.Recipes]
C
CoFinal [in Recipes.Autosubst_lib.ARS]Commutation [in Recipes.Autosubst_lib.ARS]
ComputationN [in Recipes.Autosubst_lib.ARS]
D
Definitions [in Recipes.Autosubst_lib.ARS]E
EqDec [in Recipes_neutralization.Recipes]F
FPottierIdeas [in Recipes_neutralization.My_autosubst]M
MMapInstances [in Recipes.Autosubst_lib.AutosubstSsr]MyComputationN [in Recipes_neutralization.Recipes_NF]
MyLemmas [in Recipes_neutralization.My_autosubst]
N
Neutralization [in Recipes_neutralization.Recipes]P
Plus_lemmas [in Recipes_neutralization.Recipes_NF]S
StarStep [in Recipes_neutralization.Recipes]StarStep.ChurchRosser [in Recipes_neutralization.Recipes]
Step [in Recipes_neutralization.Recipes]
SubstLemmasP [in Recipes_neutralization.Recipes]
T
Termination [in Recipes.Autosubst_lib.ARS]TypingDefinitions [in Recipes_neutralization.Recipes]
TypingLemmas [in Recipes_neutralization.Recipes]
TypingLemmas.SubjectReduction [in Recipes_neutralization.Recipes]
Definition Index
A
accn_ind' [in Recipes_neutralization.Recipes_NF]accn_ind' [in Recipes.Autosubst_lib.ARS]
accn_sind [in Recipes.Autosubst_lib.ARS]
accn_ind [in Recipes.Autosubst_lib.ARS]
admissible_subst2 [in Recipes_neutralization.Recipes]
admissible_subst [in Recipes_neutralization.Recipes]
C
cand [in Recipes_neutralization.Recipes_SN]closed [in Recipes_neutralization.My_autosubst]
cofinal [in Recipes.Autosubst_lib.ARS]
com [in Recipes.Autosubst_lib.ARS]
confluent [in Recipes.Autosubst_lib.ARS]
conv_sind [in Recipes.Autosubst_lib.ARS]
conv_ind [in Recipes.Autosubst_lib.ARS]
CR [in Recipes.Autosubst_lib.ARS]
ctx [in Recipes_neutralization.Recipes]
D
diamond [in Recipes.Autosubst_lib.ARS]E
eval [in Recipes_neutralization.Recipes_NF]evaln [in Recipes.Autosubst_lib.ARS]
eval_nf [in Recipes_neutralization.Recipes_NF]
eval0 [in Recipes_neutralization.Recipes_NF]
F
fmla_sind [in Recipes_neutralization.Recipes]fmla_rec [in Recipes_neutralization.Recipes]
fmla_ind [in Recipes_neutralization.Recipes]
fmla_rect [in Recipes_neutralization.Recipes]
fv [in Recipes_neutralization.My_autosubst]
fv_hsubst_old [in Recipes_neutralization.My_autosubst]
fv_t_old [in Recipes_neutralization.My_autosubst]
fv_old [in Recipes_neutralization.My_autosubst]
fv_hsubst [in Recipes_neutralization.My_autosubst]
fv_t [in Recipes_neutralization.My_autosubst]
H
has_type_sind [in Recipes_neutralization.Recipes]has_type_ind [in Recipes_neutralization.Recipes]
J
joinable [in Recipes.Autosubst_lib.ARS]M
my_evaln [in Recipes_neutralization.Recipes_NF]my_accn_sind [in Recipes_neutralization.Recipes_NF]
my_accn_ind [in Recipes_neutralization.Recipes_NF]
my_nf [in Recipes_neutralization.Recipes_NF]
N
NEU [in Recipes_neutralization.Recipes_neutralization]neu [in Recipes_neutralization.Recipes]
neutral [in Recipes_neutralization.Recipes_neutralization]
NEUσ [in Recipes_neutralization.Recipes_neutralization]
nf [in Recipes.Autosubst_lib.ARS]
normal [in Recipes.Autosubst_lib.ARS]
normalizing [in Recipes.Autosubst_lib.ARS]
ns [in Recipes_neutralization.Recipes]
P
plus_sind [in Recipes.Autosubst_lib.ARS]plus_ind [in Recipes.Autosubst_lib.ARS]
ppets [in Recipes_neutralization.Recipes_NF]
Pred [in Recipes.Autosubst_lib.ARS]
psstep [in Recipes_neutralization.Recipes]
pstep_sind [in Recipes_neutralization.Recipes]
pstep_ind [in Recipes_neutralization.Recipes]
R
recipe_sind [in Recipes_neutralization.Recipes]recipe_rec [in Recipes_neutralization.Recipes]
recipe_ind [in Recipes_neutralization.Recipes]
recipe_rect [in Recipes_neutralization.Recipes]
RED [in Recipes_neutralization.Recipes_SN]
red [in Recipes_neutralization.Recipes]
reducible [in Recipes.Autosubst_lib.ARS]
REDσ [in Recipes_neutralization.Recipes_SN]
Rel [in Recipes.Autosubst_lib.ARS]
rho [in Recipes_neutralization.Recipes_NF]
rho [in Recipes_neutralization.Recipes]
rho_wt [in Recipes_neutralization.Recipes_NF]
S
simple [in Recipes_neutralization.Recipes_SN]sneu [in Recipes_neutralization.Recipes]
sn_sind [in Recipes.Autosubst_lib.ARS]
sn_rec [in Recipes.Autosubst_lib.ARS]
sn_ind [in Recipes.Autosubst_lib.ARS]
sn_rect [in Recipes.Autosubst_lib.ARS]
sred [in Recipes_neutralization.Recipes]
star_sind [in Recipes.Autosubst_lib.ARS]
star_ind [in Recipes.Autosubst_lib.ARS]
step_sind [in Recipes_neutralization.Recipes]
step_ind [in Recipes_neutralization.Recipes]
T
term_sind [in Recipes_neutralization.Recipes]term_rec [in Recipes_neutralization.Recipes]
term_ind [in Recipes_neutralization.Recipes]
term_rect [in Recipes_neutralization.Recipes]
triangle [in Recipes.Autosubst_lib.ARS]
type_sind [in Recipes_neutralization.Recipes]
type_rec [in Recipes_neutralization.Recipes]
type_ind [in Recipes_neutralization.Recipes]
type_rect [in Recipes_neutralization.Recipes]
W
wf_subst [in Recipes_neutralization.Recipes]wf_ctx [in Recipes_neutralization.Recipes]
wn [in Recipes.Autosubst_lib.ARS]
wt2nf_sig [in Recipes_neutralization.Recipes_NF]
Record Index
R
reducible [in Recipes_neutralization.Recipes_SN]RNF [in Recipes_neutralization.Recipes_NF]
| 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 | _ | other | (504 entries) |
| Notation 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 | _ | other | (8 entries) |
| Variable 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 | _ | other | (25 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 | _ | other | (9 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 | _ | other | (233 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 | _ | other | (6 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 | _ | other | (62 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 | _ | other | (13 entries) |
| Projection 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 | _ | other | (8 entries) |
| Instance 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 | _ | other | (29 entries) |
| Section 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 | _ | other | (21 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 | _ | other | (88 entries) |
| Record 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 | _ | other | (2 entries) |