| 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 | (645 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 | (10 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 | (3 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 | (258 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 | (16 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 | (39 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 | (38 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 | (40 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 | (16 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 | (171 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 | (38 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 | (16 entries) |
Global Index
A
A [constructor, in ExampleABA]aa [lemma, in NoUniqueNormalFormsWOElaborated]
ABA [definition, in ExampleABA]
ABA_left_linear [lemma, in ExampleABA]
ABA_trs [definition, in ExampleABA]
ABA_r [definition, in ExampleABA]
ABA_l [definition, in ExampleABA]
ABA_in [lemma, in ExampleABA]
ABA_wf [lemma, in ExampleABA]
add [definition, in Ordinal]
add_wf [lemma, in WfOrdinal]
all_pos_eq [definition, in TermEquality]
all_terms_eq_up_to_0 [lemma, in Rewriting]
all_terms_eq_up_to_d_s_Udpsid_USdpsiSd_repeat_U [lemma, in NoUniqueNormalFormsWOElaborated]
all_terms_eq_up_to_d_s_UdDnUnt_Udt_repeat_U [lemma, in NoUniqueNormalFormsWOElaborated]
all_terms_eq_up_to [definition, in Rewriting]
all_terms_eq_up_to_snoc [lemma, in Rewriting]
append [definition, in Rewriting]
append_is_cons [lemma, in NoUniqueNormalFormsWO]
append_embed [lemma, in Rewriting]
append_wf [lemma, in Rewriting]
append_length [lemma, in Rewriting]
append_embed_strict [lemma, in Rewriting]
append_finite [lemma, in Rewriting]
append_rec [definition, in Rewriting]
arity [definition, in ExampleABA]
arity [projection, in Signature]
arity [definition, in NoUniqueNormalFormsWO]
B
B [constructor, in ExampleABA]bb [lemma, in NoUniqueNormalFormsWOElaborated]
beq_symb_ok [projection, in Signature]
beq_var [definition, in ExampleABA]
beq_var_ok [lemma, in ExampleABA]
beq_var [definition, in NoUniqueNormalFormsWO]
beq_symb [definition, in ExampleABA]
beq_var_ok [projection, in Variables]
beq_symb_ok [lemma, in ExampleABA]
beq_symb [definition, in NoUniqueNormalFormsWO]
beq_symb_ok [lemma, in NoUniqueNormalFormsWO]
beq_var_ok [lemma, in NoUniqueNormalFormsWO]
beq_var [projection, in Variables]
beq_symb [projection, in Signature]
C
Cast [section, in Vector]Cast.A [variable, in Vector]
ccD [lemma, in NoUniqueNormalFormsWOElaborated]
ccU [lemma, in NoUniqueNormalFormsWOElaborated]
ceut_fun_inv_v [lemma, in ContextEquality]
ceut_fun_inv [lemma, in ContextEquality]
ceut_hole [constructor, in ContextEquality]
ceut_fun_inv_w [lemma, in ContextEquality]
ceut_cfun [constructor, in ContextEquality]
ceut_0 [constructor, in ContextEquality]
CFun [constructor, in Context]
CFun_bis [constructor, in ContextEquality]
Cons [constructor, in Rewriting]
cons_term_bis [definition, in Rewriting]
context [abbreviation, in NoUniqueNormalFormsWO]
context [inductive, in Context]
Context [section, in Context]
context [abbreviation, in ContextEquality]
context [abbreviation, in ExampleABA]
context [abbreviation, in Rewriting]
Context [library]
ContextEquality [section, in ContextEquality]
ContextEquality [library]
ContextEquality.F [variable, in ContextEquality]
ContextEquality.X [variable, in ContextEquality]
context_eq [definition, in ContextEquality]
context_ind2 [definition, in NoUniqueNormalFormsWOElaborated]
context_bis_symm [lemma, in ContextEquality]
context_rect2 [definition, in NoUniqueNormalFormsWOElaborated]
context_eq_fun_inv_i [lemma, in ContextEquality]
context_bis_trans [lemma, in ContextEquality]
context_bis_refl [lemma, in ContextEquality]
context_bis_implies_context_eq [lemma, in ContextEquality]
context_eq_implies_context_bis [lemma, in ContextEquality]
context_bis_context_eq [lemma, in ContextEquality]
context_eq_fun_inv_v [lemma, in ContextEquality]
context_eq_fun_inv_j [lemma, in ContextEquality]
context_eq_fun_inv_symbol [lemma, in ContextEquality]
context_eq_fun_inv [lemma, in ContextEquality]
context_eq_up_to [inductive, in ContextEquality]
context_eq_fun_inv_w [lemma, in ContextEquality]
context_bis [inductive, in ContextEquality]
Context.F [variable, in Context]
Context.X [variable, in Context]
converges [definition, in TermEquality]
converges_nB_A [lemma, in ExampleABA]
converges_Unpsin [lemma, in NoUniqueNormalFormsWO]
converges_DSnU2SnpsiSn [lemma, in NoUniqueNormalFormsWO]
critical_pairs_trivial_UD [lemma, in NoUniqueNormalFormsWO]
critical_pair [definition, in Rewriting]
critical_pair_Ux_Ux [lemma, in NoUniqueNormalFormsWOElaborated]
D
D [constructor, in NoUniqueNormalFormsWO]DDnt_eq_DnDt [lemma, in NoUniqueNormalFormsWO]
DD2nt_eq_D2nDt [lemma, in NoUniqueNormalFormsWO]
depth [definition, in Rewriting]
dig [definition, in Context]
disc_O_S [definition, in Prelims]
disc_S_O [definition, in Prelims]
Dnc [definition, in NoUniqueNormalFormsWO]
Dnt [definition, in NoUniqueNormalFormsWO]
DnUnt [definition, in NoUniqueNormalFormsWO]
DSnUSnt_eq_DDnUnUt [lemma, in NoUniqueNormalFormsWO]
DU [definition, in NoUniqueNormalFormsWO]
DU_l [definition, in NoUniqueNormalFormsWO]
DU_r [definition, in NoUniqueNormalFormsWO]
DU_in [lemma, in NoUniqueNormalFormsWO]
D2nt [definition, in NoUniqueNormalFormsWO]
D2nU2nt [definition, in NoUniqueNormalFormsWO]
D2nU2nt_eq_D2nU2nt [lemma, in NoUniqueNormalFormsWO]
D2SnU2Snt_eq_DDD2nU2nUUt [lemma, in NoUniqueNormalFormsWO]
E
embed [inductive, in Rewriting]embed_strict_trans [lemma, in Rewriting]
embed_strict_append_DnU2npsin_DSnU2SnpsiSn [lemma, in NoUniqueNormalFormsWO]
embed_refl [lemma, in Rewriting]
embed_cons_elim [lemma, in Rewriting]
embed_not_cons_nil [lemma, in Rewriting]
embed_append_right [lemma, in Rewriting]
embed_strict_append_Unpsin_USnpsiSn [lemma, in NoUniqueNormalFormsWO]
embed_not_snoc_nil [lemma, in Rewriting]
embed_not_pred_right_strong [lemma, in Rewriting]
embed_pred_left [lemma, in Rewriting]
Embed_Nil [constructor, in Rewriting]
embed_pred_right [lemma, in Rewriting]
Embed_Cons [constructor, in Rewriting]
embed_snoc_right [lemma, in Rewriting]
embed_strict_embed [lemma, in Rewriting]
embed_snoc_elim [lemma, in Rewriting]
embed_lim_right [lemma, in Rewriting]
embed_not_append_pred_left [lemma, in Rewriting]
embed_strict_cons_right [lemma, in Rewriting]
embed_cons_left [lemma, in Rewriting]
embed_strict [definition, in Rewriting]
Embed_Lim [constructor, in Rewriting]
embed_length [lemma, in Rewriting]
embed_not_pred_right [lemma, in Rewriting]
embed_trans [lemma, in Rewriting]
embed_cons_right [lemma, in Rewriting]
embed_cons_intro [lemma, in Rewriting]
embed_not_cons [lemma, in Rewriting]
empty_substitution [definition, in Substitution]
empty_substitution_is_id' [lemma, in Substitution]
empty_substitution_is_id [lemma, in Substitution]
eq_up_to_rewriting_depth [lemma, in Rewriting]
ExampleABA [library]
exp [definition, in Ordinal]
F
F [definition, in ExampleABA]F [definition, in NoUniqueNormalFormsWO]
fact_term_bis_A [lemma, in ExampleABA]
fact_term_bis_DmUSnDSnt [lemma, in NoUniqueNormalFormsWO]
fact_term_eq_UmDnUnt [lemma, in NoUniqueNormalFormsWO]
fact_term_bis_BnBA [lemma, in ExampleABA]
fact_term_bis_nBA [lemma, in ExampleABA]
fact_term_bis_DmUnDnt [lemma, in NoUniqueNormalFormsWO]
fact_term_bis_psi [lemma, in NoUniqueNormalFormsWOElaborated]
fact_b [lemma, in Ordinal]
fact_term_bis_UmDSnUSnt [lemma, in NoUniqueNormalFormsWO]
fact_a [lemma, in Ordinal]
fact_term_bis_BBA [lemma, in ExampleABA]
fact_term_bis_BA' [lemma, in ExampleABA]
fact_term_bis_Upsi1 [lemma, in NoUniqueNormalFormsWOElaborated]
fact_term_eq_DmUnDnt [lemma, in NoUniqueNormalFormsWO]
fact_term_bis_BA [lemma, in ExampleABA]
fact_term_bis_UmDnUnt [lemma, in NoUniqueNormalFormsWO]
FFun [constructor, in FiniteTerm]
fill [definition, in Context]
fill_Unc_t [lemma, in NoUniqueNormalFormsWO]
fill_term_bis [lemma, in Context]
fill_DnHole_t [lemma, in NoUniqueNormalFormsWO]
fill_eq_up_to [lemma, in Context]
fill_UnHole_t [lemma, in NoUniqueNormalFormsWO]
fill_UmDnHole_t [lemma, in NoUniqueNormalFormsWO]
fill_context_bis [lemma, in ContextEquality]
fill_DmUnc_t [lemma, in NoUniqueNormalFormsWO]
fill_UmDnc_t [lemma, in NoUniqueNormalFormsWO]
fill_Dnc_t [lemma, in NoUniqueNormalFormsWO]
fill_DmUnHole_t [lemma, in NoUniqueNormalFormsWO]
Fin [inductive, in Vector]
finite [definition, in Rewriting]
FiniteTerm [section, in FiniteTerm]
FiniteTerm [library]
FiniteTerm.F [variable, in FiniteTerm]
FiniteTerm.X [variable, in FiniteTerm]
finite_subterm [definition, in Term]
finite_s_psi_DSnU2SnpsiSn [lemma, in NoUniqueNormalFormsWO]
finite_term_as_term [definition, in Term]
finite_term [inductive, in FiniteTerm]
finite_s_DmUnDnt_Dmt [lemma, in NoUniqueNormalFormsWO]
finite_s_DnU2npsin_DSnU2SnpsiSn_helper [lemma, in NoUniqueNormalFormsWO]
finite_s_psi_Unpsin [lemma, in NoUniqueNormalFormsWO]
finite_s_UmDnUnt_Umt [lemma, in NoUniqueNormalFormsWO]
finite_s_psi_DSnU2SnpsiSn_helper [lemma, in NoUniqueNormalFormsWO]
finite_s_DnU2npsin_DSnU2SnpsiSn [lemma, in NoUniqueNormalFormsWO]
finite_s_Unpsin_USnpsiSn [lemma, in NoUniqueNormalFormsWO]
Fin_0_inv [lemma, in Vector]
First [constructor, in Vector]
first_pred_after_cons_id [lemma, in Rewriting]
first_pd_after_succ_id [lemma, in Ordinal]
Fold [section, in Vector]
Fold.A [variable, in Vector]
Fold.b [variable, in Vector]
Fold.B [variable, in Vector]
Fold.f [variable, in Vector]
fterm [abbreviation, in Rewriting]
fterm [abbreviation, in ExampleABA]
fterm [abbreviation, in Term]
fterm [abbreviation, in Rewriting]
fterm [abbreviation, in NoUniqueNormalFormsWO]
fterm [abbreviation, in Substitution]
fterm [abbreviation, in FiniteTerm]
fterm [abbreviation, in Term]
fterms [abbreviation, in FiniteTerm]
fterms [abbreviation, in Term]
ftest_BA [definition, in ExampleABA]
ftest_BBA [definition, in ExampleABA]
ftest_A [definition, in ExampleABA]
Fun [constructor, in Term]
Fun_inf [constructor, in Term]
Fun_bis [constructor, in TermEquality]
FVar [constructor, in FiniteTerm]
H
helper [lemma, in NoUniqueNormalFormsWOElaborated]Hole [constructor, in Context]
hole_depth [definition, in Context]
hole_position_depth [lemma, in Context]
Hole_bis [constructor, in ContextEquality]
hole_position [definition, in Context]
I
id_sub [abbreviation, in NoUniqueNormalFormsWOElaborated]id_sub [abbreviation, in ExampleABA]
InductionPrinciple [section, in NoUniqueNormalFormsWOElaborated]
InductionPrinciple.H1 [variable, in NoUniqueNormalFormsWOElaborated]
InductionPrinciple.H2 [variable, in NoUniqueNormalFormsWOElaborated]
InductionPrinciple.H3 [variable, in NoUniqueNormalFormsWOElaborated]
InductionPrinciple.P [variable, in NoUniqueNormalFormsWOElaborated]
infinite [definition, in Term]
infinite_repeat_U [lemma, in NoUniqueNormalFormsWOElaborated]
infinite_nf_repeat_U [lemma, in NoUniqueNormalFormsWOElaborated]
infinite_repeat_D [lemma, in NoUniqueNormalFormsWOElaborated]
infinite_nf_repeat_D [lemma, in NoUniqueNormalFormsWOElaborated]
is_var [definition, in Term]
is_cons_s_DmUnDnt_Dmt [lemma, in NoUniqueNormalFormsWO]
is_cons_s_DnU2npsin_DSnU2SnpsiSn_helper [lemma, in NoUniqueNormalFormsWO]
is_cons [definition, in NoUniqueNormalFormsWO]
is_limit [definition, in WfOrdinal]
is_succ [definition, in WfOrdinal]
is_cons_s_DnU2npsin_DSnU2SnpsiSn [lemma, in NoUniqueNormalFormsWO]
is_cons_snoc [lemma, in NoUniqueNormalFormsWO]
L
left_linear [definition, in Rewriting]left_linear_UD [lemma, in NoUniqueNormalFormsWO]
length [definition, in Rewriting]
length_s_A_repeat_B_le_omega [lemma, in ExampleABA]
length_s_A_repeat_B_eq_omega [lemma, in ExampleABA]
le_implies_ord_le [lemma, in Ordinal]
lhs [projection, in Rewriting]
Lim [constructor, in Rewriting]
limit [definition, in WfOrdinal]
Limit [constructor, in Ordinal]
linear [definition, in FiniteTerm]
lt_implies_ord_lt [lemma, in Ordinal]
lt_plus_minus_r [lemma, in Context]
M
Map [section, in Vector]Map.A [variable, in Vector]
Map.B [variable, in Vector]
Map.f [variable, in Vector]
mul [definition, in Ordinal]
N
nat_as_ord [definition, in Ordinal]nat_wf [lemma, in WfOrdinal]
nat_as_wf_ord [definition, in WfOrdinal]
nB_Hole [definition, in ExampleABA]
nB_A [definition, in ExampleABA]
neq_repeat_D_repeat_U [lemma, in NoUniqueNormalFormsWO]
Next [constructor, in Vector]
Nil [abbreviation, in ExampleABA]
Nil [constructor, in Rewriting]
Nil' [abbreviation, in NoUniqueNormalFormsWO]
normal_form [definition, in Rewriting]
normal_form_repeat_D [lemma, in NoUniqueNormalFormsWO]
normal_form_repeat_U [lemma, in NoUniqueNormalFormsWO]
NoUniqueNormalFormsWO [library]
NoUniqueNormalFormsWOElaborated [library]
no_unique_normal_forms_UD [lemma, in NoUniqueNormalFormsWO]
no_unique_normal_forms_wo [lemma, in NoUniqueNormalFormsWO]
n_lt_omega [lemma, in WfOrdinal]
n_le_omega [lemma, in WfOrdinal]
O
oldpsi [definition, in NoUniqueNormalFormsWOElaborated]oldpsi' [definition, in NoUniqueNormalFormsWOElaborated]
omega [definition, in Ordinal]
omega_le_length_s_A_repeat_B [lemma, in ExampleABA]
ord [inductive, in Ordinal]
Ordinal [library]
ord_le_add [lemma, in Ordinal]
ord_lt_lt [lemma, in Ordinal]
ord_le_succ_right [lemma, in Ordinal]
ord_lt_zero_zero [lemma, in Ordinal]
Ord_le_Succ [constructor, in Ordinal]
ord_le_limit_left [lemma, in Ordinal]
Ord_le_Zero [constructor, in Ordinal]
ord_le [inductive, in Ordinal]
ord_lt_add [lemma, in Ordinal]
ord_le_le [lemma, in Ordinal]
ord_lt_succ_right [lemma, in Ordinal]
ord_lt_not_ord_le [lemma, in Ordinal]
ord_le_refl [lemma, in Ordinal]
ord_le_pd_left [lemma, in Ordinal]
ord_le_succ_left [lemma, in Ordinal]
ord_le_succ_intro [lemma, in Ordinal]
ord_lt_implies_lt [lemma, in Ordinal]
ord_le_implies_le [lemma, in Ordinal]
ord_le_omega_elim [lemma, in WfOrdinal]
ord_le_trans [lemma, in Ordinal]
ord_le_limit_right [lemma, in Ordinal]
ord_lt_ord_le_succ [lemma, in Ordinal]
ord_lt [definition, in Ordinal]
ord_lt_asymm [lemma, in Ordinal]
ord_le_pd_right [lemma, in Ordinal]
ord_le_succ_pd_right [lemma, in Ordinal]
ord_lt_succ_left [lemma, in Ordinal]
ord_le_not_succ_succ_one [lemma, in Ordinal]
ord_eq_trans [lemma, in Ordinal]
ord_eq_omega_discriminate [lemma, in Ordinal]
ord_le_not_pd_right_weak [lemma, in Ordinal]
ord_lt_irrefl [lemma, in Ordinal]
ord_le_zero_right [lemma, in Ordinal]
ord_le_not_pd_right [lemma, in Ordinal]
ord_eq [definition, in Ordinal]
ord_le_succ_elim [lemma, in Ordinal]
ord_eq_refl [lemma, in Ordinal]
ord_le_not_succ [lemma, in Ordinal]
ord_lt_ord_le [lemma, in Ordinal]
ord_eq_symm [lemma, in Ordinal]
Ord_le_Limit [constructor, in Ordinal]
ord_le_add_right [lemma, in Ordinal]
ord_le_antisymm [lemma, in Ordinal]
ord_le_not_succ_zero [lemma, in Ordinal]
ord_lt_trans [lemma, in Ordinal]
orthogonal [definition, in Rewriting]
P
pattern_depth [definition, in FiniteTerm]pd [definition, in Ordinal]
pd_type_pred_type_inv [lemma, in Rewriting]
pd_type_as_pred_type [definition, in Rewriting]
pd_trans [lemma, in Ordinal]
pd_type_as_pred_type_ok [lemma, in Rewriting]
pd_type [definition, in Ordinal]
peek [definition, in Term]
peek_eq [lemma, in Term]
position [abbreviation, in Term]
Position [section, in Term]
PositionEquality [section, in TermEquality]
PositionEquality.F [variable, in TermEquality]
PositionEquality.X [variable, in TermEquality]
position_depth [definition, in Term]
Position.F [variable, in Term]
Position.X [variable, in Term]
pos_eq [definition, in TermEquality]
pred [definition, in Rewriting]
pred_type [definition, in Rewriting]
pred_append [lemma, in Rewriting]
pred_type_as_pd_type [definition, in Rewriting]
pred_type_as_pd_type_ok [lemma, in Rewriting]
pred_trans [lemma, in Rewriting]
Prelims [library]
psi [definition, in NoUniqueNormalFormsWO]
psin_eq_DS2nUS2nUpsiSn [lemma, in NoUniqueNormalFormsWO]
psin_eq_DD2nU2nUUpsiSn [lemma, in NoUniqueNormalFormsWO]
psi' [definition, in NoUniqueNormalFormsWO]
p_Upsi1_UDDUUUpsi2 [definition, in NoUniqueNormalFormsWOElaborated]
p_A_BA [definition, in ExampleABA]
p_psi_Upsi1 [definition, in NoUniqueNormalFormsWOElaborated]
p_DmUSnDSnt_DmUnDnt [definition, in NoUniqueNormalFormsWO]
p_BA_BBA [definition, in ExampleABA]
p_nBA_nBBA [definition, in ExampleABA]
p_UmDSnUSnt_UmDnUnt [definition, in NoUniqueNormalFormsWO]
R
repeat_D_repeat_U_only_infinite_normal_forms_alt [lemma, in NoUniqueNormalFormsWOElaborated]repeat_D_repeat_U_only_infinite_normal_forms [lemma, in NoUniqueNormalFormsWOElaborated]
repeat_D [definition, in NoUniqueNormalFormsWO]
repeat_DU [definition, in NoUniqueNormalFormsWOElaborated]
repeat_B [definition, in ExampleABA]
repeat_U [definition, in NoUniqueNormalFormsWO]
repeat_DU_rewrites_to_itself [lemma, in NoUniqueNormalFormsWOElaborated]
Rewriting [library]
rhs [projection, in Rewriting]
root [definition, in Term]
Rule [section, in Rewriting]
rule [record, in Rewriting]
Rule [constructor, in Rewriting]
rule_wf [projection, in Rewriting]
Rule.F [variable, in Rewriting]
Rule.X [variable, in Rewriting]
S
sequence [inductive, in Rewriting]sequence_rect [definition, in Rewriting]
sequence_ind [definition, in Rewriting]
Signature [constructor, in Signature]
signature [record, in Signature]
Signature [library]
size [definition, in FiniteTerm]
snoc [definition, in Rewriting]
snoc_embed_strict [lemma, in Rewriting]
snoc_embed [lemma, in Rewriting]
snoc_finite [lemma, in Rewriting]
snoc_rec [definition, in Rewriting]
snoc_wf [lemma, in Rewriting]
snoc_weakly_convergent [lemma, in Rewriting]
snoc_weakly_convergent_helper [lemma, in Rewriting]
Step [constructor, in Rewriting]
Step [abbreviation, in ExampleABA]
step [inductive, in Rewriting]
Step [abbreviation, in NoUniqueNormalFormsWO]
step_eq_target [lemma, in Rewriting]
step_eq_symm [lemma, in Rewriting]
step_eq_trans [lemma, in Rewriting]
step_eq_refl [lemma, in Rewriting]
step_eq [definition, in Rewriting]
step_eq_source [lemma, in Rewriting]
strongly_convergent [definition, in Rewriting]
substitute [definition, in Substitution]
substitute' [definition, in Substitution]
substitution [abbreviation, in Rewriting]
Substitution [section, in Substitution]
substitution [definition, in Substitution]
Substitution [library]
substitutions_related [lemma, in Substitution]
substitution_eq_app_right [lemma, in Substitution]
substitution_eq_symm [lemma, in Substitution]
substitution_eq_app_left [lemma, in Substitution]
substitution_eq_refl [lemma, in Substitution]
substitution_eq_substitute [lemma, in Substitution]
substitution_eq_incl [lemma, in Substitution]
substitution_eq [definition, in Substitution]
substitution_eq_trans [lemma, in Substitution]
Substitution.F [variable, in Substitution]
Substitution.X [variable, in Substitution]
subterm [definition, in Term]
sub_psi_Upsi1 [definition, in NoUniqueNormalFormsWOElaborated]
sub_t [definition, in NoUniqueNormalFormsWO]
sub_Upsi1_UDDUUUpsi2 [definition, in NoUniqueNormalFormsWOElaborated]
Succ [constructor, in Ordinal]
succ [definition, in WfOrdinal]
symbol [projection, in Signature]
symbol [inductive, in ExampleABA]
symbol [inductive, in NoUniqueNormalFormsWO]
s_A_BBA [definition, in ExampleABA]
s_psi_UDDUUUpsi2 [definition, in NoUniqueNormalFormsWOElaborated]
s_psi_repeat_U [definition, in NoUniqueNormalFormsWO]
s_A_BA [definition, in ExampleABA]
s_A_repeat_B [definition, in ExampleABA]
s_UmDnUnt_Umt_is_cons [lemma, in NoUniqueNormalFormsWO]
s_DnU2npsin_DSnU2SnpsiSn [definition, in NoUniqueNormalFormsWO]
s_DmUnDnt_Dmt [definition, in NoUniqueNormalFormsWO]
s_A_nBA [definition, in ExampleABA]
s_psi_DSnU2SnpsiSn [definition, in NoUniqueNormalFormsWO]
s_psi_Upsi1 [definition, in NoUniqueNormalFormsWOElaborated]
s_UmDnUnt_Umt [definition, in NoUniqueNormalFormsWO]
s_Unpsin_USnpsiSn [definition, in NoUniqueNormalFormsWO]
s_psi_repeat_D [definition, in NoUniqueNormalFormsWO]
s_psi_Unpsin [definition, in NoUniqueNormalFormsWO]
S_eq_inv [definition, in Prelims]
s_A [definition, in ExampleABA]
s_psi_psi [definition, in NoUniqueNormalFormsWOElaborated]
S_eq [definition, in Prelims]
T
term [abbreviation, in NoUniqueNormalFormsWO]term [abbreviation, in TermEquality]
term [abbreviation, in TermEquality]
term [abbreviation, in Term]
term [abbreviation, in Context]
term [abbreviation, in Rewriting]
term [abbreviation, in ExampleABA]
term [abbreviation, in Substitution]
term [abbreviation, in ContextEquality]
Term [section, in Term]
term [inductive, in Term]
Term [library]
TermEquality [section, in TermEquality]
TermEquality [library]
TermEquality.F [variable, in TermEquality]
TermEquality.X [variable, in TermEquality]
terms [abbreviation, in Context]
terms [abbreviation, in Term]
terms [abbreviation, in ContextEquality]
terms [abbreviation, in TermEquality]
terms [abbreviation, in TermEquality]
terms [abbreviation, in NoUniqueNormalFormsWO]
term_eq_up_to_n_nB_A_repeat_B [lemma, in ExampleABA]
term_bis_U [lemma, in NoUniqueNormalFormsWO]
term_eq_implies_term_bis [lemma, in TermEquality]
term_bis_D [lemma, in NoUniqueNormalFormsWO]
term_eq_trans [lemma, in TermEquality]
term_eq_fun_inv [lemma, in TermEquality]
term_bis_implies_term_eq [lemma, in TermEquality]
term_eq_up_to_n_Unt_repeat_U [lemma, in NoUniqueNormalFormsWO]
term_bis_Dnt [lemma, in NoUniqueNormalFormsWO]
term_eq_up_to_refl [lemma, in TermEquality]
term_eq_up_to_weaken [lemma, in TermEquality]
term_bis_term_eq [lemma, in TermEquality]
term_bis [inductive, in TermEquality]
term_eq_up_to_n_Dnt_repeat_D [lemma, in NoUniqueNormalFormsWO]
term_eq_up_to_symm [lemma, in TermEquality]
term_eq_up_to_trans [lemma, in TermEquality]
term_eq_up_to_weaken_generalized [lemma, in TermEquality]
term_bis_symm [lemma, in TermEquality]
term_eq_refl [lemma, in TermEquality]
term_eq_symm [lemma, in TermEquality]
term_inf [inductive, in Term]
term_bis_refl [lemma, in TermEquality]
term_eq [definition, in TermEquality]
term_eq_up_to [inductive, in TermEquality]
term_eq_fun_inv_symbol [lemma, in TermEquality]
term_bis_trans [lemma, in TermEquality]
term_inf_repeat_U [lemma, in NoUniqueNormalFormsWOElaborated]
term_inf_repeat_D [lemma, in NoUniqueNormalFormsWOElaborated]
term_bis_Unt [lemma, in NoUniqueNormalFormsWO]
Term.F [variable, in Term]
Term.X [variable, in Term]
test_BA [definition, in ExampleABA]
test_BBA [definition, in ExampleABA]
test_A [definition, in ExampleABA]
teut_0 [constructor, in TermEquality]
teut_var [constructor, in TermEquality]
teut_fun_inv [lemma, in TermEquality]
teut_fun [constructor, in TermEquality]
trs [abbreviation, in NoUniqueNormalFormsWO]
TRS [section, in Rewriting]
trs [abbreviation, in Rewriting]
trs [definition, in Rewriting]
trs [abbreviation, in ExampleABA]
trs_left_linear [definition, in Rewriting]
TRS.F [variable, in Rewriting]
TRS.InductionPrinciple [section, in Rewriting]
TRS.InductionPrinciple.H1 [variable, in Rewriting]
TRS.InductionPrinciple.H2 [variable, in Rewriting]
TRS.InductionPrinciple.H3 [variable, in Rewriting]
TRS.InductionPrinciple.P [variable, in Rewriting]
TRS.system [variable, in Rewriting]
TRS.X [variable, in Rewriting]
_ [>] _ [notation, in Rewriting]
_ [seq _ ] [notation, in Rewriting]
_ < _ [notation, in Rewriting]
_ [ _ ] [notation, in Rewriting]
_ [1 _ ] [notation, in Rewriting]
_ <= _ [notation, in Rewriting]
_ [2 _ ] [notation, in Rewriting]
_ ->> _ [notation, in Rewriting]
_ ->> _ [notation, in Rewriting]
_ [stp _ ] [notation, in Rewriting]
U
U [constructor, in NoUniqueNormalFormsWO]UD [definition, in NoUniqueNormalFormsWO]
UD_l [definition, in NoUniqueNormalFormsWO]
UD_trs [definition, in NoUniqueNormalFormsWO]
UD_in [lemma, in NoUniqueNormalFormsWO]
UD_r [definition, in NoUniqueNormalFormsWO]
Unc [definition, in NoUniqueNormalFormsWO]
UnDnt [definition, in NoUniqueNormalFormsWO]
unique_normal_forms [definition, in Rewriting]
Unt [definition, in NoUniqueNormalFormsWO]
USnDSnt_eq_UUnDnDt [lemma, in NoUniqueNormalFormsWO]
UUnt_eq_UnUt [lemma, in NoUniqueNormalFormsWO]
UUSnt_eq_USnUt [lemma, in NoUniqueNormalFormsWOElaborated]
UU2nt_eq_U2nUt [lemma, in NoUniqueNormalFormsWO]
UU2nt_eq_U2nUt_unfolded [lemma, in NoUniqueNormalFormsWO]
U2nD2nt [definition, in NoUniqueNormalFormsWO]
U2nt [definition, in NoUniqueNormalFormsWO]
U2SnD2Snt_eq_UUU2nD2nDDt [lemma, in NoUniqueNormalFormsWO]
V
vappend [definition, in Vector]Var [constructor, in Term]
variable [definition, in NoUniqueNormalFormsWO]
variable [projection, in Variables]
variable [definition, in ExampleABA]
Variables [constructor, in Variables]
variables [record, in Variables]
Variables [library]
vars [definition, in FiniteTerm]
varx [definition, in NoUniqueNormalFormsWO]
Var_bis [constructor, in TermEquality]
vcast [definition, in Vector]
vcast_vcons [lemma, in Vector]
vcast_intro [lemma, in Vector]
vcons [definition, in Vector]
vcons_vhead_vtail [lemma, in Vector]
vdrop [definition, in Vector]
vector [definition, in Vector]
Vector [section, in Vector]
Vector [library]
Vector.A [variable, in Vector]
vfold [definition, in Vector]
vhead [definition, in Vector]
vmap [definition, in Vector]
vnil [definition, in Vector]
vnth [definition, in Vector]
vtail [definition, in Vector]
vtail_vcons [lemma, in Vector]
vtake [definition, in Vector]
W
weakly_orthogonal_UD [lemma, in NoUniqueNormalFormsWO]weakly_convergent [definition, in Rewriting]
weakly_orthogonal [definition, in Rewriting]
weakly_convergent_finite [lemma, in Rewriting]
wf [definition, in WfOrdinal]
wf [definition, in Rewriting]
WfOrdinal [library]
wf_UD [lemma, in NoUniqueNormalFormsWO]
wf_DU [lemma, in NoUniqueNormalFormsWO]
wf_ord_as_ord [definition, in WfOrdinal]
wf_ord_eq_ord_eq [lemma, in WfOrdinal]
wf_s_psi_DSnU2SnpsiSn [lemma, in NoUniqueNormalFormsWO]
wf_ord_le_zero_right [lemma, in WfOrdinal]
wf_s_psi_repeat_U [lemma, in NoUniqueNormalFormsWO]
wf_ord_eq [definition, in WfOrdinal]
wf_ord_le [definition, in WfOrdinal]
wf_ord_lt [definition, in WfOrdinal]
wf_omega [definition, in WfOrdinal]
wf_s_psi_Unpsin [lemma, in NoUniqueNormalFormsWO]
wf_finite [lemma, in Rewriting]
wf_s_A_repeat_B [lemma, in ExampleABA]
wf_ord [definition, in WfOrdinal]
wf_s_psi_repeat_D [lemma, in NoUniqueNormalFormsWO]
X
X [definition, in NoUniqueNormalFormsWO]X [definition, in ExampleABA]
Z
Zero [constructor, in Ordinal]zero [definition, in WfOrdinal]
other
_ == _ (ord_scope) [notation, in Ordinal]_ <= _ (ord_scope) [notation, in Ordinal]
_ [ _ ] (ord_scope) [notation, in Ordinal]
_ < _ (ord_scope) [notation, in Ordinal]
_
_
_ =wf= _ (wf_ord_scope) [notation, in WfOrdinal]
_ [seq _ ] [notation, in NoUniqueNormalFormsWO]
_ @ _ [notation, in NoUniqueNormalFormsWO]
_ [=] _ [notation, in TermEquality]
_ [2 _ ] [notation, in NoUniqueNormalFormsWO]
_ [1 _ ] [notation, in NoUniqueNormalFormsWO]
_ @@ _ [notation, in NoUniqueNormalFormsWO]
_ ! [notation, in ExampleABA]
_ ->> _ [notation, in ExampleABA]
_ @@@ _ [notation, in NoUniqueNormalFormsWO]
_ @ _ [notation, in ExampleABA]
_ @@ _ [notation, in ExampleABA]
_ [>] _ [notation, in ExampleABA]
_ @@@ _ [notation, in ExampleABA]
_ !! [notation, in ExampleABA]
_ [~] _ [notation, in TermEquality]
_ ! [notation, in NoUniqueNormalFormsWO]
_ [>] _ [notation, in NoUniqueNormalFormsWO]
_ ->> _ [notation, in NoUniqueNormalFormsWO]
_ [stp _ ] [notation, in NoUniqueNormalFormsWO]
_ [ _ ] [notation, in NoUniqueNormalFormsWO]
! [notation, in Prelims]
Projection Index
A
arity [in Signature]B
beq_symb_ok [in Signature]beq_var_ok [in Variables]
beq_var [in Variables]
beq_symb [in Signature]
L
lhs [in Rewriting]R
rhs [in Rewriting]rule_wf [in Rewriting]
S
symbol [in Signature]V
variable [in Variables]Record Index
R
rule [in Rewriting]S
signature [in Signature]V
variables [in Variables]Lemma Index
A
aa [in NoUniqueNormalFormsWOElaborated]ABA_left_linear [in ExampleABA]
ABA_in [in ExampleABA]
ABA_wf [in ExampleABA]
add_wf [in WfOrdinal]
all_terms_eq_up_to_0 [in Rewriting]
all_terms_eq_up_to_d_s_Udpsid_USdpsiSd_repeat_U [in NoUniqueNormalFormsWOElaborated]
all_terms_eq_up_to_d_s_UdDnUnt_Udt_repeat_U [in NoUniqueNormalFormsWOElaborated]
all_terms_eq_up_to_snoc [in Rewriting]
append_is_cons [in NoUniqueNormalFormsWO]
append_embed [in Rewriting]
append_wf [in Rewriting]
append_length [in Rewriting]
append_embed_strict [in Rewriting]
append_finite [in Rewriting]
B
bb [in NoUniqueNormalFormsWOElaborated]beq_var_ok [in ExampleABA]
beq_symb_ok [in ExampleABA]
beq_symb_ok [in NoUniqueNormalFormsWO]
beq_var_ok [in NoUniqueNormalFormsWO]
C
ccD [in NoUniqueNormalFormsWOElaborated]ccU [in NoUniqueNormalFormsWOElaborated]
ceut_fun_inv_v [in ContextEquality]
ceut_fun_inv [in ContextEquality]
ceut_fun_inv_w [in ContextEquality]
context_bis_symm [in ContextEquality]
context_eq_fun_inv_i [in ContextEquality]
context_bis_trans [in ContextEquality]
context_bis_refl [in ContextEquality]
context_bis_implies_context_eq [in ContextEquality]
context_eq_implies_context_bis [in ContextEquality]
context_bis_context_eq [in ContextEquality]
context_eq_fun_inv_v [in ContextEquality]
context_eq_fun_inv_j [in ContextEquality]
context_eq_fun_inv_symbol [in ContextEquality]
context_eq_fun_inv [in ContextEquality]
context_eq_fun_inv_w [in ContextEquality]
converges_nB_A [in ExampleABA]
converges_Unpsin [in NoUniqueNormalFormsWO]
converges_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
critical_pairs_trivial_UD [in NoUniqueNormalFormsWO]
critical_pair_Ux_Ux [in NoUniqueNormalFormsWOElaborated]
D
DDnt_eq_DnDt [in NoUniqueNormalFormsWO]DD2nt_eq_D2nDt [in NoUniqueNormalFormsWO]
DSnUSnt_eq_DDnUnUt [in NoUniqueNormalFormsWO]
DU_in [in NoUniqueNormalFormsWO]
D2nU2nt_eq_D2nU2nt [in NoUniqueNormalFormsWO]
D2SnU2Snt_eq_DDD2nU2nUUt [in NoUniqueNormalFormsWO]
E
embed_strict_trans [in Rewriting]embed_strict_append_DnU2npsin_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
embed_refl [in Rewriting]
embed_cons_elim [in Rewriting]
embed_not_cons_nil [in Rewriting]
embed_append_right [in Rewriting]
embed_strict_append_Unpsin_USnpsiSn [in NoUniqueNormalFormsWO]
embed_not_snoc_nil [in Rewriting]
embed_not_pred_right_strong [in Rewriting]
embed_pred_left [in Rewriting]
embed_pred_right [in Rewriting]
embed_snoc_right [in Rewriting]
embed_strict_embed [in Rewriting]
embed_snoc_elim [in Rewriting]
embed_lim_right [in Rewriting]
embed_not_append_pred_left [in Rewriting]
embed_strict_cons_right [in Rewriting]
embed_cons_left [in Rewriting]
embed_length [in Rewriting]
embed_not_pred_right [in Rewriting]
embed_trans [in Rewriting]
embed_cons_right [in Rewriting]
embed_cons_intro [in Rewriting]
embed_not_cons [in Rewriting]
empty_substitution_is_id' [in Substitution]
empty_substitution_is_id [in Substitution]
eq_up_to_rewriting_depth [in Rewriting]
F
fact_term_bis_A [in ExampleABA]fact_term_bis_DmUSnDSnt [in NoUniqueNormalFormsWO]
fact_term_eq_UmDnUnt [in NoUniqueNormalFormsWO]
fact_term_bis_BnBA [in ExampleABA]
fact_term_bis_nBA [in ExampleABA]
fact_term_bis_DmUnDnt [in NoUniqueNormalFormsWO]
fact_term_bis_psi [in NoUniqueNormalFormsWOElaborated]
fact_b [in Ordinal]
fact_term_bis_UmDSnUSnt [in NoUniqueNormalFormsWO]
fact_a [in Ordinal]
fact_term_bis_BBA [in ExampleABA]
fact_term_bis_BA' [in ExampleABA]
fact_term_bis_Upsi1 [in NoUniqueNormalFormsWOElaborated]
fact_term_eq_DmUnDnt [in NoUniqueNormalFormsWO]
fact_term_bis_BA [in ExampleABA]
fact_term_bis_UmDnUnt [in NoUniqueNormalFormsWO]
fill_Unc_t [in NoUniqueNormalFormsWO]
fill_term_bis [in Context]
fill_DnHole_t [in NoUniqueNormalFormsWO]
fill_eq_up_to [in Context]
fill_UnHole_t [in NoUniqueNormalFormsWO]
fill_UmDnHole_t [in NoUniqueNormalFormsWO]
fill_context_bis [in ContextEquality]
fill_DmUnc_t [in NoUniqueNormalFormsWO]
fill_UmDnc_t [in NoUniqueNormalFormsWO]
fill_Dnc_t [in NoUniqueNormalFormsWO]
fill_DmUnHole_t [in NoUniqueNormalFormsWO]
finite_s_psi_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
finite_s_DmUnDnt_Dmt [in NoUniqueNormalFormsWO]
finite_s_DnU2npsin_DSnU2SnpsiSn_helper [in NoUniqueNormalFormsWO]
finite_s_psi_Unpsin [in NoUniqueNormalFormsWO]
finite_s_UmDnUnt_Umt [in NoUniqueNormalFormsWO]
finite_s_psi_DSnU2SnpsiSn_helper [in NoUniqueNormalFormsWO]
finite_s_DnU2npsin_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
finite_s_Unpsin_USnpsiSn [in NoUniqueNormalFormsWO]
Fin_0_inv [in Vector]
first_pred_after_cons_id [in Rewriting]
first_pd_after_succ_id [in Ordinal]
H
helper [in NoUniqueNormalFormsWOElaborated]hole_position_depth [in Context]
I
infinite_repeat_U [in NoUniqueNormalFormsWOElaborated]infinite_nf_repeat_U [in NoUniqueNormalFormsWOElaborated]
infinite_repeat_D [in NoUniqueNormalFormsWOElaborated]
infinite_nf_repeat_D [in NoUniqueNormalFormsWOElaborated]
is_cons_s_DmUnDnt_Dmt [in NoUniqueNormalFormsWO]
is_cons_s_DnU2npsin_DSnU2SnpsiSn_helper [in NoUniqueNormalFormsWO]
is_cons_s_DnU2npsin_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
is_cons_snoc [in NoUniqueNormalFormsWO]
L
left_linear_UD [in NoUniqueNormalFormsWO]length_s_A_repeat_B_le_omega [in ExampleABA]
length_s_A_repeat_B_eq_omega [in ExampleABA]
le_implies_ord_le [in Ordinal]
lt_implies_ord_lt [in Ordinal]
lt_plus_minus_r [in Context]
N
nat_wf [in WfOrdinal]neq_repeat_D_repeat_U [in NoUniqueNormalFormsWO]
normal_form_repeat_D [in NoUniqueNormalFormsWO]
normal_form_repeat_U [in NoUniqueNormalFormsWO]
no_unique_normal_forms_UD [in NoUniqueNormalFormsWO]
no_unique_normal_forms_wo [in NoUniqueNormalFormsWO]
n_lt_omega [in WfOrdinal]
n_le_omega [in WfOrdinal]
O
omega_le_length_s_A_repeat_B [in ExampleABA]ord_le_add [in Ordinal]
ord_lt_lt [in Ordinal]
ord_le_succ_right [in Ordinal]
ord_lt_zero_zero [in Ordinal]
ord_le_limit_left [in Ordinal]
ord_lt_add [in Ordinal]
ord_le_le [in Ordinal]
ord_lt_succ_right [in Ordinal]
ord_lt_not_ord_le [in Ordinal]
ord_le_refl [in Ordinal]
ord_le_pd_left [in Ordinal]
ord_le_succ_left [in Ordinal]
ord_le_succ_intro [in Ordinal]
ord_lt_implies_lt [in Ordinal]
ord_le_implies_le [in Ordinal]
ord_le_omega_elim [in WfOrdinal]
ord_le_trans [in Ordinal]
ord_le_limit_right [in Ordinal]
ord_lt_ord_le_succ [in Ordinal]
ord_lt_asymm [in Ordinal]
ord_le_pd_right [in Ordinal]
ord_le_succ_pd_right [in Ordinal]
ord_lt_succ_left [in Ordinal]
ord_le_not_succ_succ_one [in Ordinal]
ord_eq_trans [in Ordinal]
ord_eq_omega_discriminate [in Ordinal]
ord_le_not_pd_right_weak [in Ordinal]
ord_lt_irrefl [in Ordinal]
ord_le_zero_right [in Ordinal]
ord_le_not_pd_right [in Ordinal]
ord_le_succ_elim [in Ordinal]
ord_eq_refl [in Ordinal]
ord_le_not_succ [in Ordinal]
ord_lt_ord_le [in Ordinal]
ord_eq_symm [in Ordinal]
ord_le_add_right [in Ordinal]
ord_le_antisymm [in Ordinal]
ord_le_not_succ_zero [in Ordinal]
ord_lt_trans [in Ordinal]
P
pd_type_pred_type_inv [in Rewriting]pd_trans [in Ordinal]
pd_type_as_pred_type_ok [in Rewriting]
peek_eq [in Term]
pred_append [in Rewriting]
pred_type_as_pd_type_ok [in Rewriting]
pred_trans [in Rewriting]
psin_eq_DS2nUS2nUpsiSn [in NoUniqueNormalFormsWO]
psin_eq_DD2nU2nUUpsiSn [in NoUniqueNormalFormsWO]
R
repeat_D_repeat_U_only_infinite_normal_forms_alt [in NoUniqueNormalFormsWOElaborated]repeat_D_repeat_U_only_infinite_normal_forms [in NoUniqueNormalFormsWOElaborated]
repeat_DU_rewrites_to_itself [in NoUniqueNormalFormsWOElaborated]
S
snoc_embed_strict [in Rewriting]snoc_embed [in Rewriting]
snoc_finite [in Rewriting]
snoc_wf [in Rewriting]
snoc_weakly_convergent [in Rewriting]
snoc_weakly_convergent_helper [in Rewriting]
step_eq_target [in Rewriting]
step_eq_symm [in Rewriting]
step_eq_trans [in Rewriting]
step_eq_refl [in Rewriting]
step_eq_source [in Rewriting]
substitutions_related [in Substitution]
substitution_eq_app_right [in Substitution]
substitution_eq_symm [in Substitution]
substitution_eq_app_left [in Substitution]
substitution_eq_refl [in Substitution]
substitution_eq_substitute [in Substitution]
substitution_eq_incl [in Substitution]
substitution_eq_trans [in Substitution]
s_UmDnUnt_Umt_is_cons [in NoUniqueNormalFormsWO]
T
term_eq_up_to_n_nB_A_repeat_B [in ExampleABA]term_bis_U [in NoUniqueNormalFormsWO]
term_eq_implies_term_bis [in TermEquality]
term_bis_D [in NoUniqueNormalFormsWO]
term_eq_trans [in TermEquality]
term_eq_fun_inv [in TermEquality]
term_bis_implies_term_eq [in TermEquality]
term_eq_up_to_n_Unt_repeat_U [in NoUniqueNormalFormsWO]
term_bis_Dnt [in NoUniqueNormalFormsWO]
term_eq_up_to_refl [in TermEquality]
term_eq_up_to_weaken [in TermEquality]
term_bis_term_eq [in TermEquality]
term_eq_up_to_n_Dnt_repeat_D [in NoUniqueNormalFormsWO]
term_eq_up_to_symm [in TermEquality]
term_eq_up_to_trans [in TermEquality]
term_eq_up_to_weaken_generalized [in TermEquality]
term_bis_symm [in TermEquality]
term_eq_refl [in TermEquality]
term_eq_symm [in TermEquality]
term_bis_refl [in TermEquality]
term_eq_fun_inv_symbol [in TermEquality]
term_bis_trans [in TermEquality]
term_inf_repeat_U [in NoUniqueNormalFormsWOElaborated]
term_inf_repeat_D [in NoUniqueNormalFormsWOElaborated]
term_bis_Unt [in NoUniqueNormalFormsWO]
teut_fun_inv [in TermEquality]
U
UD_in [in NoUniqueNormalFormsWO]USnDSnt_eq_UUnDnDt [in NoUniqueNormalFormsWO]
UUnt_eq_UnUt [in NoUniqueNormalFormsWO]
UUSnt_eq_USnUt [in NoUniqueNormalFormsWOElaborated]
UU2nt_eq_U2nUt [in NoUniqueNormalFormsWO]
UU2nt_eq_U2nUt_unfolded [in NoUniqueNormalFormsWO]
U2SnD2Snt_eq_UUU2nD2nDDt [in NoUniqueNormalFormsWO]
V
vcast_vcons [in Vector]vcast_intro [in Vector]
vcons_vhead_vtail [in Vector]
vtail_vcons [in Vector]
W
weakly_orthogonal_UD [in NoUniqueNormalFormsWO]weakly_convergent_finite [in Rewriting]
wf_UD [in NoUniqueNormalFormsWO]
wf_DU [in NoUniqueNormalFormsWO]
wf_ord_eq_ord_eq [in WfOrdinal]
wf_s_psi_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
wf_ord_le_zero_right [in WfOrdinal]
wf_s_psi_repeat_U [in NoUniqueNormalFormsWO]
wf_s_psi_Unpsin [in NoUniqueNormalFormsWO]
wf_finite [in Rewriting]
wf_s_A_repeat_B [in ExampleABA]
wf_s_psi_repeat_D [in NoUniqueNormalFormsWO]
Section Index
C
Cast [in Vector]Context [in Context]
ContextEquality [in ContextEquality]
F
FiniteTerm [in FiniteTerm]Fold [in Vector]
I
InductionPrinciple [in NoUniqueNormalFormsWOElaborated]M
Map [in Vector]P
Position [in Term]PositionEquality [in TermEquality]
R
Rule [in Rewriting]S
Substitution [in Substitution]T
Term [in Term]TermEquality [in TermEquality]
TRS [in Rewriting]
TRS.InductionPrinciple [in Rewriting]
V
Vector [in Vector]Constructor Index
A
A [in ExampleABA]B
B [in ExampleABA]C
ceut_hole [in ContextEquality]ceut_cfun [in ContextEquality]
ceut_0 [in ContextEquality]
CFun [in Context]
CFun_bis [in ContextEquality]
Cons [in Rewriting]
D
D [in NoUniqueNormalFormsWO]E
Embed_Nil [in Rewriting]Embed_Cons [in Rewriting]
Embed_Lim [in Rewriting]
F
FFun [in FiniteTerm]First [in Vector]
Fun [in Term]
Fun_inf [in Term]
Fun_bis [in TermEquality]
FVar [in FiniteTerm]
H
Hole [in Context]Hole_bis [in ContextEquality]
L
Lim [in Rewriting]Limit [in Ordinal]
N
Next [in Vector]Nil [in Rewriting]
O
Ord_le_Succ [in Ordinal]Ord_le_Zero [in Ordinal]
Ord_le_Limit [in Ordinal]
R
Rule [in Rewriting]S
Signature [in Signature]Step [in Rewriting]
Succ [in Ordinal]
T
teut_0 [in TermEquality]teut_var [in TermEquality]
teut_fun [in TermEquality]
U
U [in NoUniqueNormalFormsWO]V
Var [in Term]Variables [in Variables]
Var_bis [in TermEquality]
Z
Zero [in Ordinal]Notation Index
T
_ [>] _ [in Rewriting]_ [seq _ ] [in Rewriting]
_ < _ [in Rewriting]
_ [ _ ] [in Rewriting]
_ [1 _ ] [in Rewriting]
_ <= _ [in Rewriting]
_ [2 _ ] [in Rewriting]
_ ->> _ [in Rewriting]
_ ->> _ [in Rewriting]
_ [stp _ ] [in Rewriting]
other
_ == _ (ord_scope) [in Ordinal]_ <= _ (ord_scope) [in Ordinal]
_ [ _ ] (ord_scope) [in Ordinal]
_ < _ (ord_scope) [in Ordinal]
_
_
_ =wf= _ (wf_ord_scope) [in WfOrdinal]
_ [seq _ ] [in NoUniqueNormalFormsWO]
_ @ _ [in NoUniqueNormalFormsWO]
_ [=] _ [in TermEquality]
_ [2 _ ] [in NoUniqueNormalFormsWO]
_ [1 _ ] [in NoUniqueNormalFormsWO]
_ @@ _ [in NoUniqueNormalFormsWO]
_ ! [in ExampleABA]
_ ->> _ [in ExampleABA]
_ @@@ _ [in NoUniqueNormalFormsWO]
_ @ _ [in ExampleABA]
_ @@ _ [in ExampleABA]
_ [>] _ [in ExampleABA]
_ @@@ _ [in ExampleABA]
_ !! [in ExampleABA]
_ [~] _ [in TermEquality]
_ ! [in NoUniqueNormalFormsWO]
_ [>] _ [in NoUniqueNormalFormsWO]
_ ->> _ [in NoUniqueNormalFormsWO]
_ [stp _ ] [in NoUniqueNormalFormsWO]
_ [ _ ] [in NoUniqueNormalFormsWO]
! [in Prelims]
Abbreviation Index
C
context [in NoUniqueNormalFormsWO]context [in ContextEquality]
context [in ExampleABA]
context [in Rewriting]
F
fterm [in Rewriting]fterm [in ExampleABA]
fterm [in Term]
fterm [in Rewriting]
fterm [in NoUniqueNormalFormsWO]
fterm [in Substitution]
fterm [in FiniteTerm]
fterm [in Term]
fterms [in FiniteTerm]
fterms [in Term]
I
id_sub [in NoUniqueNormalFormsWOElaborated]id_sub [in ExampleABA]
N
Nil [in ExampleABA]Nil' [in NoUniqueNormalFormsWO]
P
position [in Term]S
Step [in ExampleABA]Step [in NoUniqueNormalFormsWO]
substitution [in Rewriting]
T
term [in NoUniqueNormalFormsWO]term [in TermEquality]
term [in TermEquality]
term [in Term]
term [in Context]
term [in Rewriting]
term [in ExampleABA]
term [in Substitution]
term [in ContextEquality]
terms [in Context]
terms [in Term]
terms [in ContextEquality]
terms [in TermEquality]
terms [in TermEquality]
terms [in NoUniqueNormalFormsWO]
trs [in NoUniqueNormalFormsWO]
trs [in Rewriting]
trs [in ExampleABA]
Inductive Index
C
context [in Context]context_eq_up_to [in ContextEquality]
context_bis [in ContextEquality]
E
embed [in Rewriting]F
Fin [in Vector]finite_term [in FiniteTerm]
O
ord [in Ordinal]ord_le [in Ordinal]
S
sequence [in Rewriting]step [in Rewriting]
symbol [in ExampleABA]
symbol [in NoUniqueNormalFormsWO]
T
term [in Term]term_bis [in TermEquality]
term_inf [in Term]
term_eq_up_to [in TermEquality]
Definition Index
A
ABA [in ExampleABA]ABA_trs [in ExampleABA]
ABA_r [in ExampleABA]
ABA_l [in ExampleABA]
add [in Ordinal]
all_pos_eq [in TermEquality]
all_terms_eq_up_to [in Rewriting]
append [in Rewriting]
append_rec [in Rewriting]
arity [in ExampleABA]
arity [in NoUniqueNormalFormsWO]
B
beq_var [in ExampleABA]beq_var [in NoUniqueNormalFormsWO]
beq_symb [in ExampleABA]
beq_symb [in NoUniqueNormalFormsWO]
C
cons_term_bis [in Rewriting]context_eq [in ContextEquality]
context_ind2 [in NoUniqueNormalFormsWOElaborated]
context_rect2 [in NoUniqueNormalFormsWOElaborated]
converges [in TermEquality]
critical_pair [in Rewriting]
D
depth [in Rewriting]dig [in Context]
disc_O_S [in Prelims]
disc_S_O [in Prelims]
Dnc [in NoUniqueNormalFormsWO]
Dnt [in NoUniqueNormalFormsWO]
DnUnt [in NoUniqueNormalFormsWO]
DU [in NoUniqueNormalFormsWO]
DU_l [in NoUniqueNormalFormsWO]
DU_r [in NoUniqueNormalFormsWO]
D2nt [in NoUniqueNormalFormsWO]
D2nU2nt [in NoUniqueNormalFormsWO]
E
embed_strict [in Rewriting]empty_substitution [in Substitution]
exp [in Ordinal]
F
F [in ExampleABA]F [in NoUniqueNormalFormsWO]
fill [in Context]
finite [in Rewriting]
finite_subterm [in Term]
finite_term_as_term [in Term]
ftest_BA [in ExampleABA]
ftest_BBA [in ExampleABA]
ftest_A [in ExampleABA]
H
hole_depth [in Context]hole_position [in Context]
I
infinite [in Term]is_var [in Term]
is_cons [in NoUniqueNormalFormsWO]
is_limit [in WfOrdinal]
is_succ [in WfOrdinal]
L
left_linear [in Rewriting]length [in Rewriting]
limit [in WfOrdinal]
linear [in FiniteTerm]
M
mul [in Ordinal]N
nat_as_ord [in Ordinal]nat_as_wf_ord [in WfOrdinal]
nB_Hole [in ExampleABA]
nB_A [in ExampleABA]
normal_form [in Rewriting]
O
oldpsi [in NoUniqueNormalFormsWOElaborated]oldpsi' [in NoUniqueNormalFormsWOElaborated]
omega [in Ordinal]
ord_lt [in Ordinal]
ord_eq [in Ordinal]
orthogonal [in Rewriting]
P
pattern_depth [in FiniteTerm]pd [in Ordinal]
pd_type_as_pred_type [in Rewriting]
pd_type [in Ordinal]
peek [in Term]
position_depth [in Term]
pos_eq [in TermEquality]
pred [in Rewriting]
pred_type [in Rewriting]
pred_type_as_pd_type [in Rewriting]
psi [in NoUniqueNormalFormsWO]
psi' [in NoUniqueNormalFormsWO]
p_Upsi1_UDDUUUpsi2 [in NoUniqueNormalFormsWOElaborated]
p_A_BA [in ExampleABA]
p_psi_Upsi1 [in NoUniqueNormalFormsWOElaborated]
p_DmUSnDSnt_DmUnDnt [in NoUniqueNormalFormsWO]
p_BA_BBA [in ExampleABA]
p_nBA_nBBA [in ExampleABA]
p_UmDSnUSnt_UmDnUnt [in NoUniqueNormalFormsWO]
R
repeat_D [in NoUniqueNormalFormsWO]repeat_DU [in NoUniqueNormalFormsWOElaborated]
repeat_B [in ExampleABA]
repeat_U [in NoUniqueNormalFormsWO]
root [in Term]
S
sequence_rect [in Rewriting]sequence_ind [in Rewriting]
size [in FiniteTerm]
snoc [in Rewriting]
snoc_rec [in Rewriting]
step_eq [in Rewriting]
strongly_convergent [in Rewriting]
substitute [in Substitution]
substitute' [in Substitution]
substitution [in Substitution]
substitution_eq [in Substitution]
subterm [in Term]
sub_psi_Upsi1 [in NoUniqueNormalFormsWOElaborated]
sub_t [in NoUniqueNormalFormsWO]
sub_Upsi1_UDDUUUpsi2 [in NoUniqueNormalFormsWOElaborated]
succ [in WfOrdinal]
s_A_BBA [in ExampleABA]
s_psi_UDDUUUpsi2 [in NoUniqueNormalFormsWOElaborated]
s_psi_repeat_U [in NoUniqueNormalFormsWO]
s_A_BA [in ExampleABA]
s_A_repeat_B [in ExampleABA]
s_DnU2npsin_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
s_DmUnDnt_Dmt [in NoUniqueNormalFormsWO]
s_A_nBA [in ExampleABA]
s_psi_DSnU2SnpsiSn [in NoUniqueNormalFormsWO]
s_psi_Upsi1 [in NoUniqueNormalFormsWOElaborated]
s_UmDnUnt_Umt [in NoUniqueNormalFormsWO]
s_Unpsin_USnpsiSn [in NoUniqueNormalFormsWO]
s_psi_repeat_D [in NoUniqueNormalFormsWO]
s_psi_Unpsin [in NoUniqueNormalFormsWO]
S_eq_inv [in Prelims]
s_A [in ExampleABA]
s_psi_psi [in NoUniqueNormalFormsWOElaborated]
S_eq [in Prelims]
T
term_eq [in TermEquality]test_BA [in ExampleABA]
test_BBA [in ExampleABA]
test_A [in ExampleABA]
trs [in Rewriting]
trs_left_linear [in Rewriting]
U
UD [in NoUniqueNormalFormsWO]UD_l [in NoUniqueNormalFormsWO]
UD_trs [in NoUniqueNormalFormsWO]
UD_r [in NoUniqueNormalFormsWO]
Unc [in NoUniqueNormalFormsWO]
UnDnt [in NoUniqueNormalFormsWO]
unique_normal_forms [in Rewriting]
Unt [in NoUniqueNormalFormsWO]
U2nD2nt [in NoUniqueNormalFormsWO]
U2nt [in NoUniqueNormalFormsWO]
V
vappend [in Vector]variable [in NoUniqueNormalFormsWO]
variable [in ExampleABA]
vars [in FiniteTerm]
varx [in NoUniqueNormalFormsWO]
vcast [in Vector]
vcons [in Vector]
vdrop [in Vector]
vector [in Vector]
vfold [in Vector]
vhead [in Vector]
vmap [in Vector]
vnil [in Vector]
vnth [in Vector]
vtail [in Vector]
vtake [in Vector]
W
weakly_convergent [in Rewriting]weakly_orthogonal [in Rewriting]
wf [in WfOrdinal]
wf [in Rewriting]
wf_ord_as_ord [in WfOrdinal]
wf_ord_eq [in WfOrdinal]
wf_ord_le [in WfOrdinal]
wf_ord_lt [in WfOrdinal]
wf_omega [in WfOrdinal]
wf_ord [in WfOrdinal]
X
X [in NoUniqueNormalFormsWO]X [in ExampleABA]
Z
zero [in WfOrdinal]Variable Index
C
Cast.A [in Vector]ContextEquality.F [in ContextEquality]
ContextEquality.X [in ContextEquality]
Context.F [in Context]
Context.X [in Context]
F
FiniteTerm.F [in FiniteTerm]FiniteTerm.X [in FiniteTerm]
Fold.A [in Vector]
Fold.b [in Vector]
Fold.B [in Vector]
Fold.f [in Vector]
I
InductionPrinciple.H1 [in NoUniqueNormalFormsWOElaborated]InductionPrinciple.H2 [in NoUniqueNormalFormsWOElaborated]
InductionPrinciple.H3 [in NoUniqueNormalFormsWOElaborated]
InductionPrinciple.P [in NoUniqueNormalFormsWOElaborated]
M
Map.A [in Vector]Map.B [in Vector]
Map.f [in Vector]
P
PositionEquality.F [in TermEquality]PositionEquality.X [in TermEquality]
Position.F [in Term]
Position.X [in Term]
R
Rule.F [in Rewriting]Rule.X [in Rewriting]
S
Substitution.F [in Substitution]Substitution.X [in Substitution]
T
TermEquality.F [in TermEquality]TermEquality.X [in TermEquality]
Term.F [in Term]
Term.X [in Term]
TRS.F [in Rewriting]
TRS.InductionPrinciple.H1 [in Rewriting]
TRS.InductionPrinciple.H2 [in Rewriting]
TRS.InductionPrinciple.H3 [in Rewriting]
TRS.InductionPrinciple.P [in Rewriting]
TRS.system [in Rewriting]
TRS.X [in Rewriting]
V
Vector.A [in Vector]Library Index
C
ContextContextEquality
E
ExampleABAF
FiniteTermN
NoUniqueNormalFormsWONoUniqueNormalFormsWOElaborated
O
OrdinalP
PrelimsR
RewritingS
SignatureSubstitution
T
TermTermEquality
V
VariablesVector
W
WfOrdinal| 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 | (645 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 | (10 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 | (3 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 | (258 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 | (16 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 | (39 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 | (38 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 | (40 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 | (16 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 | (171 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 | (38 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 | (16 entries) |
This page has been generated by coqdoc