| 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 | (307 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 | (19 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 | (20 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 | (76 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 | (101 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 | (34 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 | (6 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 | (23 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 | (28 entries) |
Global Index
A
adjoint [definition, in Subst.sur_les_relations]app [constructor, in Subst.TS]
app_bpar [constructor, in Subst.betapar]
a_set [definition, in Subst.sur_les_relations]
B
betapar [library]betapar_inv [abbreviation, in Subst.betapar]
beta_par [abbreviation, in Subst.betapar]
beta_bpar [constructor, in Subst.betapar]
beta1 [constructor, in Subst.lambda_sigma_lift]
C
commut [lemma, in Subst.commutation]commutation [lemma, in Subst.commutation]
commutation [library]
comp [constructor, in Subst.TS]
comparith [library]
comp_bpar [constructor, in Subst.betapar]
comp_rel [abbreviation, in Subst.sur_les_relations]
comp_2rel [constructor, in Subst.sur_les_relations]
confluence [abbreviation, in Subst.sur_les_relations]
confluence_LSL [lemma, in Subst.confluence_LSL]
confluence_en [definition, in Subst.sur_les_relations]
confluence_LSL [library]
conf_local_SL [lemma, in Subst.conf_local_SL]
conf_local_SL [library]
conf_strong_betapar [library]
cons [constructor, in Subst.TS]
cons_bpar [constructor, in Subst.betapar]
D
determinePC_SL [library]diag1 [abbreviation, in Subst.commutation]
E
egaliteTS [library]env [constructor, in Subst.TS]
env_bpar [constructor, in Subst.betapar]
explicit_noetherian [definition, in Subst.sur_les_relations]
explicit_inclus [definition, in Subst.sur_les_relations]
explicit_strong_confluence [definition, in Subst.sur_les_relations]
explicit_local_confluence [definition, in Subst.sur_les_relations]
explicit_confluence [definition, in Subst.sur_les_relations]
explicit_rel_plus [inductive, in Subst.sur_les_relations]
explicit_comp_rel [inductive, in Subst.sur_les_relations]
explicit_star [inductive, in Subst.sur_les_relations]
e_slstar_bp_slstar [definition, in Subst.SLstar_bpar_SLstar]
e_lexfg [definition, in Subst.terminaison_SL]
e_betapar_inv [definition, in Subst.betapar]
e_beta_par [inductive, in Subst.betapar]
e_local1 [definition, in Subst.conf_local_SL]
e_relLSLstar [definition, in Subst.lambda_sigma_lift]
e_relLSL [inductive, in Subst.lambda_sigma_lift]
e_systemLSL [inductive, in Subst.lambda_sigma_lift]
e_invSL [definition, in Subst.inversionSL]
e_P2 [definition, in Subst.Pol2]
e_diag1 [definition, in Subst.commutation]
e_relSLstar [definition, in Subst.sigma_lift]
e_relSL [inductive, in Subst.sigma_lift]
e_systemSL [inductive, in Subst.sigma_lift]
e_P1 [definition, in Subst.Pol1]
G
gt_P1_1 [lemma, in Subst.Pol1]H
hereditary [definition, in Subst.sur_les_relations]I
id [constructor, in Subst.TS]id_bpar [constructor, in Subst.betapar]
inclus [abbreviation, in Subst.sur_les_relations]
inversionSL [library]
invSL [abbreviation, in Subst.inversionSL]
L
lambda [constructor, in Subst.TS]lambda_bpar [constructor, in Subst.betapar]
lambda_sigma_lift [library]
lexfg [abbreviation, in Subst.terminaison_SL]
lexfg_relSL [lemma, in Subst.terminaison_SL]
lexfg_lift [lemma, in Subst.terminaison_SL]
lexfg_comp_r [lemma, in Subst.terminaison_SL]
lexfg_comp_l [lemma, in Subst.terminaison_SL]
lexfg_cons_s [lemma, in Subst.terminaison_SL]
lexfg_cons_t [lemma, in Subst.terminaison_SL]
lexfg_env_s [lemma, in Subst.terminaison_SL]
lexfg_env_t [lemma, in Subst.terminaison_SL]
lexfg_lambda [lemma, in Subst.terminaison_SL]
lexfg_app_r [lemma, in Subst.terminaison_SL]
lexfg_app_l [lemma, in Subst.terminaison_SL]
lexfg_systemSL [lemma, in Subst.terminaison_SL]
lexfg_notherian [lemma, in Subst.terminaison_SL]
lift [constructor, in Subst.TS]
lift_bpar [constructor, in Subst.betapar]
local_confluence [abbreviation, in Subst.sur_les_relations]
local_confluence_en [definition, in Subst.sur_les_relations]
local1 [abbreviation, in Subst.conf_local_SL]
LSL_context_lift [constructor, in Subst.lambda_sigma_lift]
LSL_context_comp_r [constructor, in Subst.lambda_sigma_lift]
LSL_context_comp_l [constructor, in Subst.lambda_sigma_lift]
LSL_context_cons_s [constructor, in Subst.lambda_sigma_lift]
LSL_context_cons_t [constructor, in Subst.lambda_sigma_lift]
LSL_context_env_s [constructor, in Subst.lambda_sigma_lift]
LSL_context_env_t [constructor, in Subst.lambda_sigma_lift]
LSL_context_lambda [constructor, in Subst.lambda_sigma_lift]
LSL_context_app_r [constructor, in Subst.lambda_sigma_lift]
LSL_context_app_l [constructor, in Subst.lambda_sigma_lift]
LSL_one_regle [constructor, in Subst.lambda_sigma_lift]
M
metax_bpar [constructor, in Subst.betapar]metaX_bpar [constructor, in Subst.betapar]
meta_x [constructor, in Subst.TS]
meta_X [constructor, in Subst.TS]
N
Newman [lemma, in Subst.Newman]Newman [library]
NewmanS [section, in Subst.Newman]
NewmanS.A [variable, in Subst.Newman]
NewmanS.C [variable, in Subst.Newman]
NewmanS.N [variable, in Subst.Newman]
NewmanS.R [variable, in Subst.Newman]
noetherian [abbreviation, in Subst.sur_les_relations]
noetherian_induction [lemma, in Subst.sur_les_relations]
noetherian_induction1 [lemma, in Subst.sur_les_relations]
noether_inclus [lemma, in Subst.sur_les_relations]
O
ordre [section, in Subst.terminaison_SL]ordre.A [variable, in Subst.terminaison_SL]
ordre.f [variable, in Subst.terminaison_SL]
ordre.g [variable, in Subst.terminaison_SL]
P
plus_preserves_noetherian [lemma, in Subst.sur_les_relations]Pol1 [library]
Pol2 [library]
power2 [definition, in Subst.comparith]
P1 [abbreviation, in Subst.Pol1]
P1_id [lemma, in Subst.Pol1]
P1_liftid [lemma, in Subst.Pol1]
P1_idr [lemma, in Subst.Pol1]
P1_idl [lemma, in Subst.Pol1]
P1_liftenv [lemma, in Subst.Pol1]
P1_lift2 [lemma, in Subst.Pol1]
P1_lift1 [lemma, in Subst.Pol1]
P1_shiftlift2 [lemma, in Subst.Pol1]
P1_shiftlift1 [lemma, in Subst.Pol1]
P1_shiftcons [lemma, in Subst.Pol1]
P1_mapenv [lemma, in Subst.Pol1]
P1_assenv [lemma, in Subst.Pol1]
P1_rvarlift2 [lemma, in Subst.Pol1]
P1_rvarlift1 [lemma, in Subst.Pol1]
P1_rvarcons [lemma, in Subst.Pol1]
P1_fvarlift2 [lemma, in Subst.Pol1]
P1_fvarlift1 [lemma, in Subst.Pol1]
P1_fvarcons [lemma, in Subst.Pol1]
P1_varshift2 [lemma, in Subst.Pol1]
P1_varshift1 [lemma, in Subst.Pol1]
P1_clos [lemma, in Subst.Pol1]
P1_lambda [lemma, in Subst.Pol1]
P1_app [lemma, in Subst.Pol1]
P2 [abbreviation, in Subst.Pol2]
P2_id [lemma, in Subst.Pol2]
P2_liftid [lemma, in Subst.Pol2]
P2_idr [lemma, in Subst.Pol2]
P2_idl [lemma, in Subst.Pol2]
P2_liftenv [lemma, in Subst.Pol2]
P2_lift2 [lemma, in Subst.Pol2]
P2_lift1 [lemma, in Subst.Pol2]
P2_shiftlift2 [lemma, in Subst.Pol2]
P2_shiftlift1 [lemma, in Subst.Pol2]
P2_shiftcons [lemma, in Subst.Pol2]
P2_mapenv [lemma, in Subst.Pol2]
P2_assenv [lemma, in Subst.Pol2]
P2_rvarlift2 [lemma, in Subst.Pol2]
P2_rvarlift1 [lemma, in Subst.Pol2]
P2_rvarcons [lemma, in Subst.Pol2]
P2_fvarlift2 [lemma, in Subst.Pol2]
P2_fvarlift1 [lemma, in Subst.Pol2]
P2_fvarcons [lemma, in Subst.Pol2]
P2_varshift2 [lemma, in Subst.Pol2]
P2_varshift1 [lemma, in Subst.Pol2]
P2_clos [lemma, in Subst.Pol2]
P2_lambda [lemma, in Subst.Pol2]
P2_app [lemma, in Subst.Pol2]
P2_pos [lemma, in Subst.Pol2]
R
regle_id [constructor, in Subst.sigma_lift]regle_liftid [constructor, in Subst.sigma_lift]
regle_idr [constructor, in Subst.sigma_lift]
regle_idl [constructor, in Subst.sigma_lift]
regle_liftenv [constructor, in Subst.sigma_lift]
regle_lift2 [constructor, in Subst.sigma_lift]
regle_lift1 [constructor, in Subst.sigma_lift]
regle_shiftlift2 [constructor, in Subst.sigma_lift]
regle_shiftlift1 [constructor, in Subst.sigma_lift]
regle_shiftcons [constructor, in Subst.sigma_lift]
regle_mapenv [constructor, in Subst.sigma_lift]
regle_assenv [constructor, in Subst.sigma_lift]
regle_rvarlift2 [constructor, in Subst.sigma_lift]
regle_rvarlift1 [constructor, in Subst.sigma_lift]
regle_rvarcons [constructor, in Subst.sigma_lift]
regle_fvarlift2 [constructor, in Subst.sigma_lift]
regle_fvarlift1 [constructor, in Subst.sigma_lift]
regle_fvarcons [constructor, in Subst.sigma_lift]
regle_varshift2 [constructor, in Subst.sigma_lift]
regle_varshift1 [constructor, in Subst.sigma_lift]
regle_clos [constructor, in Subst.sigma_lift]
regle_lambda [constructor, in Subst.sigma_lift]
regle_app [constructor, in Subst.sigma_lift]
reg_beta [inductive, in Subst.lambda_sigma_lift]
reg_id [inductive, in Subst.sigma_lift]
reg_liftid [inductive, in Subst.sigma_lift]
reg_idr [inductive, in Subst.sigma_lift]
reg_idl [inductive, in Subst.sigma_lift]
reg_liftenv [inductive, in Subst.sigma_lift]
reg_lift2 [inductive, in Subst.sigma_lift]
reg_lift1 [inductive, in Subst.sigma_lift]
reg_shiftlift2 [inductive, in Subst.sigma_lift]
reg_shiftlift1 [inductive, in Subst.sigma_lift]
reg_shiftcons [inductive, in Subst.sigma_lift]
reg_mapenv [inductive, in Subst.sigma_lift]
reg_assenv [inductive, in Subst.sigma_lift]
reg_rvarlift2 [inductive, in Subst.sigma_lift]
reg_rvarlift1 [inductive, in Subst.sigma_lift]
reg_rvarcons [inductive, in Subst.sigma_lift]
reg_fvarlift2 [inductive, in Subst.sigma_lift]
reg_fvarlift1 [inductive, in Subst.sigma_lift]
reg_fvarcons [inductive, in Subst.sigma_lift]
reg_varshift2 [inductive, in Subst.sigma_lift]
reg_varshift1 [inductive, in Subst.sigma_lift]
reg_clos [inductive, in Subst.sigma_lift]
reg_lambda [inductive, in Subst.sigma_lift]
reg_app [inductive, in Subst.sigma_lift]
reg1_beta [constructor, in Subst.lambda_sigma_lift]
reg1_id [constructor, in Subst.sigma_lift]
reg1_liftid [constructor, in Subst.sigma_lift]
reg1_idr [constructor, in Subst.sigma_lift]
reg1_idl [constructor, in Subst.sigma_lift]
reg1_liftenv [constructor, in Subst.sigma_lift]
reg1_lift2 [constructor, in Subst.sigma_lift]
reg1_lift1 [constructor, in Subst.sigma_lift]
reg1_shiftlift2 [constructor, in Subst.sigma_lift]
reg1_shiftlift1 [constructor, in Subst.sigma_lift]
reg1_shiftcons [constructor, in Subst.sigma_lift]
reg1_mapenv [constructor, in Subst.sigma_lift]
reg1_assenv [constructor, in Subst.sigma_lift]
reg1_rvarlift2 [constructor, in Subst.sigma_lift]
reg1_rvarlift1 [constructor, in Subst.sigma_lift]
reg1_rvarcons [constructor, in Subst.sigma_lift]
reg1_fvarlift2 [constructor, in Subst.sigma_lift]
reg1_fvarlift1 [constructor, in Subst.sigma_lift]
reg1_fvarcons [constructor, in Subst.sigma_lift]
reg1_varshift2 [constructor, in Subst.sigma_lift]
reg1_varshift1 [constructor, in Subst.sigma_lift]
reg1_clos [constructor, in Subst.sigma_lift]
reg1_lambda [constructor, in Subst.sigma_lift]
reg1_app [constructor, in Subst.sigma_lift]
relations_noetherian.R [variable, in Subst.sur_les_relations]
relations_noetherian.U [variable, in Subst.sur_les_relations]
relations_noetherian [section, in Subst.sur_les_relations]
relLSL [abbreviation, in Subst.lambda_sigma_lift]
relLSLstar [abbreviation, in Subst.lambda_sigma_lift]
relplus_trans1 [constructor, in Subst.sur_les_relations]
relplus_1step [constructor, in Subst.sur_les_relations]
Rels [section, in Subst.sur_les_relations]
relSL [abbreviation, in Subst.sigma_lift]
relSLstar [abbreviation, in Subst.sigma_lift]
relSL_noetherian [lemma, in Subst.terminaison_SL]
rels_prop.R [variable, in Subst.sur_les_relations]
rels_prop.A [variable, in Subst.sur_les_relations]
rels_prop [section, in Subst.sur_les_relations]
Rels.A [variable, in Subst.sur_les_relations]
rel_plus [abbreviation, in Subst.sur_les_relations]
resoudPC_SL [library]
Rstar_S_Rstar [definition, in Subst.Yokouchi]
S
sconf [definition, in Subst.conf_strong_betapar]sconf_betapar [lemma, in Subst.conf_strong_betapar]
shift [constructor, in Subst.TS]
shift_bpar [constructor, in Subst.betapar]
sigma_lift [library]
slstar_bp_slstar [abbreviation, in Subst.SLstar_bpar_SLstar]
SLstar_bpar_SLstar [library]
SL_context_lift [constructor, in Subst.sigma_lift]
SL_context_comp_r [constructor, in Subst.sigma_lift]
SL_context_comp_l [constructor, in Subst.sigma_lift]
SL_context_cons_s [constructor, in Subst.sigma_lift]
SL_context_cons_t [constructor, in Subst.sigma_lift]
SL_context_env_s [constructor, in Subst.sigma_lift]
SL_context_env_t [constructor, in Subst.sigma_lift]
SL_context_lambda [constructor, in Subst.sigma_lift]
SL_context_app_r [constructor, in Subst.sigma_lift]
SL_context_app_l [constructor, in Subst.sigma_lift]
SL_one_regle [constructor, in Subst.sigma_lift]
SL1 [constructor, in Subst.lambda_sigma_lift]
star [abbreviation, in Subst.sur_les_relations]
star_trans [lemma, in Subst.sur_les_relations]
star_trans1 [constructor, in Subst.sur_les_relations]
star_refl [constructor, in Subst.sur_les_relations]
strong_confluence [abbreviation, in Subst.sur_les_relations]
strong_confluence_en [definition, in Subst.sur_les_relations]
sub [definition, in Subst.sur_les_relations]
sub_explicits_ind [lemma, in Subst.TS]
sub_explicits [definition, in Subst.TS]
sur_les_relations [library]
systemLSL [abbreviation, in Subst.lambda_sigma_lift]
systemSL [abbreviation, in Subst.sigma_lift]
T
terminaison_SL [library]terms [definition, in Subst.TS]
terms_ind [lemma, in Subst.TS]
TS [inductive, in Subst.TS]
TS [library]
U
universal [definition, in Subst.sur_les_relations]V
var [constructor, in Subst.TS]var_bpar [constructor, in Subst.betapar]
W
ws [constructor, in Subst.TS]wsort [inductive, in Subst.TS]
wt [constructor, in Subst.TS]
Y
Yokouchi [lemma, in Subst.Yokouchi]Yokouchi [library]
YokouchiS [section, in Subst.Yokouchi]
YokouchiS.A [variable, in Subst.Yokouchi]
YokouchiS.C [variable, in Subst.Yokouchi]
YokouchiS.commut1 [variable, in Subst.Yokouchi]
YokouchiS.N [variable, in Subst.Yokouchi]
YokouchiS.R [variable, in Subst.Yokouchi]
YokouchiS.S [variable, in Subst.Yokouchi]
YokouchiS.SC [variable, in Subst.Yokouchi]
Variable Index
N
NewmanS.A [in Subst.Newman]NewmanS.C [in Subst.Newman]
NewmanS.N [in Subst.Newman]
NewmanS.R [in Subst.Newman]
O
ordre.A [in Subst.terminaison_SL]ordre.f [in Subst.terminaison_SL]
ordre.g [in Subst.terminaison_SL]
R
relations_noetherian.R [in Subst.sur_les_relations]relations_noetherian.U [in Subst.sur_les_relations]
rels_prop.R [in Subst.sur_les_relations]
rels_prop.A [in Subst.sur_les_relations]
Rels.A [in Subst.sur_les_relations]
Y
YokouchiS.A [in Subst.Yokouchi]YokouchiS.C [in Subst.Yokouchi]
YokouchiS.commut1 [in Subst.Yokouchi]
YokouchiS.N [in Subst.Yokouchi]
YokouchiS.R [in Subst.Yokouchi]
YokouchiS.S [in Subst.Yokouchi]
YokouchiS.SC [in Subst.Yokouchi]
Library Index
B
betaparC
commutationcomparith
confluence_LSL
conf_local_SL
conf_strong_betapar
D
determinePC_SLE
egaliteTSI
inversionSLL
lambda_sigma_liftN
NewmanP
Pol1Pol2
R
resoudPC_SLS
sigma_liftSLstar_bpar_SLstar
sur_les_relations
T
terminaison_SLTS
Y
YokouchiLemma Index
C
commut [in Subst.commutation]commutation [in Subst.commutation]
confluence_LSL [in Subst.confluence_LSL]
conf_local_SL [in Subst.conf_local_SL]
G
gt_P1_1 [in Subst.Pol1]L
lexfg_relSL [in Subst.terminaison_SL]lexfg_lift [in Subst.terminaison_SL]
lexfg_comp_r [in Subst.terminaison_SL]
lexfg_comp_l [in Subst.terminaison_SL]
lexfg_cons_s [in Subst.terminaison_SL]
lexfg_cons_t [in Subst.terminaison_SL]
lexfg_env_s [in Subst.terminaison_SL]
lexfg_env_t [in Subst.terminaison_SL]
lexfg_lambda [in Subst.terminaison_SL]
lexfg_app_r [in Subst.terminaison_SL]
lexfg_app_l [in Subst.terminaison_SL]
lexfg_systemSL [in Subst.terminaison_SL]
lexfg_notherian [in Subst.terminaison_SL]
N
Newman [in Subst.Newman]noetherian_induction [in Subst.sur_les_relations]
noetherian_induction1 [in Subst.sur_les_relations]
noether_inclus [in Subst.sur_les_relations]
P
plus_preserves_noetherian [in Subst.sur_les_relations]P1_id [in Subst.Pol1]
P1_liftid [in Subst.Pol1]
P1_idr [in Subst.Pol1]
P1_idl [in Subst.Pol1]
P1_liftenv [in Subst.Pol1]
P1_lift2 [in Subst.Pol1]
P1_lift1 [in Subst.Pol1]
P1_shiftlift2 [in Subst.Pol1]
P1_shiftlift1 [in Subst.Pol1]
P1_shiftcons [in Subst.Pol1]
P1_mapenv [in Subst.Pol1]
P1_assenv [in Subst.Pol1]
P1_rvarlift2 [in Subst.Pol1]
P1_rvarlift1 [in Subst.Pol1]
P1_rvarcons [in Subst.Pol1]
P1_fvarlift2 [in Subst.Pol1]
P1_fvarlift1 [in Subst.Pol1]
P1_fvarcons [in Subst.Pol1]
P1_varshift2 [in Subst.Pol1]
P1_varshift1 [in Subst.Pol1]
P1_clos [in Subst.Pol1]
P1_lambda [in Subst.Pol1]
P1_app [in Subst.Pol1]
P2_id [in Subst.Pol2]
P2_liftid [in Subst.Pol2]
P2_idr [in Subst.Pol2]
P2_idl [in Subst.Pol2]
P2_liftenv [in Subst.Pol2]
P2_lift2 [in Subst.Pol2]
P2_lift1 [in Subst.Pol2]
P2_shiftlift2 [in Subst.Pol2]
P2_shiftlift1 [in Subst.Pol2]
P2_shiftcons [in Subst.Pol2]
P2_mapenv [in Subst.Pol2]
P2_assenv [in Subst.Pol2]
P2_rvarlift2 [in Subst.Pol2]
P2_rvarlift1 [in Subst.Pol2]
P2_rvarcons [in Subst.Pol2]
P2_fvarlift2 [in Subst.Pol2]
P2_fvarlift1 [in Subst.Pol2]
P2_fvarcons [in Subst.Pol2]
P2_varshift2 [in Subst.Pol2]
P2_varshift1 [in Subst.Pol2]
P2_clos [in Subst.Pol2]
P2_lambda [in Subst.Pol2]
P2_app [in Subst.Pol2]
P2_pos [in Subst.Pol2]
R
relSL_noetherian [in Subst.terminaison_SL]S
sconf_betapar [in Subst.conf_strong_betapar]star_trans [in Subst.sur_les_relations]
sub_explicits_ind [in Subst.TS]
T
terms_ind [in Subst.TS]Y
Yokouchi [in Subst.Yokouchi]Constructor Index
A
app [in Subst.TS]app_bpar [in Subst.betapar]
B
beta_bpar [in Subst.betapar]beta1 [in Subst.lambda_sigma_lift]
C
comp [in Subst.TS]comp_bpar [in Subst.betapar]
comp_2rel [in Subst.sur_les_relations]
cons [in Subst.TS]
cons_bpar [in Subst.betapar]
E
env [in Subst.TS]env_bpar [in Subst.betapar]
I
id [in Subst.TS]id_bpar [in Subst.betapar]
L
lambda [in Subst.TS]lambda_bpar [in Subst.betapar]
lift [in Subst.TS]
lift_bpar [in Subst.betapar]
LSL_context_lift [in Subst.lambda_sigma_lift]
LSL_context_comp_r [in Subst.lambda_sigma_lift]
LSL_context_comp_l [in Subst.lambda_sigma_lift]
LSL_context_cons_s [in Subst.lambda_sigma_lift]
LSL_context_cons_t [in Subst.lambda_sigma_lift]
LSL_context_env_s [in Subst.lambda_sigma_lift]
LSL_context_env_t [in Subst.lambda_sigma_lift]
LSL_context_lambda [in Subst.lambda_sigma_lift]
LSL_context_app_r [in Subst.lambda_sigma_lift]
LSL_context_app_l [in Subst.lambda_sigma_lift]
LSL_one_regle [in Subst.lambda_sigma_lift]
M
metax_bpar [in Subst.betapar]metaX_bpar [in Subst.betapar]
meta_x [in Subst.TS]
meta_X [in Subst.TS]
R
regle_id [in Subst.sigma_lift]regle_liftid [in Subst.sigma_lift]
regle_idr [in Subst.sigma_lift]
regle_idl [in Subst.sigma_lift]
regle_liftenv [in Subst.sigma_lift]
regle_lift2 [in Subst.sigma_lift]
regle_lift1 [in Subst.sigma_lift]
regle_shiftlift2 [in Subst.sigma_lift]
regle_shiftlift1 [in Subst.sigma_lift]
regle_shiftcons [in Subst.sigma_lift]
regle_mapenv [in Subst.sigma_lift]
regle_assenv [in Subst.sigma_lift]
regle_rvarlift2 [in Subst.sigma_lift]
regle_rvarlift1 [in Subst.sigma_lift]
regle_rvarcons [in Subst.sigma_lift]
regle_fvarlift2 [in Subst.sigma_lift]
regle_fvarlift1 [in Subst.sigma_lift]
regle_fvarcons [in Subst.sigma_lift]
regle_varshift2 [in Subst.sigma_lift]
regle_varshift1 [in Subst.sigma_lift]
regle_clos [in Subst.sigma_lift]
regle_lambda [in Subst.sigma_lift]
regle_app [in Subst.sigma_lift]
reg1_beta [in Subst.lambda_sigma_lift]
reg1_id [in Subst.sigma_lift]
reg1_liftid [in Subst.sigma_lift]
reg1_idr [in Subst.sigma_lift]
reg1_idl [in Subst.sigma_lift]
reg1_liftenv [in Subst.sigma_lift]
reg1_lift2 [in Subst.sigma_lift]
reg1_lift1 [in Subst.sigma_lift]
reg1_shiftlift2 [in Subst.sigma_lift]
reg1_shiftlift1 [in Subst.sigma_lift]
reg1_shiftcons [in Subst.sigma_lift]
reg1_mapenv [in Subst.sigma_lift]
reg1_assenv [in Subst.sigma_lift]
reg1_rvarlift2 [in Subst.sigma_lift]
reg1_rvarlift1 [in Subst.sigma_lift]
reg1_rvarcons [in Subst.sigma_lift]
reg1_fvarlift2 [in Subst.sigma_lift]
reg1_fvarlift1 [in Subst.sigma_lift]
reg1_fvarcons [in Subst.sigma_lift]
reg1_varshift2 [in Subst.sigma_lift]
reg1_varshift1 [in Subst.sigma_lift]
reg1_clos [in Subst.sigma_lift]
reg1_lambda [in Subst.sigma_lift]
reg1_app [in Subst.sigma_lift]
relplus_trans1 [in Subst.sur_les_relations]
relplus_1step [in Subst.sur_les_relations]
S
shift [in Subst.TS]shift_bpar [in Subst.betapar]
SL_context_lift [in Subst.sigma_lift]
SL_context_comp_r [in Subst.sigma_lift]
SL_context_comp_l [in Subst.sigma_lift]
SL_context_cons_s [in Subst.sigma_lift]
SL_context_cons_t [in Subst.sigma_lift]
SL_context_env_s [in Subst.sigma_lift]
SL_context_env_t [in Subst.sigma_lift]
SL_context_lambda [in Subst.sigma_lift]
SL_context_app_r [in Subst.sigma_lift]
SL_context_app_l [in Subst.sigma_lift]
SL_one_regle [in Subst.sigma_lift]
SL1 [in Subst.lambda_sigma_lift]
star_trans1 [in Subst.sur_les_relations]
star_refl [in Subst.sur_les_relations]
V
var [in Subst.TS]var_bpar [in Subst.betapar]
W
ws [in Subst.TS]wt [in Subst.TS]
Inductive Index
E
explicit_rel_plus [in Subst.sur_les_relations]explicit_comp_rel [in Subst.sur_les_relations]
explicit_star [in Subst.sur_les_relations]
e_beta_par [in Subst.betapar]
e_relLSL [in Subst.lambda_sigma_lift]
e_systemLSL [in Subst.lambda_sigma_lift]
e_relSL [in Subst.sigma_lift]
e_systemSL [in Subst.sigma_lift]
R
reg_beta [in Subst.lambda_sigma_lift]reg_id [in Subst.sigma_lift]
reg_liftid [in Subst.sigma_lift]
reg_idr [in Subst.sigma_lift]
reg_idl [in Subst.sigma_lift]
reg_liftenv [in Subst.sigma_lift]
reg_lift2 [in Subst.sigma_lift]
reg_lift1 [in Subst.sigma_lift]
reg_shiftlift2 [in Subst.sigma_lift]
reg_shiftlift1 [in Subst.sigma_lift]
reg_shiftcons [in Subst.sigma_lift]
reg_mapenv [in Subst.sigma_lift]
reg_assenv [in Subst.sigma_lift]
reg_rvarlift2 [in Subst.sigma_lift]
reg_rvarlift1 [in Subst.sigma_lift]
reg_rvarcons [in Subst.sigma_lift]
reg_fvarlift2 [in Subst.sigma_lift]
reg_fvarlift1 [in Subst.sigma_lift]
reg_fvarcons [in Subst.sigma_lift]
reg_varshift2 [in Subst.sigma_lift]
reg_varshift1 [in Subst.sigma_lift]
reg_clos [in Subst.sigma_lift]
reg_lambda [in Subst.sigma_lift]
reg_app [in Subst.sigma_lift]
T
TS [in Subst.TS]W
wsort [in Subst.TS]Section Index
N
NewmanS [in Subst.Newman]O
ordre [in Subst.terminaison_SL]R
relations_noetherian [in Subst.sur_les_relations]Rels [in Subst.sur_les_relations]
rels_prop [in Subst.sur_les_relations]
Y
YokouchiS [in Subst.Yokouchi]Abbreviation Index
B
betapar_inv [in Subst.betapar]beta_par [in Subst.betapar]
C
comp_rel [in Subst.sur_les_relations]confluence [in Subst.sur_les_relations]
D
diag1 [in Subst.commutation]I
inclus [in Subst.sur_les_relations]invSL [in Subst.inversionSL]
L
lexfg [in Subst.terminaison_SL]local_confluence [in Subst.sur_les_relations]
local1 [in Subst.conf_local_SL]
N
noetherian [in Subst.sur_les_relations]P
P1 [in Subst.Pol1]P2 [in Subst.Pol2]
R
relLSL [in Subst.lambda_sigma_lift]relLSLstar [in Subst.lambda_sigma_lift]
relSL [in Subst.sigma_lift]
relSLstar [in Subst.sigma_lift]
rel_plus [in Subst.sur_les_relations]
S
slstar_bp_slstar [in Subst.SLstar_bpar_SLstar]star [in Subst.sur_les_relations]
strong_confluence [in Subst.sur_les_relations]
systemLSL [in Subst.lambda_sigma_lift]
systemSL [in Subst.sigma_lift]
Definition Index
A
adjoint [in Subst.sur_les_relations]a_set [in Subst.sur_les_relations]
C
confluence_en [in Subst.sur_les_relations]E
explicit_noetherian [in Subst.sur_les_relations]explicit_inclus [in Subst.sur_les_relations]
explicit_strong_confluence [in Subst.sur_les_relations]
explicit_local_confluence [in Subst.sur_les_relations]
explicit_confluence [in Subst.sur_les_relations]
e_slstar_bp_slstar [in Subst.SLstar_bpar_SLstar]
e_lexfg [in Subst.terminaison_SL]
e_betapar_inv [in Subst.betapar]
e_local1 [in Subst.conf_local_SL]
e_relLSLstar [in Subst.lambda_sigma_lift]
e_invSL [in Subst.inversionSL]
e_P2 [in Subst.Pol2]
e_diag1 [in Subst.commutation]
e_relSLstar [in Subst.sigma_lift]
e_P1 [in Subst.Pol1]
H
hereditary [in Subst.sur_les_relations]L
local_confluence_en [in Subst.sur_les_relations]P
power2 [in Subst.comparith]R
Rstar_S_Rstar [in Subst.Yokouchi]S
sconf [in Subst.conf_strong_betapar]strong_confluence_en [in Subst.sur_les_relations]
sub [in Subst.sur_les_relations]
sub_explicits [in Subst.TS]
T
terms [in Subst.TS]U
universal [in Subst.sur_les_relations]| 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 | (307 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 | (19 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 | (20 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 | (76 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 | (101 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 | (34 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 | (6 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 | (23 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 | (28 entries) |