| 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 | (864 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 | (41 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 | (34 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 | (22 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 | (325 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 | (167 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 | (52 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 | (24 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 | (99 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 | (17 entries) |
| Abbreviation 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 | (7 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 | (60 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 | (16 entries) |
Global Index
A
Abs [constructor, in Ssr.SystemF_SN]Abs [constructor, in Ssr.SystemF_CBV]
Abs [constructor, in Plain.POPLmark]
Abs [constructor, in Ssr.POPLmark]
accn [inductive, in Ssr.ARS]
accnH [constructor, in Ssr.ARS]
accnL [constructor, in Ssr.ARS]
accn_inv [lemma, in Ssr.ARS]
accn_ind' [definition, in Ssr.ARS]
admissible [definition, in Ssr.SystemF_SN]
ad_cons [lemma, in Ssr.SystemF_SN]
All [constructor, in Ssr.SystemF_SN]
All [constructor, in Ssr.SystemF_CBV]
All [constructor, in Plain.POPLmark]
All [constructor, in Ssr.POPLmark]
annot [definition, in Autosubst.Autosubst_Basics]
App [constructor, in Ssr.CR]
App [constructor, in Ssr.SystemF_SN]
App [constructor, in Ssr.SystemF_CBV]
App [constructor, in Plain.Demo]
App [constructor, in Ssr.pred_CC_omega]
App [constructor, in Plain.POPLmark]
App [constructor, in Ssr.BetaSubstitution]
App [constructor, in Ssr.POPLmark]
Arr [constructor, in Ssr.SystemF_SN]
Arr [constructor, in Ssr.SystemF_CBV]
Arr [constructor, in Plain.Demo]
Arr [constructor, in Plain.POPLmark]
Arr [constructor, in Ssr.POPLmark]
ARS [library]
atn [definition, in Plain.Context]
atnd [inductive, in Plain.Context]
AtndS [constructor, in Plain.Context]
atnd_defined [lemma, in Plain.Context]
atnd_repl [lemma, in Plain.Context]
atnd_step [lemma, in Plain.Context]
atnd_steps' [lemma, in Plain.Context]
atnd_steps [lemma, in Plain.Context]
Atnd0 [constructor, in Plain.Context]
atn_mmap [lemma, in Plain.Context]
Autosubst [library]
AutosubstSsr [library]
Autosubst_Lemmas [library]
Autosubst_Tactics [library]
Autosubst_Derive [library]
Autosubst_Basics [library]
Autosubst_Classes [library]
Autosubst_MMap [library]
Autosubst_MMapInstances [library]
B
Base [constructor, in Plain.Demo]BetaSubstitution [library]
beta_expansion [lemma, in Ssr.SystemF_SN]
C
cand [definition, in Ssr.SystemF_SN]canonical_all [lemma, in Ssr.POPLmark]
canonical_all' [lemma, in Ssr.POPLmark]
canonical_arr [lemma, in Ssr.POPLmark]
canonical_arr' [lemma, in Ssr.POPLmark]
can_form_all [lemma, in Plain.POPLmark]
can_form_arr [lemma, in Plain.POPLmark]
church_rosser [lemma, in Ssr.CR]
church_rosser [lemma, in Ssr.pred_CC_omega]
cofinal [definition, in Ssr.ARS]
CoFinal [section, in Ssr.ARS]
cofinal_normalizing [lemma, in Ssr.ARS]
CoFinal.e [variable, in Ssr.ARS]
CoFinal.rho [variable, in Ssr.ARS]
CoFinal.T [variable, in Ssr.ARS]
CoFinal.tri [variable, in Ssr.ARS]
com [definition, in Ssr.ARS]
Commutation [section, in Ssr.ARS]
Commutation.T [variable, in Ssr.ARS]
compA [lemma, in Autosubst.Autosubst_Basics]
ComputationN [section, in Ssr.ARS]
ComputationN.classical [variable, in Ssr.ARS]
ComputationN.e [variable, in Ssr.ARS]
ComputationN.norm [variable, in Ssr.ARS]
ComputationN.rho [variable, in Ssr.ARS]
ComputationN.sound [variable, in Ssr.ARS]
ComputationN.T [variable, in Ssr.ARS]
comp_id [lemma, in Autosubst.Autosubst_Basics]
com_lift [lemma, in Ssr.ARS]
com_strip [lemma, in Ssr.ARS]
confluent [definition, in Ssr.ARS]
confluent_stable [lemma, in Ssr.ARS]
confluent_cr [lemma, in Ssr.ARS]
conj' [lemma, in Plain.POPLmark]
consistency [lemma, in Ssr.SystemF_CBV]
Context [library]
Context [library]
context_ok [inductive, in Ssr.pred_CC_omega]
conv [inductive, in Ssr.ARS]
convES [lemma, in Ssr.ARS]
convESi [lemma, in Ssr.ARS]
convR [constructor, in Ssr.ARS]
convSE [constructor, in Ssr.ARS]
convSEi [constructor, in Ssr.ARS]
conv_sub [lemma, in Ssr.pred_CC_omega]
conv_sub1 [lemma, in Ssr.pred_CC_omega]
conv_prod_sort [lemma, in Ssr.pred_CC_omega]
conv_beta [lemma, in Ssr.pred_CC_omega]
conv_compat [lemma, in Ssr.pred_CC_omega]
conv_subst [lemma, in Ssr.pred_CC_omega]
conv_prod [lemma, in Ssr.pred_CC_omega]
conv_lam [lemma, in Ssr.pred_CC_omega]
conv_app [lemma, in Ssr.pred_CC_omega]
conv_closure [lemma, in Ssr.ARS]
conv_hom [lemma, in Ssr.ARS]
conv_img [lemma, in Ssr.ARS]
conv_sym [lemma, in Ssr.ARS]
conv_trans [lemma, in Ssr.ARS]
conv1 [lemma, in Ssr.ARS]
conv1i [lemma, in Ssr.ARS]
CR [definition, in Ssr.ARS]
CR [library]
cr_method [lemma, in Ssr.ARS]
cr_conv_normal [lemma, in Ssr.ARS]
cr_star_normal [lemma, in Ssr.ARS]
ctx [definition, in Ssr.SystemF_SN]
ctx [definition, in Ssr.SystemF_CBV]
ctx_ncons [constructor, in Ssr.pred_CC_omega]
ctx_nil [constructor, in Ssr.pred_CC_omega]
D
Dec [record, in Plain.Decidable]Dec [inductive, in Plain.Decidable]
dec [definition, in Plain.Decidable]
Decidable [library]
decide [projection, in Plain.Decidable]
decide [constructor, in Plain.Decidable]
decide_lt_nat [instance, in Plain.Decidable]
decide_le_nat [instance, in Plain.Decidable]
decide_eq_nat [instance, in Plain.Decidable]
Definitions [section, in Ssr.ARS]
Definitions.e [variable, in Ssr.ARS]
Definitions.T [variable, in Ssr.ARS]
Demo [library]
dget [definition, in Ssr.Context]
diamond [definition, in Ssr.ARS]
diamond_confluent [lemma, in Ssr.ARS]
E
E [abbreviation, in Ssr.SystemF_CBV]EL [definition, in Ssr.SystemF_SN]
equal_f [lemma, in Autosubst.Autosubst_Basics]
eq_V [lemma, in Ssr.SystemF_CBV]
eq_star [lemma, in Ssr.ARS]
eval [inductive, in Ssr.SystemF_CBV]
eval [inductive, in Plain.POPLmark]
eval [inductive, in Ssr.POPLmark]
evaln [definition, in Ssr.ARS]
evalnP [lemma, in Ssr.ARS]
evaln_sound [lemma, in Ssr.ARS]
eval_tabs [constructor, in Ssr.SystemF_CBV]
eval_abs [constructor, in Ssr.SystemF_CBV]
eval_tbeta [constructor, in Ssr.SystemF_CBV]
eval_beta [constructor, in Ssr.SystemF_CBV]
ev_progress [lemma, in Plain.POPLmark]
ev_progress [lemma, in Ssr.POPLmark]
ev_progress' [lemma, in Ssr.POPLmark]
eweakening [lemma, in Ssr.pred_CC_omega]
extend_ext [lemma, in Ssr.SystemF_SN]
E_ren [lemma, in Ssr.SystemF_CBV]
E_TypeFun [constructor, in Plain.POPLmark]
E_AppArg [constructor, in Plain.POPLmark]
E_AppFun [constructor, in Plain.POPLmark]
E_TAppTAbs [constructor, in Plain.POPLmark]
E_AppAbs [constructor, in Plain.POPLmark]
E_TypeFun [constructor, in Ssr.POPLmark]
E_AppArg [constructor, in Ssr.POPLmark]
E_AppFun [constructor, in Ssr.POPLmark]
E_TAppTAbs [constructor, in Ssr.POPLmark]
E_AppAbs [constructor, in Ssr.POPLmark]
F
fold_upn_up [lemma, in Autosubst.Autosubst_Tactics]fold_up_upn [lemma, in Autosubst.Autosubst_Tactics]
fold_up_up [lemma, in Autosubst.Autosubst_Tactics]
fold_up0 [lemma, in Autosubst.Autosubst_Tactics]
fold_up [lemma, in Autosubst.Autosubst_Tactics]
fold_ren_cons [lemma, in Autosubst.Autosubst_Tactics]
funcomp [definition, in Autosubst.Autosubst_Basics]
G
get [definition, in Ssr.Context]get_map [lemma, in Ssr.Context]
H
has_type [inductive, in Ssr.SystemF_SN]has_type [inductive, in Ssr.SystemF_CBV]
has_type [inductive, in Ssr.pred_CC_omega]
hcomp [definition, in Autosubst.Autosubst_Classes]
hcomp_dist_internal [lemma, in Autosubst.Autosubst_Derive]
hcomp_ren_internal [lemma, in Autosubst.Autosubst_Derive]
hcomp_lift_internal [lemma, in Autosubst.Autosubst_Derive]
hcomp_lift_n_internal [lemma, in Autosubst.Autosubst_Derive]
hsubst [projection, in Autosubst.Autosubst_Classes]
HSubst [record, in Autosubst.Autosubst_Classes]
hsubst [constructor, in Autosubst.Autosubst_Classes]
HSubst [inductive, in Autosubst.Autosubst_Classes]
HSubstHSubstComp [record, in Autosubst.Autosubst_Classes]
HSubstHSubstComp [inductive, in Autosubst.Autosubst_Classes]
HSubstHSubstInd [record, in Autosubst.Autosubst_Classes]
HSubstHSubstInd [inductive, in Autosubst.Autosubst_Classes]
HSubstLemmas [record, in Autosubst.Autosubst_Classes]
HSubstLemmas_term [instance, in Ssr.SystemF_SN]
HSubstLemmas_term [instance, in Ssr.SystemF_CBV]
HSubstLemmas_term [instance, in Plain.POPLmark]
HSubstLemmas_term [instance, in Ssr.POPLmark]
HSubst_term [instance, in Ssr.SystemF_SN]
HSubst_term [instance, in Ssr.SystemF_CBV]
hsubst_hsubst_ind [projection, in Autosubst.Autosubst_Classes]
hsubst_hsubst_ind [constructor, in Autosubst.Autosubst_Classes]
hsubst_hsubst_comp [projection, in Autosubst.Autosubst_Classes]
hsubst_hsubst_comp [constructor, in Autosubst.Autosubst_Classes]
hsubst_comp [projection, in Autosubst.Autosubst_Classes]
hsubst_id [projection, in Autosubst.Autosubst_Classes]
hsubst_compR [lemma, in Autosubst.Autosubst_Tactics]
hsubst_compX [lemma, in Autosubst.Autosubst_Tactics]
hsubst_compI [lemma, in Autosubst.Autosubst_Tactics]
hsubst_idX [lemma, in Autosubst.Autosubst_Tactics]
hsubst_term [instance, in Plain.POPLmark]
HSubst_term [instance, in Ssr.POPLmark]
I
id [definition, in Autosubst.Autosubst_Basics]ids [projection, in Autosubst.Autosubst_Classes]
Ids [record, in Autosubst.Autosubst_Classes]
ids [constructor, in Autosubst.Autosubst_Classes]
Ids [inductive, in Autosubst.Autosubst_Classes]
Ids_term [instance, in Ssr.CR]
Ids_term [instance, in Ssr.SystemF_SN]
Ids_type [instance, in Ssr.SystemF_SN]
Ids_term [instance, in Ssr.SystemF_CBV]
Ids_type [instance, in Ssr.SystemF_CBV]
Ids_term [instance, in Plain.Demo]
Ids_term [instance, in Ssr.pred_CC_omega]
Ids_term [instance, in Plain.POPLmark]
Ids_type [instance, in Plain.POPLmark]
Ids_term [instance, in Ssr.BetaSubstitution]
Ids_term [instance, in Ssr.POPLmark]
Ids_type [instance, in Ssr.POPLmark]
id_hsubst [projection, in Autosubst.Autosubst_Classes]
id_subst [projection, in Autosubst.Autosubst_Classes]
id_hsubstR [lemma, in Autosubst.Autosubst_Tactics]
id_hsubstX [lemma, in Autosubst.Autosubst_Tactics]
id_scompR [lemma, in Autosubst.Autosubst_Tactics]
id_scompX [lemma, in Autosubst.Autosubst_Tactics]
id_comp [lemma, in Autosubst.Autosubst_Basics]
inj_prod [lemma, in Ssr.pred_CC_omega]
inj_sort [lemma, in Ssr.pred_CC_omega]
inst_expansion [lemma, in Ssr.SystemF_SN]
InternalLemmas [section, in Autosubst.Autosubst_Derive]
InternalLemmasHSubst [section, in Autosubst.Autosubst_Derive]
is_tabs [definition, in Ssr.POPLmark]
is_abs [definition, in Ssr.POPLmark]
is_var [definition, in Ssr.POPLmark]
iterate [definition, in Autosubst.Autosubst_Basics]
iterate_Sr [lemma, in Autosubst.Autosubst_Basics]
iterate_0 [lemma, in Autosubst.Autosubst_Basics]
iterate_S [lemma, in Autosubst.Autosubst_Basics]
iter_param [lemma, in Autosubst.Autosubst_Derive]
iter_fp [lemma, in Autosubst.Autosubst_Derive]
J
joinable [definition, in Ssr.ARS]join_conv [lemma, in Ssr.ARS]
L
L [definition, in Ssr.SystemF_SN]L [definition, in Ssr.SystemF_CBV]
Lam [constructor, in Ssr.CR]
Lam [constructor, in Plain.Demo]
Lam [constructor, in Ssr.pred_CC_omega]
Lam [constructor, in Ssr.BetaSubstitution]
LemmasForFun [section, in Autosubst.Autosubst_Basics]
LemmasForHSubst [section, in Autosubst.Autosubst_Tactics]
LemmasForMMap [section, in Autosubst.Autosubst_MMap]
LemmasForSubst [section, in Autosubst.Autosubst_Tactics]
lift [definition, in Autosubst.Autosubst_Basics]
lift [abbreviation, in Ssr.BetaSubstitution]
lift_eta [lemma, in Autosubst.Autosubst_Basics]
lift_compR [lemma, in Autosubst.Autosubst_Basics]
lift_comp [lemma, in Autosubst.Autosubst_Basics]
lift_scons [lemma, in Autosubst.Autosubst_Basics]
lift_injn [lemma, in Autosubst.Autosubst_Lemmas]
lift_inj [lemma, in Autosubst.Autosubst_Lemmas]
lift_sound [lemma, in Ssr.BetaSubstitution]
lift_at_sound [lemma, in Ssr.BetaSubstitution]
lift_at [definition, in Ssr.BetaSubstitution]
lift0 [lemma, in Autosubst.Autosubst_Basics]
lift0 [lemma, in Autosubst.Autosubst_Lemmas]
L_subst [lemma, in Ssr.SystemF_SN]
L_weaken [lemma, in Ssr.SystemF_SN]
L_ren [lemma, in Ssr.SystemF_SN]
L_ext [lemma, in Ssr.SystemF_SN]
L_cl_star [lemma, in Ssr.SystemF_SN]
L_var [lemma, in Ssr.SystemF_SN]
L_nc [lemma, in Ssr.SystemF_SN]
L_cl [lemma, in Ssr.SystemF_SN]
L_sn [lemma, in Ssr.SystemF_SN]
L_reducible [lemma, in Ssr.SystemF_SN]
M
mmap [projection, in Autosubst.Autosubst_MMap]MMap [record, in Autosubst.Autosubst_MMap]
mmap [constructor, in Autosubst.Autosubst_MMap]
MMap [inductive, in Autosubst.Autosubst_MMap]
MMapConst [section, in Autosubst.Autosubst_MMap]
MMapExt [record, in Autosubst.Autosubst_MMap]
MMapExt [inductive, in Autosubst.Autosubst_MMap]
MMapExt_fun [instance, in Ssr.AutosubstSsr]
mmapExt_seq [instance, in Ssr.AutosubstSsr]
MMapExt_pair [instance, in Ssr.AutosubstSsr]
MMapExt_option [instance, in Ssr.AutosubstSsr]
MMapExt_fun [instance, in Autosubst.Autosubst_MMapInstances]
MMapExt_pair [instance, in Autosubst.Autosubst_MMapInstances]
MMapExt_list [instance, in Autosubst.Autosubst_MMapInstances]
MMapExt_option [instance, in Autosubst.Autosubst_MMapInstances]
MMapExt_const [instance, in Autosubst.Autosubst_MMap]
MMapExt_refl [instance, in Autosubst.Autosubst_MMap]
MMapId [section, in Autosubst.Autosubst_MMap]
MMapInstances [section, in Ssr.AutosubstSsr]
MMapInstances [section, in Autosubst.Autosubst_MMapInstances]
MMapInstances.A [variable, in Ssr.AutosubstSsr]
MMapInstances.A [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.B [variable, in Ssr.AutosubstSsr]
MMapInstances.B [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.C [variable, in Ssr.AutosubstSsr]
MMapInstances.C [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapExt_A_C [variable, in Ssr.AutosubstSsr]
MMapInstances.MMapExt_A_B [variable, in Ssr.AutosubstSsr]
MMapInstances.MMapExt_A_C [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapExt_A_B [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_C [variable, in Ssr.AutosubstSsr]
MMapInstances.MMapLemmas_A_B [variable, in Ssr.AutosubstSsr]
MMapInstances.MMapLemmas_A_C [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_B [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMap_A_C [variable, in Ssr.AutosubstSsr]
MMapInstances.MMap_A_B [variable, in Ssr.AutosubstSsr]
MMapInstances.MMap_A_C [variable, in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMap_A_B [variable, in Autosubst.Autosubst_MMapInstances]
MMapLemmas [record, in Autosubst.Autosubst_MMap]
MMapLemmas_fun [instance, in Ssr.AutosubstSsr]
mmapLemmas_seq [instance, in Ssr.AutosubstSsr]
MMapLemmas_pair [instance, in Ssr.AutosubstSsr]
MMapLemmas_option [instance, in Ssr.AutosubstSsr]
MMapLemmas_fun [instance, in Autosubst.Autosubst_MMapInstances]
MMapLemmas_pair [instance, in Autosubst.Autosubst_MMapInstances]
MMapLemmas_list [instance, in Autosubst.Autosubst_MMapInstances]
MMapLemmas_option [instance, in Autosubst.Autosubst_MMapInstances]
MMapLemmas_const [instance, in Autosubst.Autosubst_MMap]
MMapLemmas_refl [instance, in Autosubst.Autosubst_MMap]
MMap_fun [instance, in Ssr.AutosubstSsr]
mmap_seq [instance, in Ssr.AutosubstSsr]
MMap_pair [instance, in Ssr.AutosubstSsr]
MMap_option [instance, in Ssr.AutosubstSsr]
mmap_atn [lemma, in Plain.Context]
MMap_fun [instance, in Autosubst.Autosubst_MMapInstances]
MMap_pair [instance, in Autosubst.Autosubst_MMapInstances]
MMap_list [instance, in Autosubst.Autosubst_MMapInstances]
MMap_option [instance, in Autosubst.Autosubst_MMapInstances]
mmap_id_ext [lemma, in Autosubst.Autosubst_Derive]
mmap_const_instE [lemma, in Autosubst.Autosubst_MMap]
MMap_const [instance, in Autosubst.Autosubst_MMap]
mmap_id_instE [lemma, in Autosubst.Autosubst_MMap]
MMap_refl [instance, in Autosubst.Autosubst_MMap]
mmap_compR [lemma, in Autosubst.Autosubst_MMap]
mmap_compX [lemma, in Autosubst.Autosubst_MMap]
mmap_idX [lemma, in Autosubst.Autosubst_MMap]
mmap_comp [projection, in Autosubst.Autosubst_MMap]
mmap_id [projection, in Autosubst.Autosubst_MMap]
mmap_ext [projection, in Autosubst.Autosubst_MMap]
mmap_ext [constructor, in Autosubst.Autosubst_MMap]
N
neutral [definition, in Ssr.SystemF_SN]nf [definition, in Ssr.ARS]
nf_accn [lemma, in Ssr.ARS]
nilA [definition, in Ssr.SystemF_CBV]
normal [definition, in Ssr.ARS]
normalization [lemma, in Ssr.SystemF_CBV]
normalizing [definition, in Ssr.ARS]
normal_step_sort [lemma, in Ssr.pred_CC_omega]
normal_star [lemma, in Ssr.ARS]
P
plusA [lemma, in Autosubst.Autosubst_Basics]plusnO [lemma, in Autosubst.Autosubst_Basics]
plusnS [lemma, in Autosubst.Autosubst_Basics]
plusOn [lemma, in Autosubst.Autosubst_Basics]
plusSn [lemma, in Autosubst.Autosubst_Basics]
POPLmark [library]
POPLmark [library]
Pred [definition, in Ssr.ARS]
pred_CC_omega [library]
preservation [lemma, in Plain.POPLmark]
preservation [lemma, in Ssr.POPLmark]
Prod [constructor, in Ssr.pred_CC_omega]
propagation [lemma, in Ssr.pred_CC_omega]
psstep [definition, in Ssr.CR]
psstep [definition, in Ssr.pred_CC_omega]
psstep_up [lemma, in Ssr.CR]
psstep_up [lemma, in Ssr.pred_CC_omega]
pstep [inductive, in Ssr.CR]
pstep [inductive, in Ssr.pred_CC_omega]
pstep_compat_beta [lemma, in Ssr.CR]
pstep_compat [lemma, in Ssr.CR]
pstep_subst [lemma, in Ssr.CR]
pstep_red [lemma, in Ssr.CR]
pstep_refl [lemma, in Ssr.CR]
pstep_ebeta [lemma, in Ssr.CR]
pstep_lam [constructor, in Ssr.CR]
pstep_app [constructor, in Ssr.CR]
pstep_var [constructor, in Ssr.CR]
pstep_beta [constructor, in Ssr.CR]
pstep_compat_beta [lemma, in Ssr.pred_CC_omega]
pstep_compat [lemma, in Ssr.pred_CC_omega]
pstep_subst [lemma, in Ssr.pred_CC_omega]
pstep_red [lemma, in Ssr.pred_CC_omega]
pstep_refl [lemma, in Ssr.pred_CC_omega]
pstep_prod [constructor, in Ssr.pred_CC_omega]
pstep_lam [constructor, in Ssr.pred_CC_omega]
pstep_app [constructor, in Ssr.pred_CC_omega]
pstep_sort [constructor, in Ssr.pred_CC_omega]
pstep_var [constructor, in Ssr.pred_CC_omega]
pstep_beta [constructor, in Ssr.pred_CC_omega]
p_nc [projection, in Ssr.SystemF_SN]
p_cl [projection, in Ssr.SystemF_SN]
p_sn [projection, in Ssr.SystemF_SN]
R
red [abbreviation, in Ssr.CR]red [definition, in Ssr.SystemF_SN]
red [abbreviation, in Ssr.pred_CC_omega]
RedProdSpec [inductive, in Ssr.pred_CC_omega]
RedProdSpecI [constructor, in Ssr.pred_CC_omega]
reducible [record, in Ssr.SystemF_SN]
reducible [definition, in Ssr.ARS]
reducible_var [lemma, in Ssr.SystemF_SN]
reducible_sn [lemma, in Ssr.SystemF_SN]
red_lam [lemma, in Ssr.CR]
red_app [lemma, in Ssr.CR]
red_beta [lemma, in Ssr.SystemF_SN]
red_compat [lemma, in Ssr.SystemF_SN]
red_hsubst [lemma, in Ssr.SystemF_SN]
red_subst [lemma, in Ssr.SystemF_SN]
red_tabs [lemma, in Ssr.SystemF_SN]
red_tapp [lemma, in Ssr.SystemF_SN]
red_abs [lemma, in Ssr.SystemF_SN]
red_app [lemma, in Ssr.SystemF_SN]
red_prod_inv [lemma, in Ssr.pred_CC_omega]
red_compat [lemma, in Ssr.pred_CC_omega]
red_subst [lemma, in Ssr.pred_CC_omega]
red_prod [lemma, in Ssr.pred_CC_omega]
red_lam [lemma, in Ssr.pred_CC_omega]
red_app [lemma, in Ssr.pred_CC_omega]
Rel [definition, in Ssr.ARS]
ren [definition, in Autosubst.Autosubst_Classes]
rename [projection, in Autosubst.Autosubst_Classes]
Rename [record, in Autosubst.Autosubst_Classes]
rename [constructor, in Autosubst.Autosubst_Classes]
Rename [inductive, in Autosubst.Autosubst_Classes]
Rename_term [instance, in Ssr.CR]
Rename_term [instance, in Ssr.SystemF_SN]
Rename_type [instance, in Ssr.SystemF_SN]
Rename_term [instance, in Ssr.SystemF_CBV]
Rename_type [instance, in Ssr.SystemF_CBV]
rename_subst [projection, in Autosubst.Autosubst_Classes]
rename_substX [lemma, in Autosubst.Autosubst_Tactics]
Rename_term [instance, in Plain.Demo]
Rename_term [instance, in Ssr.pred_CC_omega]
Rename_term [instance, in Plain.POPLmark]
Rename_type [instance, in Plain.POPLmark]
Rename_term [instance, in Ssr.BetaSubstitution]
Rename_term [instance, in Ssr.POPLmark]
Rename_type [instance, in Ssr.POPLmark]
renS [lemma, in Autosubst.Autosubst_Lemmas]
ren_uncomp [lemma, in Autosubst.Autosubst_Lemmas]
ren_size_inv [lemma, in Plain.POPLmark]
rho [definition, in Ssr.CR]
rho [definition, in Ssr.pred_CC_omega]
rho_triangle [lemma, in Ssr.CR]
rho_id [lemma, in Ssr.SystemF_SN]
rho_triangle [lemma, in Ssr.pred_CC_omega]
S
SA_All [constructor, in Plain.POPLmark]SA_Arrow [constructor, in Plain.POPLmark]
SA_Trans [constructor, in Plain.POPLmark]
SA_Refl [constructor, in Plain.POPLmark]
SA_Top [constructor, in Plain.POPLmark]
sbst [abbreviation, in Ssr.BetaSubstitution]
sbst_sound [lemma, in Ssr.BetaSubstitution]
sbst_at_sound [lemma, in Ssr.BetaSubstitution]
sbst_at [definition, in Ssr.BetaSubstitution]
scomp [definition, in Autosubst.Autosubst_Classes]
scomp_hcompR [lemma, in Autosubst.Autosubst_Tactics]
scomp_hcompX [lemma, in Autosubst.Autosubst_Tactics]
scomp_hcompI [lemma, in Autosubst.Autosubst_Tactics]
scons [definition, in Autosubst.Autosubst_Basics]
scons_eta [lemma, in Autosubst.Autosubst_Basics]
scons_comp [lemma, in Autosubst.Autosubst_Basics]
sconv [definition, in Ssr.pred_CC_omega]
sconv_up [lemma, in Ssr.pred_CC_omega]
size [projection, in Plain.Size]
Size [record, in Plain.Size]
size [constructor, in Plain.Size]
Size [inductive, in Plain.Size]
Size [library]
SizeFact [record, in Plain.Size]
SizeFact [inductive, in Plain.Size]
size_term [instance, in Plain.POPLmark]
size_type [instance, in Plain.POPLmark]
size_fact_In [instance, in Plain.Size]
size_In [lemma, in Plain.Size]
size_fact_app [instance, in Plain.Size]
size_app [lemma, in Plain.Size]
size_fact [projection, in Plain.Size]
size_fact [constructor, in Plain.Size]
size_nat [instance, in Plain.Size]
size_list [instance, in Plain.Size]
size_ind2 [lemma, in Plain.Size]
size_rec [lemma, in Plain.Size]
sn [abbreviation, in Ssr.SystemF_SN]
sn [inductive, in Ssr.ARS]
SNI [constructor, in Ssr.ARS]
sn_hsubst [lemma, in Ssr.SystemF_SN]
sn_subst [lemma, in Ssr.SystemF_SN]
sn_tclosed [lemma, in Ssr.SystemF_SN]
sn_closed [lemma, in Ssr.SystemF_SN]
sn_wn [lemma, in Ssr.ARS]
sn_preimage [lemma, in Ssr.ARS]
Sort [constructor, in Ssr.pred_CC_omega]
soundness [lemma, in Ssr.SystemF_SN]
soundness [lemma, in Ssr.SystemF_CBV]
soundness_nil [lemma, in Ssr.SystemF_CBV]
sred [definition, in Ssr.SystemF_SN]
sred [definition, in Ssr.pred_CC_omega]
sred_hup [lemma, in Ssr.SystemF_SN]
sred_up [lemma, in Ssr.SystemF_SN]
sred_up [lemma, in Ssr.pred_CC_omega]
star [inductive, in Ssr.ARS]
starES [lemma, in Ssr.ARS]
starR [constructor, in Ssr.ARS]
starSE [constructor, in Ssr.ARS]
star_interpolation [lemma, in Ssr.ARS]
star_monotone [lemma, in Ssr.ARS]
star_closure [lemma, in Ssr.ARS]
star_hom [lemma, in Ssr.ARS]
star_img [lemma, in Ssr.ARS]
star_conv [lemma, in Ssr.ARS]
star_trans [lemma, in Ssr.ARS]
star1 [lemma, in Ssr.ARS]
step [inductive, in Ssr.CR]
step [inductive, in Ssr.SystemF_SN]
step [inductive, in Plain.Demo]
step [inductive, in Ssr.pred_CC_omega]
step_pstep [lemma, in Ssr.CR]
step_lam [constructor, in Ssr.CR]
step_appR [constructor, in Ssr.CR]
step_appL [constructor, in Ssr.CR]
step_beta [constructor, in Ssr.CR]
step_hsubst [lemma, in Ssr.SystemF_SN]
step_subst [lemma, in Ssr.SystemF_SN]
step_substf [lemma, in Ssr.SystemF_SN]
step_einst [lemma, in Ssr.SystemF_SN]
step_ebeta [lemma, in Ssr.SystemF_SN]
step_tabs [constructor, in Ssr.SystemF_SN]
step_tapp [constructor, in Ssr.SystemF_SN]
step_abs [constructor, in Ssr.SystemF_SN]
step_appR [constructor, in Ssr.SystemF_SN]
step_appL [constructor, in Ssr.SystemF_SN]
step_inst [constructor, in Ssr.SystemF_SN]
step_beta [constructor, in Ssr.SystemF_SN]
Step_lam [constructor, in Plain.Demo]
Step_appR [constructor, in Plain.Demo]
Step_appL [constructor, in Plain.Demo]
Step_beta [constructor, in Plain.Demo]
step_pstep [lemma, in Ssr.pred_CC_omega]
step_subst [lemma, in Ssr.pred_CC_omega]
step_prodR [constructor, in Ssr.pred_CC_omega]
step_prodL [constructor, in Ssr.pred_CC_omega]
step_lam [constructor, in Ssr.pred_CC_omega]
step_appR [constructor, in Ssr.pred_CC_omega]
step_appL [constructor, in Ssr.pred_CC_omega]
step_beta [constructor, in Ssr.pred_CC_omega]
strong_normalization [lemma, in Ssr.SystemF_SN]
sty_up [lemma, in Ssr.pred_CC_omega]
sub [inductive, in Ssr.pred_CC_omega]
sub [inductive, in Plain.POPLmark]
sub [inductive, in Ssr.POPLmark]
SubI [constructor, in Ssr.pred_CC_omega]
subject_reduction [lemma, in Ssr.pred_CC_omega]
subst [projection, in Autosubst.Autosubst_Classes]
Subst [record, in Autosubst.Autosubst_Classes]
subst [constructor, in Autosubst.Autosubst_Classes]
Subst [inductive, in Autosubst.Autosubst_Classes]
SubstHSubstComp [record, in Autosubst.Autosubst_Classes]
SubstHSubstComp [inductive, in Autosubst.Autosubst_Classes]
SubstHSubstComp_type_term [instance, in Ssr.SystemF_SN]
SubstHSubstComp_type_term [instance, in Ssr.SystemF_CBV]
SubstHSubstComp_type_term [instance, in Plain.POPLmark]
SubstHSubstComp_type_term [instance, in Ssr.POPLmark]
SubstInstance [section, in Plain.Context]
substitutivity [lemma, in Plain.Demo]
SubstLemmas [record, in Autosubst.Autosubst_Classes]
SubstLemmas [section, in Autosubst.Autosubst_Lemmas]
SubstLemmas_term [instance, in Ssr.CR]
SubstLemmas_term [instance, in Ssr.SystemF_SN]
SubstLemmas_type [instance, in Ssr.SystemF_SN]
SubstLemmas_term [instance, in Ssr.SystemF_CBV]
SubstLemmas_type [instance, in Ssr.SystemF_CBV]
SubstLemmas_term [instance, in Plain.Demo]
substLemmas_term [instance, in Ssr.pred_CC_omega]
SubstLemmas_term [instance, in Plain.POPLmark]
SubstLemmas_type [instance, in Plain.POPLmark]
SubstLemmas_term [instance, in Ssr.BetaSubstitution]
SubstLemmas_term [instance, in Ssr.POPLmark]
SubstLemmas_type [instance, in Ssr.POPLmark]
Subst_term [instance, in Ssr.CR]
Subst_term [instance, in Ssr.SystemF_SN]
Subst_type [instance, in Ssr.SystemF_SN]
Subst_term [instance, in Ssr.SystemF_CBV]
Subst_type [instance, in Ssr.SystemF_CBV]
subst_hsubst_comp [projection, in Autosubst.Autosubst_Classes]
subst_hsubst_comp [constructor, in Autosubst.Autosubst_Classes]
subst_comp [projection, in Autosubst.Autosubst_Classes]
subst_id [projection, in Autosubst.Autosubst_Classes]
subst_compR [lemma, in Autosubst.Autosubst_Tactics]
subst_compX [lemma, in Autosubst.Autosubst_Tactics]
subst_compI [lemma, in Autosubst.Autosubst_Tactics]
subst_idX [lemma, in Autosubst.Autosubst_Tactics]
Subst_term [instance, in Plain.Demo]
Subst_term [instance, in Ssr.pred_CC_omega]
Subst_term [instance, in Plain.POPLmark]
Subst_type [instance, in Plain.POPLmark]
Subst_term [instance, in Ssr.BetaSubstitution]
Subst_term [instance, in Ssr.POPLmark]
Subst_type [instance, in Ssr.POPLmark]
sub_subst [lemma, in Ssr.pred_CC_omega]
sub_prod_inv [lemma, in Ssr.pred_CC_omega]
sub_trans [lemma, in Ssr.pred_CC_omega]
sub_sort [lemma, in Ssr.pred_CC_omega]
sub_refl [lemma, in Ssr.pred_CC_omega]
sub_subst [lemma, in Plain.POPLmark]
sub_narrow [lemma, in Plain.POPLmark]
sub_trans [lemma, in Plain.POPLmark]
sub_trans' [lemma, in Plain.POPLmark]
sub_wf_2 [lemma, in Plain.POPLmark]
sub_wf_1 [lemma, in Plain.POPLmark]
sub_wf [lemma, in Plain.POPLmark]
sub_weak1 [lemma, in Plain.POPLmark]
sub_weak [lemma, in Plain.POPLmark]
sub_refl [lemma, in Plain.POPLmark]
sub_subst [lemma, in Ssr.POPLmark]
sub_narrow [lemma, in Ssr.POPLmark]
sub_trans [lemma, in Ssr.POPLmark]
sub_trans_t [lemma, in Ssr.POPLmark]
sub_trans_snoc [lemma, in Ssr.POPLmark]
sub_narrow_t [lemma, in Ssr.POPLmark]
sub_weak [lemma, in Ssr.POPLmark]
sub_ren [lemma, in Ssr.POPLmark]
sub_refl [lemma, in Ssr.POPLmark]
sub_all [constructor, in Ssr.POPLmark]
sub_fun [constructor, in Ssr.POPLmark]
sub_var_trans [constructor, in Ssr.POPLmark]
sub_var_refl [constructor, in Ssr.POPLmark]
sub_top [constructor, in Ssr.POPLmark]
sub1 [inductive, in Ssr.pred_CC_omega]
sub1_subst [lemma, in Ssr.pred_CC_omega]
sub1_trans [lemma, in Ssr.pred_CC_omega]
sub1_conv [lemma, in Ssr.pred_CC_omega]
sub1_sub [lemma, in Ssr.pred_CC_omega]
sub1_prod [constructor, in Ssr.pred_CC_omega]
sub1_sort [constructor, in Ssr.pred_CC_omega]
sub1_refl [constructor, in Ssr.pred_CC_omega]
SystemF_CBV [library]
SystemF_SN [library]
T
TAbs [constructor, in Ssr.SystemF_SN]TAbs [constructor, in Ssr.SystemF_CBV]
TAbs [constructor, in Plain.POPLmark]
TAbs [constructor, in Ssr.POPLmark]
TApp [constructor, in Ssr.SystemF_SN]
TApp [constructor, in Ssr.SystemF_CBV]
TApp [constructor, in Plain.POPLmark]
TApp [constructor, in Ssr.POPLmark]
term [inductive, in Ssr.CR]
term [inductive, in Ssr.SystemF_SN]
term [inductive, in Ssr.SystemF_CBV]
term [inductive, in Plain.Demo]
term [inductive, in Ssr.pred_CC_omega]
term [inductive, in Plain.POPLmark]
term [inductive, in Ssr.BetaSubstitution]
term [inductive, in Ssr.POPLmark]
Termination [section, in Ssr.ARS]
Termination.cr [variable, in Ssr.ARS]
Termination.e [variable, in Ssr.ARS]
Termination.T [variable, in Ssr.ARS]
TeVar [constructor, in Ssr.SystemF_SN]
TeVar [constructor, in Ssr.SystemF_CBV]
TeVar [constructor, in Plain.POPLmark]
TeVar [constructor, in Ssr.POPLmark]
Top [constructor, in Plain.POPLmark]
Top [constructor, in Ssr.POPLmark]
transitivity_ren [lemma, in Ssr.POPLmark]
transitivity_proj [lemma, in Ssr.POPLmark]
transitivity_at [definition, in Ssr.POPLmark]
triangle [definition, in Ssr.ARS]
triangle_cofinal [lemma, in Ssr.ARS]
triangle_monotone [lemma, in Ssr.ARS]
triangle_diamond [lemma, in Ssr.ARS]
ty [inductive, in Plain.Demo]
ty [inductive, in Plain.POPLmark]
ty [inductive, in Ssr.POPLmark]
type [inductive, in Ssr.SystemF_SN]
type [inductive, in Ssr.SystemF_CBV]
type [inductive, in Plain.Demo]
type [inductive, in Plain.POPLmark]
type [inductive, in Ssr.POPLmark]
type_L [lemma, in Ssr.SystemF_SN]
TyVar [constructor, in Ssr.SystemF_SN]
TyVar [constructor, in Ssr.SystemF_CBV]
TyVar [constructor, in Plain.POPLmark]
TyVar [constructor, in Ssr.POPLmark]
ty_tapp [constructor, in Ssr.SystemF_SN]
ty_tabs [constructor, in Ssr.SystemF_SN]
ty_app [constructor, in Ssr.SystemF_SN]
ty_abs [constructor, in Ssr.SystemF_SN]
ty_var [constructor, in Ssr.SystemF_SN]
ty_tapp [constructor, in Ssr.SystemF_CBV]
ty_tabs [constructor, in Ssr.SystemF_CBV]
ty_app [constructor, in Ssr.SystemF_CBV]
ty_abs [constructor, in Ssr.SystemF_CBV]
ty_var [constructor, in Ssr.SystemF_CBV]
ty_pres [lemma, in Plain.Demo]
ty_subst [lemma, in Plain.Demo]
ty_ren [lemma, in Plain.Demo]
Ty_App [constructor, in Plain.Demo]
Ty_Lam [constructor, in Plain.Demo]
Ty_Var [constructor, in Plain.Demo]
ty_lam_inv [lemma, in Ssr.pred_CC_omega]
ty_lam_invX [lemma, in Ssr.pred_CC_omega]
ty_prod_inv [lemma, in Ssr.pred_CC_omega]
ty_prod_invX [lemma, in Ssr.pred_CC_omega]
ty_ctx_conv [lemma, in Ssr.pred_CC_omega]
ty_cut [lemma, in Ssr.pred_CC_omega]
ty_subst [lemma, in Ssr.pred_CC_omega]
ty_ok [lemma, in Ssr.pred_CC_omega]
ty_renaming [lemma, in Ssr.pred_CC_omega]
ty_prod_wf [lemma, in Ssr.pred_CC_omega]
ty_sort_wf [lemma, in Ssr.pred_CC_omega]
ty_eapp [lemma, in Ssr.pred_CC_omega]
ty_evar [lemma, in Ssr.pred_CC_omega]
ty_sub [constructor, in Ssr.pred_CC_omega]
ty_prod [constructor, in Ssr.pred_CC_omega]
ty_lam [constructor, in Ssr.pred_CC_omega]
ty_app [constructor, in Ssr.pred_CC_omega]
ty_sort [constructor, in Ssr.pred_CC_omega]
ty_var [constructor, in Ssr.pred_CC_omega]
ty_inv_tabs [lemma, in Plain.POPLmark]
ty_inv_abs [lemma, in Plain.POPLmark]
ty_subst_term [lemma, in Plain.POPLmark]
ty_subst [lemma, in Plain.POPLmark]
ty_narrow [lemma, in Plain.POPLmark]
ty_weak_ter1 [lemma, in Plain.POPLmark]
ty_weak_ter [lemma, in Plain.POPLmark]
ty_weak_ty' [lemma, in Plain.POPLmark]
ty_weak_ty [lemma, in Plain.POPLmark]
ty_weak [lemma, in Plain.POPLmark]
ty_inv_tabs [lemma, in Ssr.POPLmark]
ty_inv_tabs' [lemma, in Ssr.POPLmark]
ty_inv_abs [lemma, in Ssr.POPLmark]
ty_inv_abs' [lemma, in Ssr.POPLmark]
ty_betaT [lemma, in Ssr.POPLmark]
ty_narrowT [lemma, in Ssr.POPLmark]
ty_beta [lemma, in Ssr.POPLmark]
ty_narrow [lemma, in Ssr.POPLmark]
ty_subst [lemma, in Ssr.POPLmark]
ty_tweak [lemma, in Ssr.POPLmark]
ty_hsubst [lemma, in Ssr.POPLmark]
ty_weak [lemma, in Ssr.POPLmark]
ty_ren [lemma, in Ssr.POPLmark]
ty_etapp [lemma, in Ssr.POPLmark]
ty_evar [lemma, in Ssr.POPLmark]
ty_sub [constructor, in Ssr.POPLmark]
ty_tapp [constructor, in Ssr.POPLmark]
ty_tabs [constructor, in Ssr.POPLmark]
ty_app [constructor, in Ssr.POPLmark]
ty_abs [constructor, in Ssr.POPLmark]
ty_var [constructor, in Ssr.POPLmark]
T_Sub [constructor, in Plain.POPLmark]
T_TApp [constructor, in Plain.POPLmark]
T_TAbs [constructor, in Plain.POPLmark]
T_App [constructor, in Plain.POPLmark]
T_Abs [constructor, in Plain.POPLmark]
T_Var [constructor, in Plain.POPLmark]
U
up [definition, in Autosubst.Autosubst_Classes]upE [lemma, in Autosubst.Autosubst_Tactics]
upn [abbreviation, in Autosubst.Autosubst_Classes]
upnP [lemma, in Ssr.BetaSubstitution]
upnSE [lemma, in Autosubst.Autosubst_Tactics]
upnSX [lemma, in Autosubst.Autosubst_Tactics]
upn0 [lemma, in Autosubst.Autosubst_Tactics]
upren [definition, in Autosubst.Autosubst_Classes]
upX [lemma, in Autosubst.Autosubst_Tactics]
up_atnd [lemma, in Plain.Context]
up_mmap_atn [lemma, in Plain.Context]
up_comp_n [lemma, in Autosubst.Autosubst_Lemmas]
up_comp [lemma, in Autosubst.Autosubst_Lemmas]
up_liftn [lemma, in Autosubst.Autosubst_Lemmas]
up_lift1 [lemma, in Autosubst.Autosubst_Lemmas]
up_id_n [lemma, in Autosubst.Autosubst_Lemmas]
up_id [lemma, in Autosubst.Autosubst_Lemmas]
up_hcomp_n_internal [lemma, in Autosubst.Autosubst_Derive]
up_hcomp_internal [lemma, in Autosubst.Autosubst_Derive]
up_comp_n_internal [lemma, in Autosubst.Autosubst_Derive]
up_comp_internal [lemma, in Autosubst.Autosubst_Derive]
up_comp_subst_ren_n_internal [lemma, in Autosubst.Autosubst_Derive]
up_comp_subst_ren_internal [lemma, in Autosubst.Autosubst_Derive]
up_comp_ren_subst_n [lemma, in Autosubst.Autosubst_Derive]
up_comp_ren_subst [lemma, in Autosubst.Autosubst_Derive]
up_id_n_internal [lemma, in Autosubst.Autosubst_Derive]
up_id_internal [lemma, in Autosubst.Autosubst_Derive]
up_upren_n_internal [lemma, in Autosubst.Autosubst_Derive]
up_upren_internal [lemma, in Autosubst.Autosubst_Derive]
V
V [definition, in Ssr.SystemF_CBV]value [inductive, in Plain.POPLmark]
value [definition, in Ssr.POPLmark]
Value_TAbs [constructor, in Plain.POPLmark]
Value_Abs [constructor, in Plain.POPLmark]
Var [constructor, in Ssr.CR]
var [definition, in Autosubst.Autosubst_Basics]
Var [constructor, in Plain.Demo]
Var [constructor, in Ssr.pred_CC_omega]
Var [constructor, in Ssr.BetaSubstitution]
VG [definition, in Ssr.SystemF_CBV]
V_subst [lemma, in Ssr.SystemF_CBV]
V_ren [lemma, in Ssr.SystemF_CBV]
V_to_E [lemma, in Ssr.SystemF_CBV]
V_value [lemma, in Ssr.SystemF_CBV]
W
weakening [lemma, in Ssr.pred_CC_omega]wf_subst [lemma, in Plain.POPLmark]
wf_weak' [lemma, in Plain.POPLmark]
wf_weak1 [lemma, in Plain.POPLmark]
wf_weak [lemma, in Plain.POPLmark]
wf_ty [definition, in Plain.POPLmark]
wn [definition, in Ssr.ARS]
wn_accn [lemma, in Ssr.ARS]
_
_bind [definition, in Autosubst.Autosubst_Classes]other
{ bind _ } (bind_scope) [notation, in Autosubst.Autosubst_Classes]{ bind _ in _ } (bind_scope) [notation, in Autosubst.Autosubst_Classes]
{ bind _ of _ } (bind_scope) [notation, in Autosubst.Autosubst_Classes]
{ bind _ of _ in _ } (bind_scope) [notation, in Autosubst.Autosubst_Classes]
_ <=>2 _ (prop_scope) [notation, in Ssr.ARS]
_ <=2 _ (prop_scope) [notation, in Ssr.ARS]
_ ..|[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ ..|[ _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ ..|[ _ ] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ .|[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ .|[ _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ .|[ _ ] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ >>| _ (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ ..[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ ..[ _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ ..[ _ ] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ .[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ .[ _ /] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ .[ _ ] (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ >> _ (subst_scope) [notation, in Autosubst.Autosubst_Classes]
_ .: _ (subst_scope) [notation, in Autosubst.Autosubst_Basics]
_ >>> _ (subst_scope) [notation, in Autosubst.Autosubst_Basics]
_ === _ [notation, in Ssr.CR]
_ `_ _ [notation, in Ssr.SystemF_SN]
_ `_ _ [notation, in Ssr.SystemF_CBV]
_ `_ _ [notation, in Ssr.pred_CC_omega]
_ <: _ [notation, in Ssr.pred_CC_omega]
_ === _ [notation, in Ssr.pred_CC_omega]
_ ``_ _ [notation, in Ssr.POPLmark]
_ `_ _ [notation, in Ssr.POPLmark]
EV _ => _ [notation, in Plain.POPLmark]
EV _ => _ [notation, in Ssr.POPLmark]
SUB _ |- _ <: _ [notation, in Plain.POPLmark]
SUB _ |- _ <: _ [notation, in Ssr.POPLmark]
TY _ ; _ |- _ : _ [notation, in Plain.POPLmark]
TY _ ; _ |- _ : _ [notation, in Ssr.POPLmark]
( + _ ) [notation, in Autosubst.Autosubst_Basics]
[ _ |- _ -| _ ] [notation, in Ssr.pred_CC_omega]
[ _ |- _ ] [notation, in Ssr.pred_CC_omega]
[ _ |- ] [notation, in Ssr.pred_CC_omega]
[ _ |- _ :- _ ] [notation, in Ssr.pred_CC_omega]
Notation Index
other
{ bind _ } (bind_scope) [in Autosubst.Autosubst_Classes]{ bind _ in _ } (bind_scope) [in Autosubst.Autosubst_Classes]
{ bind _ of _ } (bind_scope) [in Autosubst.Autosubst_Classes]
{ bind _ of _ in _ } (bind_scope) [in Autosubst.Autosubst_Classes]
_ <=>2 _ (prop_scope) [in Ssr.ARS]
_ <=2 _ (prop_scope) [in Ssr.ARS]
_ ..|[ _ , _ , .. , _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ ..|[ _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ ..|[ _ ] (subst_scope) [in Autosubst.Autosubst_Classes]
_ .|[ _ , _ , .. , _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ .|[ _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ .|[ _ ] (subst_scope) [in Autosubst.Autosubst_Classes]
_ >>| _ (subst_scope) [in Autosubst.Autosubst_Classes]
_ ..[ _ , _ , .. , _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ ..[ _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ ..[ _ ] (subst_scope) [in Autosubst.Autosubst_Classes]
_ .[ _ , _ , .. , _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ .[ _ /] (subst_scope) [in Autosubst.Autosubst_Classes]
_ .[ _ ] (subst_scope) [in Autosubst.Autosubst_Classes]
_ >> _ (subst_scope) [in Autosubst.Autosubst_Classes]
_ .: _ (subst_scope) [in Autosubst.Autosubst_Basics]
_ >>> _ (subst_scope) [in Autosubst.Autosubst_Basics]
_ === _ [in Ssr.CR]
_ `_ _ [in Ssr.SystemF_SN]
_ `_ _ [in Ssr.SystemF_CBV]
_ `_ _ [in Ssr.pred_CC_omega]
_ <: _ [in Ssr.pred_CC_omega]
_ === _ [in Ssr.pred_CC_omega]
_ ``_ _ [in Ssr.POPLmark]
_ `_ _ [in Ssr.POPLmark]
EV _ => _ [in Plain.POPLmark]
EV _ => _ [in Ssr.POPLmark]
SUB _ |- _ <: _ [in Plain.POPLmark]
SUB _ |- _ <: _ [in Ssr.POPLmark]
TY _ ; _ |- _ : _ [in Plain.POPLmark]
TY _ ; _ |- _ : _ [in Ssr.POPLmark]
( + _ ) [in Autosubst.Autosubst_Basics]
[ _ |- _ -| _ ] [in Ssr.pred_CC_omega]
[ _ |- _ ] [in Ssr.pred_CC_omega]
[ _ |- ] [in Ssr.pred_CC_omega]
[ _ |- _ :- _ ] [in Ssr.pred_CC_omega]
Variable Index
C
CoFinal.e [in Ssr.ARS]CoFinal.rho [in Ssr.ARS]
CoFinal.T [in Ssr.ARS]
CoFinal.tri [in Ssr.ARS]
Commutation.T [in Ssr.ARS]
ComputationN.classical [in Ssr.ARS]
ComputationN.e [in Ssr.ARS]
ComputationN.norm [in Ssr.ARS]
ComputationN.rho [in Ssr.ARS]
ComputationN.sound [in Ssr.ARS]
ComputationN.T [in Ssr.ARS]
D
Definitions.e [in Ssr.ARS]Definitions.T [in Ssr.ARS]
M
MMapInstances.A [in Ssr.AutosubstSsr]MMapInstances.A [in Autosubst.Autosubst_MMapInstances]
MMapInstances.B [in Ssr.AutosubstSsr]
MMapInstances.B [in Autosubst.Autosubst_MMapInstances]
MMapInstances.C [in Ssr.AutosubstSsr]
MMapInstances.C [in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapExt_A_C [in Ssr.AutosubstSsr]
MMapInstances.MMapExt_A_B [in Ssr.AutosubstSsr]
MMapInstances.MMapExt_A_C [in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapExt_A_B [in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_C [in Ssr.AutosubstSsr]
MMapInstances.MMapLemmas_A_B [in Ssr.AutosubstSsr]
MMapInstances.MMapLemmas_A_C [in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_B [in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMap_A_C [in Ssr.AutosubstSsr]
MMapInstances.MMap_A_B [in Ssr.AutosubstSsr]
MMapInstances.MMap_A_C [in Autosubst.Autosubst_MMapInstances]
MMapInstances.MMap_A_B [in Autosubst.Autosubst_MMapInstances]
T
Termination.cr [in Ssr.ARS]Termination.e [in Ssr.ARS]
Termination.T [in Ssr.ARS]
Library Index
A
ARSAutosubst
AutosubstSsr
Autosubst_Lemmas
Autosubst_Tactics
Autosubst_Derive
Autosubst_Basics
Autosubst_Classes
Autosubst_MMap
Autosubst_MMapInstances
B
BetaSubstitutionC
ContextContext
CR
D
DecidableDemo
P
POPLmarkPOPLmark
pred_CC_omega
S
SizeSystemF_CBV
SystemF_SN
Lemma Index
A
accn_inv [in Ssr.ARS]ad_cons [in Ssr.SystemF_SN]
atnd_defined [in Plain.Context]
atnd_repl [in Plain.Context]
atnd_step [in Plain.Context]
atnd_steps' [in Plain.Context]
atnd_steps [in Plain.Context]
atn_mmap [in Plain.Context]
B
beta_expansion [in Ssr.SystemF_SN]C
canonical_all [in Ssr.POPLmark]canonical_all' [in Ssr.POPLmark]
canonical_arr [in Ssr.POPLmark]
canonical_arr' [in Ssr.POPLmark]
can_form_all [in Plain.POPLmark]
can_form_arr [in Plain.POPLmark]
church_rosser [in Ssr.CR]
church_rosser [in Ssr.pred_CC_omega]
cofinal_normalizing [in Ssr.ARS]
compA [in Autosubst.Autosubst_Basics]
comp_id [in Autosubst.Autosubst_Basics]
com_lift [in Ssr.ARS]
com_strip [in Ssr.ARS]
confluent_stable [in Ssr.ARS]
confluent_cr [in Ssr.ARS]
conj' [in Plain.POPLmark]
consistency [in Ssr.SystemF_CBV]
convES [in Ssr.ARS]
convESi [in Ssr.ARS]
conv_sub [in Ssr.pred_CC_omega]
conv_sub1 [in Ssr.pred_CC_omega]
conv_prod_sort [in Ssr.pred_CC_omega]
conv_beta [in Ssr.pred_CC_omega]
conv_compat [in Ssr.pred_CC_omega]
conv_subst [in Ssr.pred_CC_omega]
conv_prod [in Ssr.pred_CC_omega]
conv_lam [in Ssr.pred_CC_omega]
conv_app [in Ssr.pred_CC_omega]
conv_closure [in Ssr.ARS]
conv_hom [in Ssr.ARS]
conv_img [in Ssr.ARS]
conv_sym [in Ssr.ARS]
conv_trans [in Ssr.ARS]
conv1 [in Ssr.ARS]
conv1i [in Ssr.ARS]
cr_method [in Ssr.ARS]
cr_conv_normal [in Ssr.ARS]
cr_star_normal [in Ssr.ARS]
D
diamond_confluent [in Ssr.ARS]E
equal_f [in Autosubst.Autosubst_Basics]eq_V [in Ssr.SystemF_CBV]
eq_star [in Ssr.ARS]
evalnP [in Ssr.ARS]
evaln_sound [in Ssr.ARS]
ev_progress [in Plain.POPLmark]
ev_progress [in Ssr.POPLmark]
ev_progress' [in Ssr.POPLmark]
eweakening [in Ssr.pred_CC_omega]
extend_ext [in Ssr.SystemF_SN]
E_ren [in Ssr.SystemF_CBV]
F
fold_upn_up [in Autosubst.Autosubst_Tactics]fold_up_upn [in Autosubst.Autosubst_Tactics]
fold_up_up [in Autosubst.Autosubst_Tactics]
fold_up0 [in Autosubst.Autosubst_Tactics]
fold_up [in Autosubst.Autosubst_Tactics]
fold_ren_cons [in Autosubst.Autosubst_Tactics]
G
get_map [in Ssr.Context]H
hcomp_dist_internal [in Autosubst.Autosubst_Derive]hcomp_ren_internal [in Autosubst.Autosubst_Derive]
hcomp_lift_internal [in Autosubst.Autosubst_Derive]
hcomp_lift_n_internal [in Autosubst.Autosubst_Derive]
hsubst_compR [in Autosubst.Autosubst_Tactics]
hsubst_compX [in Autosubst.Autosubst_Tactics]
hsubst_compI [in Autosubst.Autosubst_Tactics]
hsubst_idX [in Autosubst.Autosubst_Tactics]
I
id_hsubstR [in Autosubst.Autosubst_Tactics]id_hsubstX [in Autosubst.Autosubst_Tactics]
id_scompR [in Autosubst.Autosubst_Tactics]
id_scompX [in Autosubst.Autosubst_Tactics]
id_comp [in Autosubst.Autosubst_Basics]
inj_prod [in Ssr.pred_CC_omega]
inj_sort [in Ssr.pred_CC_omega]
inst_expansion [in Ssr.SystemF_SN]
iterate_Sr [in Autosubst.Autosubst_Basics]
iterate_0 [in Autosubst.Autosubst_Basics]
iterate_S [in Autosubst.Autosubst_Basics]
iter_param [in Autosubst.Autosubst_Derive]
iter_fp [in Autosubst.Autosubst_Derive]
J
join_conv [in Ssr.ARS]L
lift_eta [in Autosubst.Autosubst_Basics]lift_compR [in Autosubst.Autosubst_Basics]
lift_comp [in Autosubst.Autosubst_Basics]
lift_scons [in Autosubst.Autosubst_Basics]
lift_injn [in Autosubst.Autosubst_Lemmas]
lift_inj [in Autosubst.Autosubst_Lemmas]
lift_sound [in Ssr.BetaSubstitution]
lift_at_sound [in Ssr.BetaSubstitution]
lift0 [in Autosubst.Autosubst_Basics]
lift0 [in Autosubst.Autosubst_Lemmas]
L_subst [in Ssr.SystemF_SN]
L_weaken [in Ssr.SystemF_SN]
L_ren [in Ssr.SystemF_SN]
L_ext [in Ssr.SystemF_SN]
L_cl_star [in Ssr.SystemF_SN]
L_var [in Ssr.SystemF_SN]
L_nc [in Ssr.SystemF_SN]
L_cl [in Ssr.SystemF_SN]
L_sn [in Ssr.SystemF_SN]
L_reducible [in Ssr.SystemF_SN]
M
mmap_atn [in Plain.Context]mmap_id_ext [in Autosubst.Autosubst_Derive]
mmap_const_instE [in Autosubst.Autosubst_MMap]
mmap_id_instE [in Autosubst.Autosubst_MMap]
mmap_compR [in Autosubst.Autosubst_MMap]
mmap_compX [in Autosubst.Autosubst_MMap]
mmap_idX [in Autosubst.Autosubst_MMap]
N
nf_accn [in Ssr.ARS]normalization [in Ssr.SystemF_CBV]
normal_step_sort [in Ssr.pred_CC_omega]
normal_star [in Ssr.ARS]
P
plusA [in Autosubst.Autosubst_Basics]plusnO [in Autosubst.Autosubst_Basics]
plusnS [in Autosubst.Autosubst_Basics]
plusOn [in Autosubst.Autosubst_Basics]
plusSn [in Autosubst.Autosubst_Basics]
preservation [in Plain.POPLmark]
preservation [in Ssr.POPLmark]
propagation [in Ssr.pred_CC_omega]
psstep_up [in Ssr.CR]
psstep_up [in Ssr.pred_CC_omega]
pstep_compat_beta [in Ssr.CR]
pstep_compat [in Ssr.CR]
pstep_subst [in Ssr.CR]
pstep_red [in Ssr.CR]
pstep_refl [in Ssr.CR]
pstep_ebeta [in Ssr.CR]
pstep_compat_beta [in Ssr.pred_CC_omega]
pstep_compat [in Ssr.pred_CC_omega]
pstep_subst [in Ssr.pred_CC_omega]
pstep_red [in Ssr.pred_CC_omega]
pstep_refl [in Ssr.pred_CC_omega]
R
reducible_var [in Ssr.SystemF_SN]reducible_sn [in Ssr.SystemF_SN]
red_lam [in Ssr.CR]
red_app [in Ssr.CR]
red_beta [in Ssr.SystemF_SN]
red_compat [in Ssr.SystemF_SN]
red_hsubst [in Ssr.SystemF_SN]
red_subst [in Ssr.SystemF_SN]
red_tabs [in Ssr.SystemF_SN]
red_tapp [in Ssr.SystemF_SN]
red_abs [in Ssr.SystemF_SN]
red_app [in Ssr.SystemF_SN]
red_prod_inv [in Ssr.pred_CC_omega]
red_compat [in Ssr.pred_CC_omega]
red_subst [in Ssr.pred_CC_omega]
red_prod [in Ssr.pred_CC_omega]
red_lam [in Ssr.pred_CC_omega]
red_app [in Ssr.pred_CC_omega]
rename_substX [in Autosubst.Autosubst_Tactics]
renS [in Autosubst.Autosubst_Lemmas]
ren_uncomp [in Autosubst.Autosubst_Lemmas]
ren_size_inv [in Plain.POPLmark]
rho_triangle [in Ssr.CR]
rho_id [in Ssr.SystemF_SN]
rho_triangle [in Ssr.pred_CC_omega]
S
sbst_sound [in Ssr.BetaSubstitution]sbst_at_sound [in Ssr.BetaSubstitution]
scomp_hcompR [in Autosubst.Autosubst_Tactics]
scomp_hcompX [in Autosubst.Autosubst_Tactics]
scomp_hcompI [in Autosubst.Autosubst_Tactics]
scons_eta [in Autosubst.Autosubst_Basics]
scons_comp [in Autosubst.Autosubst_Basics]
sconv_up [in Ssr.pred_CC_omega]
size_In [in Plain.Size]
size_app [in Plain.Size]
size_ind2 [in Plain.Size]
size_rec [in Plain.Size]
sn_hsubst [in Ssr.SystemF_SN]
sn_subst [in Ssr.SystemF_SN]
sn_tclosed [in Ssr.SystemF_SN]
sn_closed [in Ssr.SystemF_SN]
sn_wn [in Ssr.ARS]
sn_preimage [in Ssr.ARS]
soundness [in Ssr.SystemF_SN]
soundness [in Ssr.SystemF_CBV]
soundness_nil [in Ssr.SystemF_CBV]
sred_hup [in Ssr.SystemF_SN]
sred_up [in Ssr.SystemF_SN]
sred_up [in Ssr.pred_CC_omega]
starES [in Ssr.ARS]
star_interpolation [in Ssr.ARS]
star_monotone [in Ssr.ARS]
star_closure [in Ssr.ARS]
star_hom [in Ssr.ARS]
star_img [in Ssr.ARS]
star_conv [in Ssr.ARS]
star_trans [in Ssr.ARS]
star1 [in Ssr.ARS]
step_pstep [in Ssr.CR]
step_hsubst [in Ssr.SystemF_SN]
step_subst [in Ssr.SystemF_SN]
step_substf [in Ssr.SystemF_SN]
step_einst [in Ssr.SystemF_SN]
step_ebeta [in Ssr.SystemF_SN]
step_pstep [in Ssr.pred_CC_omega]
step_subst [in Ssr.pred_CC_omega]
strong_normalization [in Ssr.SystemF_SN]
sty_up [in Ssr.pred_CC_omega]
subject_reduction [in Ssr.pred_CC_omega]
substitutivity [in Plain.Demo]
subst_compR [in Autosubst.Autosubst_Tactics]
subst_compX [in Autosubst.Autosubst_Tactics]
subst_compI [in Autosubst.Autosubst_Tactics]
subst_idX [in Autosubst.Autosubst_Tactics]
sub_subst [in Ssr.pred_CC_omega]
sub_prod_inv [in Ssr.pred_CC_omega]
sub_trans [in Ssr.pred_CC_omega]
sub_sort [in Ssr.pred_CC_omega]
sub_refl [in Ssr.pred_CC_omega]
sub_subst [in Plain.POPLmark]
sub_narrow [in Plain.POPLmark]
sub_trans [in Plain.POPLmark]
sub_trans' [in Plain.POPLmark]
sub_wf_2 [in Plain.POPLmark]
sub_wf_1 [in Plain.POPLmark]
sub_wf [in Plain.POPLmark]
sub_weak1 [in Plain.POPLmark]
sub_weak [in Plain.POPLmark]
sub_refl [in Plain.POPLmark]
sub_subst [in Ssr.POPLmark]
sub_narrow [in Ssr.POPLmark]
sub_trans [in Ssr.POPLmark]
sub_trans_t [in Ssr.POPLmark]
sub_trans_snoc [in Ssr.POPLmark]
sub_narrow_t [in Ssr.POPLmark]
sub_weak [in Ssr.POPLmark]
sub_ren [in Ssr.POPLmark]
sub_refl [in Ssr.POPLmark]
sub1_subst [in Ssr.pred_CC_omega]
sub1_trans [in Ssr.pred_CC_omega]
sub1_conv [in Ssr.pred_CC_omega]
sub1_sub [in Ssr.pred_CC_omega]
T
transitivity_ren [in Ssr.POPLmark]transitivity_proj [in Ssr.POPLmark]
triangle_cofinal [in Ssr.ARS]
triangle_monotone [in Ssr.ARS]
triangle_diamond [in Ssr.ARS]
type_L [in Ssr.SystemF_SN]
ty_pres [in Plain.Demo]
ty_subst [in Plain.Demo]
ty_ren [in Plain.Demo]
ty_lam_inv [in Ssr.pred_CC_omega]
ty_lam_invX [in Ssr.pred_CC_omega]
ty_prod_inv [in Ssr.pred_CC_omega]
ty_prod_invX [in Ssr.pred_CC_omega]
ty_ctx_conv [in Ssr.pred_CC_omega]
ty_cut [in Ssr.pred_CC_omega]
ty_subst [in Ssr.pred_CC_omega]
ty_ok [in Ssr.pred_CC_omega]
ty_renaming [in Ssr.pred_CC_omega]
ty_prod_wf [in Ssr.pred_CC_omega]
ty_sort_wf [in Ssr.pred_CC_omega]
ty_eapp [in Ssr.pred_CC_omega]
ty_evar [in Ssr.pred_CC_omega]
ty_inv_tabs [in Plain.POPLmark]
ty_inv_abs [in Plain.POPLmark]
ty_subst_term [in Plain.POPLmark]
ty_subst [in Plain.POPLmark]
ty_narrow [in Plain.POPLmark]
ty_weak_ter1 [in Plain.POPLmark]
ty_weak_ter [in Plain.POPLmark]
ty_weak_ty' [in Plain.POPLmark]
ty_weak_ty [in Plain.POPLmark]
ty_weak [in Plain.POPLmark]
ty_inv_tabs [in Ssr.POPLmark]
ty_inv_tabs' [in Ssr.POPLmark]
ty_inv_abs [in Ssr.POPLmark]
ty_inv_abs' [in Ssr.POPLmark]
ty_betaT [in Ssr.POPLmark]
ty_narrowT [in Ssr.POPLmark]
ty_beta [in Ssr.POPLmark]
ty_narrow [in Ssr.POPLmark]
ty_subst [in Ssr.POPLmark]
ty_tweak [in Ssr.POPLmark]
ty_hsubst [in Ssr.POPLmark]
ty_weak [in Ssr.POPLmark]
ty_ren [in Ssr.POPLmark]
ty_etapp [in Ssr.POPLmark]
ty_evar [in Ssr.POPLmark]
U
upE [in Autosubst.Autosubst_Tactics]upnP [in Ssr.BetaSubstitution]
upnSE [in Autosubst.Autosubst_Tactics]
upnSX [in Autosubst.Autosubst_Tactics]
upn0 [in Autosubst.Autosubst_Tactics]
upX [in Autosubst.Autosubst_Tactics]
up_atnd [in Plain.Context]
up_mmap_atn [in Plain.Context]
up_comp_n [in Autosubst.Autosubst_Lemmas]
up_comp [in Autosubst.Autosubst_Lemmas]
up_liftn [in Autosubst.Autosubst_Lemmas]
up_lift1 [in Autosubst.Autosubst_Lemmas]
up_id_n [in Autosubst.Autosubst_Lemmas]
up_id [in Autosubst.Autosubst_Lemmas]
up_hcomp_n_internal [in Autosubst.Autosubst_Derive]
up_hcomp_internal [in Autosubst.Autosubst_Derive]
up_comp_n_internal [in Autosubst.Autosubst_Derive]
up_comp_internal [in Autosubst.Autosubst_Derive]
up_comp_subst_ren_n_internal [in Autosubst.Autosubst_Derive]
up_comp_subst_ren_internal [in Autosubst.Autosubst_Derive]
up_comp_ren_subst_n [in Autosubst.Autosubst_Derive]
up_comp_ren_subst [in Autosubst.Autosubst_Derive]
up_id_n_internal [in Autosubst.Autosubst_Derive]
up_id_internal [in Autosubst.Autosubst_Derive]
up_upren_n_internal [in Autosubst.Autosubst_Derive]
up_upren_internal [in Autosubst.Autosubst_Derive]
V
V_subst [in Ssr.SystemF_CBV]V_ren [in Ssr.SystemF_CBV]
V_to_E [in Ssr.SystemF_CBV]
V_value [in Ssr.SystemF_CBV]
W
weakening [in Ssr.pred_CC_omega]wf_subst [in Plain.POPLmark]
wf_weak' [in Plain.POPLmark]
wf_weak1 [in Plain.POPLmark]
wf_weak [in Plain.POPLmark]
wn_accn [in Ssr.ARS]
Constructor Index
A
Abs [in Ssr.SystemF_SN]Abs [in Ssr.SystemF_CBV]
Abs [in Plain.POPLmark]
Abs [in Ssr.POPLmark]
accnH [in Ssr.ARS]
accnL [in Ssr.ARS]
All [in Ssr.SystemF_SN]
All [in Ssr.SystemF_CBV]
All [in Plain.POPLmark]
All [in Ssr.POPLmark]
App [in Ssr.CR]
App [in Ssr.SystemF_SN]
App [in Ssr.SystemF_CBV]
App [in Plain.Demo]
App [in Ssr.pred_CC_omega]
App [in Plain.POPLmark]
App [in Ssr.BetaSubstitution]
App [in Ssr.POPLmark]
Arr [in Ssr.SystemF_SN]
Arr [in Ssr.SystemF_CBV]
Arr [in Plain.Demo]
Arr [in Plain.POPLmark]
Arr [in Ssr.POPLmark]
AtndS [in Plain.Context]
Atnd0 [in Plain.Context]
B
Base [in Plain.Demo]C
convR [in Ssr.ARS]convSE [in Ssr.ARS]
convSEi [in Ssr.ARS]
ctx_ncons [in Ssr.pred_CC_omega]
ctx_nil [in Ssr.pred_CC_omega]
D
decide [in Plain.Decidable]E
eval_tabs [in Ssr.SystemF_CBV]eval_abs [in Ssr.SystemF_CBV]
eval_tbeta [in Ssr.SystemF_CBV]
eval_beta [in Ssr.SystemF_CBV]
E_TypeFun [in Plain.POPLmark]
E_AppArg [in Plain.POPLmark]
E_AppFun [in Plain.POPLmark]
E_TAppTAbs [in Plain.POPLmark]
E_AppAbs [in Plain.POPLmark]
E_TypeFun [in Ssr.POPLmark]
E_AppArg [in Ssr.POPLmark]
E_AppFun [in Ssr.POPLmark]
E_TAppTAbs [in Ssr.POPLmark]
E_AppAbs [in Ssr.POPLmark]
H
hsubst [in Autosubst.Autosubst_Classes]hsubst_hsubst_ind [in Autosubst.Autosubst_Classes]
hsubst_hsubst_comp [in Autosubst.Autosubst_Classes]
I
ids [in Autosubst.Autosubst_Classes]L
Lam [in Ssr.CR]Lam [in Plain.Demo]
Lam [in Ssr.pred_CC_omega]
Lam [in Ssr.BetaSubstitution]
M
mmap [in Autosubst.Autosubst_MMap]mmap_ext [in Autosubst.Autosubst_MMap]
P
Prod [in Ssr.pred_CC_omega]pstep_lam [in Ssr.CR]
pstep_app [in Ssr.CR]
pstep_var [in Ssr.CR]
pstep_beta [in Ssr.CR]
pstep_prod [in Ssr.pred_CC_omega]
pstep_lam [in Ssr.pred_CC_omega]
pstep_app [in Ssr.pred_CC_omega]
pstep_sort [in Ssr.pred_CC_omega]
pstep_var [in Ssr.pred_CC_omega]
pstep_beta [in Ssr.pred_CC_omega]
R
RedProdSpecI [in Ssr.pred_CC_omega]rename [in Autosubst.Autosubst_Classes]
S
SA_All [in Plain.POPLmark]SA_Arrow [in Plain.POPLmark]
SA_Trans [in Plain.POPLmark]
SA_Refl [in Plain.POPLmark]
SA_Top [in Plain.POPLmark]
size [in Plain.Size]
size_fact [in Plain.Size]
SNI [in Ssr.ARS]
Sort [in Ssr.pred_CC_omega]
starR [in Ssr.ARS]
starSE [in Ssr.ARS]
step_lam [in Ssr.CR]
step_appR [in Ssr.CR]
step_appL [in Ssr.CR]
step_beta [in Ssr.CR]
step_tabs [in Ssr.SystemF_SN]
step_tapp [in Ssr.SystemF_SN]
step_abs [in Ssr.SystemF_SN]
step_appR [in Ssr.SystemF_SN]
step_appL [in Ssr.SystemF_SN]
step_inst [in Ssr.SystemF_SN]
step_beta [in Ssr.SystemF_SN]
Step_lam [in Plain.Demo]
Step_appR [in Plain.Demo]
Step_appL [in Plain.Demo]
Step_beta [in Plain.Demo]
step_prodR [in Ssr.pred_CC_omega]
step_prodL [in Ssr.pred_CC_omega]
step_lam [in Ssr.pred_CC_omega]
step_appR [in Ssr.pred_CC_omega]
step_appL [in Ssr.pred_CC_omega]
step_beta [in Ssr.pred_CC_omega]
SubI [in Ssr.pred_CC_omega]
subst [in Autosubst.Autosubst_Classes]
subst_hsubst_comp [in Autosubst.Autosubst_Classes]
sub_all [in Ssr.POPLmark]
sub_fun [in Ssr.POPLmark]
sub_var_trans [in Ssr.POPLmark]
sub_var_refl [in Ssr.POPLmark]
sub_top [in Ssr.POPLmark]
sub1_prod [in Ssr.pred_CC_omega]
sub1_sort [in Ssr.pred_CC_omega]
sub1_refl [in Ssr.pred_CC_omega]
T
TAbs [in Ssr.SystemF_SN]TAbs [in Ssr.SystemF_CBV]
TAbs [in Plain.POPLmark]
TAbs [in Ssr.POPLmark]
TApp [in Ssr.SystemF_SN]
TApp [in Ssr.SystemF_CBV]
TApp [in Plain.POPLmark]
TApp [in Ssr.POPLmark]
TeVar [in Ssr.SystemF_SN]
TeVar [in Ssr.SystemF_CBV]
TeVar [in Plain.POPLmark]
TeVar [in Ssr.POPLmark]
Top [in Plain.POPLmark]
Top [in Ssr.POPLmark]
TyVar [in Ssr.SystemF_SN]
TyVar [in Ssr.SystemF_CBV]
TyVar [in Plain.POPLmark]
TyVar [in Ssr.POPLmark]
ty_tapp [in Ssr.SystemF_SN]
ty_tabs [in Ssr.SystemF_SN]
ty_app [in Ssr.SystemF_SN]
ty_abs [in Ssr.SystemF_SN]
ty_var [in Ssr.SystemF_SN]
ty_tapp [in Ssr.SystemF_CBV]
ty_tabs [in Ssr.SystemF_CBV]
ty_app [in Ssr.SystemF_CBV]
ty_abs [in Ssr.SystemF_CBV]
ty_var [in Ssr.SystemF_CBV]
Ty_App [in Plain.Demo]
Ty_Lam [in Plain.Demo]
Ty_Var [in Plain.Demo]
ty_sub [in Ssr.pred_CC_omega]
ty_prod [in Ssr.pred_CC_omega]
ty_lam [in Ssr.pred_CC_omega]
ty_app [in Ssr.pred_CC_omega]
ty_sort [in Ssr.pred_CC_omega]
ty_var [in Ssr.pred_CC_omega]
ty_sub [in Ssr.POPLmark]
ty_tapp [in Ssr.POPLmark]
ty_tabs [in Ssr.POPLmark]
ty_app [in Ssr.POPLmark]
ty_abs [in Ssr.POPLmark]
ty_var [in Ssr.POPLmark]
T_Sub [in Plain.POPLmark]
T_TApp [in Plain.POPLmark]
T_TAbs [in Plain.POPLmark]
T_App [in Plain.POPLmark]
T_Abs [in Plain.POPLmark]
T_Var [in Plain.POPLmark]
V
Value_TAbs [in Plain.POPLmark]Value_Abs [in Plain.POPLmark]
Var [in Ssr.CR]
Var [in Plain.Demo]
Var [in Ssr.pred_CC_omega]
Var [in Ssr.BetaSubstitution]
Inductive Index
A
accn [in Ssr.ARS]atnd [in Plain.Context]
C
context_ok [in Ssr.pred_CC_omega]conv [in Ssr.ARS]
D
Dec [in Plain.Decidable]E
eval [in Ssr.SystemF_CBV]eval [in Plain.POPLmark]
eval [in Ssr.POPLmark]
H
has_type [in Ssr.SystemF_SN]has_type [in Ssr.SystemF_CBV]
has_type [in Ssr.pred_CC_omega]
HSubst [in Autosubst.Autosubst_Classes]
HSubstHSubstComp [in Autosubst.Autosubst_Classes]
HSubstHSubstInd [in Autosubst.Autosubst_Classes]
I
Ids [in Autosubst.Autosubst_Classes]M
MMap [in Autosubst.Autosubst_MMap]MMapExt [in Autosubst.Autosubst_MMap]
P
pstep [in Ssr.CR]pstep [in Ssr.pred_CC_omega]
R
RedProdSpec [in Ssr.pred_CC_omega]Rename [in Autosubst.Autosubst_Classes]
S
Size [in Plain.Size]SizeFact [in Plain.Size]
sn [in Ssr.ARS]
star [in Ssr.ARS]
step [in Ssr.CR]
step [in Ssr.SystemF_SN]
step [in Plain.Demo]
step [in Ssr.pred_CC_omega]
sub [in Ssr.pred_CC_omega]
sub [in Plain.POPLmark]
sub [in Ssr.POPLmark]
Subst [in Autosubst.Autosubst_Classes]
SubstHSubstComp [in Autosubst.Autosubst_Classes]
sub1 [in Ssr.pred_CC_omega]
T
term [in Ssr.CR]term [in Ssr.SystemF_SN]
term [in Ssr.SystemF_CBV]
term [in Plain.Demo]
term [in Ssr.pred_CC_omega]
term [in Plain.POPLmark]
term [in Ssr.BetaSubstitution]
term [in Ssr.POPLmark]
ty [in Plain.Demo]
ty [in Plain.POPLmark]
ty [in Ssr.POPLmark]
type [in Ssr.SystemF_SN]
type [in Ssr.SystemF_CBV]
type [in Plain.Demo]
type [in Plain.POPLmark]
type [in Ssr.POPLmark]
V
value [in Plain.POPLmark]Projection Index
D
decide [in Plain.Decidable]H
hsubst [in Autosubst.Autosubst_Classes]hsubst_hsubst_ind [in Autosubst.Autosubst_Classes]
hsubst_hsubst_comp [in Autosubst.Autosubst_Classes]
hsubst_comp [in Autosubst.Autosubst_Classes]
hsubst_id [in Autosubst.Autosubst_Classes]
I
ids [in Autosubst.Autosubst_Classes]id_hsubst [in Autosubst.Autosubst_Classes]
id_subst [in Autosubst.Autosubst_Classes]
M
mmap [in Autosubst.Autosubst_MMap]mmap_comp [in Autosubst.Autosubst_MMap]
mmap_id [in Autosubst.Autosubst_MMap]
mmap_ext [in Autosubst.Autosubst_MMap]
P
p_nc [in Ssr.SystemF_SN]p_cl [in Ssr.SystemF_SN]
p_sn [in Ssr.SystemF_SN]
R
rename [in Autosubst.Autosubst_Classes]rename_subst [in Autosubst.Autosubst_Classes]
S
size [in Plain.Size]size_fact [in Plain.Size]
subst [in Autosubst.Autosubst_Classes]
subst_hsubst_comp [in Autosubst.Autosubst_Classes]
subst_comp [in Autosubst.Autosubst_Classes]
subst_id [in Autosubst.Autosubst_Classes]
Instance Index
D
decide_lt_nat [in Plain.Decidable]decide_le_nat [in Plain.Decidable]
decide_eq_nat [in Plain.Decidable]
H
HSubstLemmas_term [in Ssr.SystemF_SN]HSubstLemmas_term [in Ssr.SystemF_CBV]
HSubstLemmas_term [in Plain.POPLmark]
HSubstLemmas_term [in Ssr.POPLmark]
HSubst_term [in Ssr.SystemF_SN]
HSubst_term [in Ssr.SystemF_CBV]
hsubst_term [in Plain.POPLmark]
HSubst_term [in Ssr.POPLmark]
I
Ids_term [in Ssr.CR]Ids_term [in Ssr.SystemF_SN]
Ids_type [in Ssr.SystemF_SN]
Ids_term [in Ssr.SystemF_CBV]
Ids_type [in Ssr.SystemF_CBV]
Ids_term [in Plain.Demo]
Ids_term [in Ssr.pred_CC_omega]
Ids_term [in Plain.POPLmark]
Ids_type [in Plain.POPLmark]
Ids_term [in Ssr.BetaSubstitution]
Ids_term [in Ssr.POPLmark]
Ids_type [in Ssr.POPLmark]
M
MMapExt_fun [in Ssr.AutosubstSsr]mmapExt_seq [in Ssr.AutosubstSsr]
MMapExt_pair [in Ssr.AutosubstSsr]
MMapExt_option [in Ssr.AutosubstSsr]
MMapExt_fun [in Autosubst.Autosubst_MMapInstances]
MMapExt_pair [in Autosubst.Autosubst_MMapInstances]
MMapExt_list [in Autosubst.Autosubst_MMapInstances]
MMapExt_option [in Autosubst.Autosubst_MMapInstances]
MMapExt_const [in Autosubst.Autosubst_MMap]
MMapExt_refl [in Autosubst.Autosubst_MMap]
MMapLemmas_fun [in Ssr.AutosubstSsr]
mmapLemmas_seq [in Ssr.AutosubstSsr]
MMapLemmas_pair [in Ssr.AutosubstSsr]
MMapLemmas_option [in Ssr.AutosubstSsr]
MMapLemmas_fun [in Autosubst.Autosubst_MMapInstances]
MMapLemmas_pair [in Autosubst.Autosubst_MMapInstances]
MMapLemmas_list [in Autosubst.Autosubst_MMapInstances]
MMapLemmas_option [in Autosubst.Autosubst_MMapInstances]
MMapLemmas_const [in Autosubst.Autosubst_MMap]
MMapLemmas_refl [in Autosubst.Autosubst_MMap]
MMap_fun [in Ssr.AutosubstSsr]
mmap_seq [in Ssr.AutosubstSsr]
MMap_pair [in Ssr.AutosubstSsr]
MMap_option [in Ssr.AutosubstSsr]
MMap_fun [in Autosubst.Autosubst_MMapInstances]
MMap_pair [in Autosubst.Autosubst_MMapInstances]
MMap_list [in Autosubst.Autosubst_MMapInstances]
MMap_option [in Autosubst.Autosubst_MMapInstances]
MMap_const [in Autosubst.Autosubst_MMap]
MMap_refl [in Autosubst.Autosubst_MMap]
R
Rename_term [in Ssr.CR]Rename_term [in Ssr.SystemF_SN]
Rename_type [in Ssr.SystemF_SN]
Rename_term [in Ssr.SystemF_CBV]
Rename_type [in Ssr.SystemF_CBV]
Rename_term [in Plain.Demo]
Rename_term [in Ssr.pred_CC_omega]
Rename_term [in Plain.POPLmark]
Rename_type [in Plain.POPLmark]
Rename_term [in Ssr.BetaSubstitution]
Rename_term [in Ssr.POPLmark]
Rename_type [in Ssr.POPLmark]
S
size_term [in Plain.POPLmark]size_type [in Plain.POPLmark]
size_fact_In [in Plain.Size]
size_fact_app [in Plain.Size]
size_nat [in Plain.Size]
size_list [in Plain.Size]
SubstHSubstComp_type_term [in Ssr.SystemF_SN]
SubstHSubstComp_type_term [in Ssr.SystemF_CBV]
SubstHSubstComp_type_term [in Plain.POPLmark]
SubstHSubstComp_type_term [in Ssr.POPLmark]
SubstLemmas_term [in Ssr.CR]
SubstLemmas_term [in Ssr.SystemF_SN]
SubstLemmas_type [in Ssr.SystemF_SN]
SubstLemmas_term [in Ssr.SystemF_CBV]
SubstLemmas_type [in Ssr.SystemF_CBV]
SubstLemmas_term [in Plain.Demo]
substLemmas_term [in Ssr.pred_CC_omega]
SubstLemmas_term [in Plain.POPLmark]
SubstLemmas_type [in Plain.POPLmark]
SubstLemmas_term [in Ssr.BetaSubstitution]
SubstLemmas_term [in Ssr.POPLmark]
SubstLemmas_type [in Ssr.POPLmark]
Subst_term [in Ssr.CR]
Subst_term [in Ssr.SystemF_SN]
Subst_type [in Ssr.SystemF_SN]
Subst_term [in Ssr.SystemF_CBV]
Subst_type [in Ssr.SystemF_CBV]
Subst_term [in Plain.Demo]
Subst_term [in Ssr.pred_CC_omega]
Subst_term [in Plain.POPLmark]
Subst_type [in Plain.POPLmark]
Subst_term [in Ssr.BetaSubstitution]
Subst_term [in Ssr.POPLmark]
Subst_type [in Ssr.POPLmark]
Section Index
C
CoFinal [in Ssr.ARS]Commutation [in Ssr.ARS]
ComputationN [in Ssr.ARS]
D
Definitions [in Ssr.ARS]I
InternalLemmas [in Autosubst.Autosubst_Derive]InternalLemmasHSubst [in Autosubst.Autosubst_Derive]
L
LemmasForFun [in Autosubst.Autosubst_Basics]LemmasForHSubst [in Autosubst.Autosubst_Tactics]
LemmasForMMap [in Autosubst.Autosubst_MMap]
LemmasForSubst [in Autosubst.Autosubst_Tactics]
M
MMapConst [in Autosubst.Autosubst_MMap]MMapId [in Autosubst.Autosubst_MMap]
MMapInstances [in Ssr.AutosubstSsr]
MMapInstances [in Autosubst.Autosubst_MMapInstances]
S
SubstInstance [in Plain.Context]SubstLemmas [in Autosubst.Autosubst_Lemmas]
T
Termination [in Ssr.ARS]Abbreviation Index
E
E [in Ssr.SystemF_CBV]L
lift [in Ssr.BetaSubstitution]R
red [in Ssr.CR]red [in Ssr.pred_CC_omega]
S
sbst [in Ssr.BetaSubstitution]sn [in Ssr.SystemF_SN]
U
upn [in Autosubst.Autosubst_Classes]Definition Index
A
accn_ind' [in Ssr.ARS]admissible [in Ssr.SystemF_SN]
annot [in Autosubst.Autosubst_Basics]
atn [in Plain.Context]
C
cand [in Ssr.SystemF_SN]cofinal [in Ssr.ARS]
com [in Ssr.ARS]
confluent [in Ssr.ARS]
CR [in Ssr.ARS]
ctx [in Ssr.SystemF_SN]
ctx [in Ssr.SystemF_CBV]
D
dec [in Plain.Decidable]dget [in Ssr.Context]
diamond [in Ssr.ARS]
E
EL [in Ssr.SystemF_SN]evaln [in Ssr.ARS]
F
funcomp [in Autosubst.Autosubst_Basics]G
get [in Ssr.Context]H
hcomp [in Autosubst.Autosubst_Classes]I
id [in Autosubst.Autosubst_Basics]is_tabs [in Ssr.POPLmark]
is_abs [in Ssr.POPLmark]
is_var [in Ssr.POPLmark]
iterate [in Autosubst.Autosubst_Basics]
J
joinable [in Ssr.ARS]L
L [in Ssr.SystemF_SN]L [in Ssr.SystemF_CBV]
lift [in Autosubst.Autosubst_Basics]
lift_at [in Ssr.BetaSubstitution]
N
neutral [in Ssr.SystemF_SN]nf [in Ssr.ARS]
nilA [in Ssr.SystemF_CBV]
normal [in Ssr.ARS]
normalizing [in Ssr.ARS]
P
Pred [in Ssr.ARS]psstep [in Ssr.CR]
psstep [in Ssr.pred_CC_omega]
R
red [in Ssr.SystemF_SN]reducible [in Ssr.ARS]
Rel [in Ssr.ARS]
ren [in Autosubst.Autosubst_Classes]
rho [in Ssr.CR]
rho [in Ssr.pred_CC_omega]
S
sbst_at [in Ssr.BetaSubstitution]scomp [in Autosubst.Autosubst_Classes]
scons [in Autosubst.Autosubst_Basics]
sconv [in Ssr.pred_CC_omega]
sred [in Ssr.SystemF_SN]
sred [in Ssr.pred_CC_omega]
T
transitivity_at [in Ssr.POPLmark]triangle [in Ssr.ARS]
U
up [in Autosubst.Autosubst_Classes]upren [in Autosubst.Autosubst_Classes]
V
V [in Ssr.SystemF_CBV]value [in Ssr.POPLmark]
var [in Autosubst.Autosubst_Basics]
VG [in Ssr.SystemF_CBV]
W
wf_ty [in Plain.POPLmark]wn [in Ssr.ARS]
_
_bind [in Autosubst.Autosubst_Classes]Record Index
D
Dec [in Plain.Decidable]H
HSubst [in Autosubst.Autosubst_Classes]HSubstHSubstComp [in Autosubst.Autosubst_Classes]
HSubstHSubstInd [in Autosubst.Autosubst_Classes]
HSubstLemmas [in Autosubst.Autosubst_Classes]
I
Ids [in Autosubst.Autosubst_Classes]M
MMap [in Autosubst.Autosubst_MMap]MMapExt [in Autosubst.Autosubst_MMap]
MMapLemmas [in Autosubst.Autosubst_MMap]
R
reducible [in Ssr.SystemF_SN]Rename [in Autosubst.Autosubst_Classes]
S
Size [in Plain.Size]SizeFact [in Plain.Size]
Subst [in Autosubst.Autosubst_Classes]
SubstHSubstComp [in Autosubst.Autosubst_Classes]
SubstLemmas [in Autosubst.Autosubst_Classes]
| 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 | (864 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 | (41 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 | (34 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 | (22 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 | (325 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 | (167 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 | (52 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 | (24 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 | (99 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 | (17 entries) |
| Abbreviation 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 | (7 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 | (60 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 | (16 entries) |