| 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 | (1863 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 | (80 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 | (255 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 | (51 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 | (798 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 | (67 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 | (33 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 | (28 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 | (152 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 | (137 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 | (29 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 | (222 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 | (11 entries) |
Global Index
A
a [abbreviation, in HOU.second_order.goldfarb.encoding]abg [definition, in HOU.second_order.goldfarb.encoding]
active [definition, in HOU.calculus.normalisation]
Add [constructor, in HOU.second_order.diophantine_equations]
add [definition, in HOU.second_order.dowek.encoding]
addEQ [definition, in HOU.second_order.goldfarb.encoding]
addEQ [definition, in HOU.second_order.dowek.encoding]
add_subst [lemma, in HOU.second_order.dowek.encoding]
add_ren [lemma, in HOU.second_order.dowek.encoding]
advanced [library]
all_terms_app [lemma, in HOU.unification.systemunification]
all_terms_nil [lemma, in HOU.unification.systemunification]
all_terms_cons_iff [lemma, in HOU.unification.systemunification]
all_terms_cons [lemma, in HOU.unification.systemunification]
all_eqs [definition, in HOU.unification.systemunification]
all_terms [definition, in HOU.unification.systemunification]
alpha [definition, in HOU.calculus.prelim]
anti_ren [lemma, in HOU.calculus.semantics]
ap [definition, in HOU.unscoped]
apc [definition, in HOU.unscoped]
app [constructor, in HOU.calculus.terms]
AppL [definition, in HOU.calculus.terms_extension]
ApplicativeHead [section, in HOU.calculus.syntax]
ApplicativeHead.X [variable, in HOU.calculus.syntax]
AppL_largest [lemma, in HOU.calculus.terms_extension]
AppL_ordertyping_inv [lemma, in HOU.calculus.terms_extension]
AppL_typing_inv [lemma, in HOU.calculus.terms_extension]
AppL_ordertyping_repeated [lemma, in HOU.calculus.terms_extension]
AppL_typing_repeated [lemma, in HOU.calculus.terms_extension]
AppL_proper [instance, in HOU.calculus.terms_extension]
AppL_lstep_proper [instance, in HOU.calculus.terms_extension]
AppL_step_proper [instance, in HOU.calculus.terms_extension]
AppL_subst [lemma, in HOU.calculus.terms_extension]
AppL_ren [lemma, in HOU.calculus.terms_extension]
AppL_app [lemma, in HOU.calculus.terms_extension]
AppR [definition, in HOU.calculus.terms_extension]
AppR_ordertyping_inv [lemma, in HOU.calculus.terms_extension]
AppR_typing_inv [lemma, in HOU.calculus.terms_extension]
AppR_ordertyping [lemma, in HOU.calculus.terms_extension]
AppR_typing [lemma, in HOU.calculus.terms_extension]
AppR_Lambda' [lemma, in HOU.calculus.terms_extension]
AppR_Lambda [lemma, in HOU.calculus.terms_extension]
AppR_proper [instance, in HOU.calculus.terms_extension]
AppR_lstep_proper [instance, in HOU.calculus.terms_extension]
AppR_step_proper [instance, in HOU.calculus.terms_extension]
AppR_subst [lemma, in HOU.calculus.terms_extension]
AppR_ren [lemma, in HOU.calculus.terms_extension]
AppR_head [lemma, in HOU.calculus.terms_extension]
AppR_vars [lemma, in HOU.calculus.terms_extension]
AppR_app [lemma, in HOU.calculus.terms_extension]
app_injective_right [lemma, in HOU.std.lists.misc]
app_injective [lemma, in HOU.std.lists.misc]
app_comm [lemma, in HOU.std.lists.basics]
app_proper [instance, in HOU.calculus.semantics]
arity [definition, in HOU.calculus.syntax]
arity_decomposed [lemma, in HOU.calculus.terms_extension]
arity_Arr [lemma, in HOU.calculus.terms_extension]
arr [constructor, in HOU.calculus.terms]
Arr [definition, in HOU.calculus.terms_extension]
Arr_left_injective [lemma, in HOU.calculus.terms_extension]
Arr_inversion [lemma, in HOU.calculus.terms_extension]
Arr_app [lemma, in HOU.calculus.terms_extension]
Atoms [section, in HOU.calculus.syntax]
Atoms.X [variable, in HOU.calculus.syntax]
atom_head_lifting [lemma, in HOU.calculus.syntax]
atom_head [lemma, in HOU.calculus.syntax]
atom_var [lemma, in HOU.calculus.syntax]
atom_lifting [lemma, in HOU.calculus.syntax]
axioms [library]
Aᵤ [projection, in HOU.unification.higher_order_unification]
A₀ [projection, in HOU.unification.nth_order_unification]
B
b [abbreviation, in HOU.second_order.goldfarb.encoding]Backward [section, in HOU.second_order.dowek.reduction]
Backward [section, in HOU.second_order.goldfarb.reduction]
backward [lemma, in HOU.second_order.goldfarb.motivation]
backward_mult [lemma, in HOU.second_order.dowek.reduction]
backward_add [lemma, in HOU.second_order.dowek.reduction]
backward_consts [lemma, in HOU.second_order.dowek.reduction]
backward_vars [lemma, in HOU.second_order.dowek.reduction]
backward_mult [lemma, in HOU.second_order.goldfarb.reduction]
backward_add [lemma, in HOU.second_order.goldfarb.reduction]
backward_consts [lemma, in HOU.second_order.goldfarb.reduction]
backward_vars [lemma, in HOU.second_order.goldfarb.reduction]
backward' [lemma, in HOU.second_order.goldfarb.motivation]
Backward.X [variable, in HOU.second_order.dowek.reduction]
basic [library]
BasicLemmas [section, in HOU.std.lists.basics]
BasicLemmas.WellFoundedStrictInclusion [section, in HOU.std.lists.basics]
BasicLemmas.X [variable, in HOU.std.lists.basics]
BasicLemmas.Y [variable, in HOU.std.lists.basics]
basics [library]
beta [definition, in HOU.calculus.terms]
bound [definition, in HOU.firstorder]
C
C [definition, in HOU.calculus.normalisation]calculus [library]
card [abbreviation, in HOU.third_order.pcp]
cast [definition, in HOU.std.misc]
cfree [definition, in HOU.concon.constants]
charac [definition, in HOU.second_order.goldfarb.motivation]
Choice [section, in HOU.std.enumerable]
ChurchEncoding [section, in HOU.second_order.dowek.encoding]
ChurchEncoding.Substitution [section, in HOU.second_order.dowek.encoding]
church_rosser [lemma, in HOU.std.ars.confluence]
church_commute [lemma, in HOU.second_order.dowek.encoding]
ClosureRelations [section, in HOU.std.ars.basic]
ClosureRelations.X [variable, in HOU.std.ars.basic]
_ === _ [notation, in HOU.std.ars.basic]
_ <<= _ [notation, in HOU.std.ars.basic]
closure_under_reduction [lemma, in HOU.calculus.normalisation]
closure_under_expansion [lemma, in HOU.calculus.normalisation]
compat_app [lemma, in HOU.calculus.normalisation]
compat_lambda [lemma, in HOU.calculus.normalisation]
compat_const [lemma, in HOU.calculus.normalisation]
compat_var [lemma, in HOU.calculus.normalisation]
compComp_exp [lemma, in HOU.calculus.terms]
compComp'_exp [lemma, in HOU.calculus.terms]
compRenRen_exp [definition, in HOU.calculus.terms]
compRenSubst_exp [definition, in HOU.calculus.terms]
compSubstRen__exp [definition, in HOU.calculus.terms]
compSubstSubst_exp [definition, in HOU.calculus.terms]
compute_evaluation_step [lemma, in HOU.calculus.evaluator]
compute_evaluation [lemma, in HOU.std.ars.evaluator]
Con [constructor, in HOU.second_order.diophantine_equations]
concon [library]
Confluence [section, in HOU.calculus.confluence]
Confluence [section, in HOU.std.ars.confluence]
confluence [library]
confluence [library]
confluence_lstep [lemma, in HOU.std.ars.list_reduction]
confluence_step [lemma, in HOU.calculus.confluence]
confluence_unique_normal_forms [lemma, in HOU.std.ars.confluence]
confluence_normal_right [lemma, in HOU.std.ars.confluence]
confluence_normal_left [lemma, in HOU.std.ars.confluence]
Confluence.X [variable, in HOU.std.ars.confluence]
_ ≫ _ [notation, in HOU.calculus.confluence]
_ === _ [notation, in HOU.std.ars.confluence]
_ <<= _ [notation, in HOU.std.ars.confluence]
confluent [definition, in HOU.std.ars.confluence]
confluent_semi [lemma, in HOU.std.ars.confluence]
congr_app [lemma, in HOU.calculus.terms]
congr_lam [lemma, in HOU.calculus.terms]
congr_const [lemma, in HOU.calculus.terms]
congr_arr [lemma, in HOU.calculus.terms]
congr_typevar [lemma, in HOU.calculus.terms]
Conservativity [section, in HOU.concon.conservativity]
conservativity [library]
Conservativity.DowncastLemmas [section, in HOU.concon.conservativity]
Conservativity.DowncastLemmas.Leq [variable, in HOU.concon.conservativity]
Conservativity.DowncastLemmas.n [variable, in HOU.concon.conservativity]
Conservativity.X [variable, in HOU.concon.conservativity]
const [constructor, in HOU.calculus.terms]
Const [record, in HOU.calculus.terms]
Constants [section, in HOU.concon.conservativity]
constants [library]
Constants.ConstantsOfTerm [section, in HOU.concon.conservativity]
Constants.ConstantSubstitution [section, in HOU.concon.conservativity]
constEQ [definition, in HOU.second_order.goldfarb.encoding]
constEQ [definition, in HOU.second_order.dowek.encoding]
Consts [definition, in HOU.concon.conservativity]
consts [definition, in HOU.concon.conservativity]
consts_inhab [lemma, in HOU.concon.conservativity]
consts_in_subst_consts [lemma, in HOU.concon.conservativity]
consts_AppR [lemma, in HOU.concon.conservativity]
consts_AppL [lemma, in HOU.concon.conservativity]
consts_Lam [lemma, in HOU.concon.conservativity]
consts_subst_vars [lemma, in HOU.concon.conservativity]
consts_subset_steps [lemma, in HOU.concon.conservativity]
consts_subset_step [lemma, in HOU.concon.conservativity]
consts_subst_in [lemma, in HOU.concon.conservativity]
consts_ren [lemma, in HOU.concon.conservativity]
Consts_montone [lemma, in HOU.concon.conservativity]
Consts_consts [lemma, in HOU.concon.conservativity]
Const_dis [instance, in HOU.calculus.syntax]
const_dis [projection, in HOU.calculus.terms]
const_type [projection, in HOU.calculus.terms]
const_ordertyping_list [lemma, in HOU.calculus.terms_extension]
countability [library]
counted [inductive, in HOU.std.ars.basic]
countedRefl [constructor, in HOU.std.ars.basic]
countedStep [constructor, in HOU.std.ars.basic]
counted_exp [lemma, in HOU.std.ars.basic]
counted_trans [lemma, in HOU.std.ars.basic]
count_nat [lemma, in HOU.std.enumerable]
count_bool [lemma, in HOU.std.enumerable]
count_enum' [lemma, in HOU.std.enumerable]
ctx [definition, in HOU.calculus.order]
ctx [definition, in HOU.calculus.typing]
ctype [projection, in HOU.calculus.terms]
cumulative [definition, in HOU.std.enumerable]
cum_T [projection, in HOU.std.enumerable]
cum_ge' [lemma, in HOU.std.enumerable]
cum_ge [lemma, in HOU.std.enumerable]
C_longenough [lemma, in HOU.std.enumerable]
C_exhaustive [lemma, in HOU.std.enumerable]
D
dec [projection, in HOU.std.decidable]Dec [record, in HOU.std.decidable]
dec [constructor, in HOU.std.decidable]
Dec [inductive, in HOU.std.decidable]
decb [definition, in HOU.std.decidable]
DecBool [section, in HOU.std.decidable]
decb_dec [lemma, in HOU.std.decidable]
decb1 [definition, in HOU.std.decidable]
decb2 [definition, in HOU.std.decidable]
decidable [library]
decidable_E [instance, in HOU.std.ars.evaluator]
decode_subst_encodes [lemma, in HOU.second_order.goldfarb.reduction]
decode_subst [definition, in HOU.second_order.goldfarb.reduction]
decomp [definition, in HOU.firstorder]
decomp_irrefl [lemma, in HOU.firstorder]
decomp_some_var [lemma, in HOU.firstorder]
decomp_none_not_unifiable [lemma, in HOU.firstorder]
decomp_lambda_free [lemma, in HOU.firstorder]
decomp_typing [lemma, in HOU.firstorder]
decomp_some_head_consts [lemma, in HOU.firstorder]
decomp_none_ind [lemma, in HOU.firstorder]
decomp_some_ind [lemma, in HOU.firstorder]
decomp' [definition, in HOU.firstorder]
decomp'_irrefl [lemma, in HOU.firstorder]
decomp'_some_var [lemma, in HOU.firstorder]
decomp'_none_not_unifiable [lemma, in HOU.firstorder]
decomp'_lambda_free [lemma, in HOU.firstorder]
decomp'_typing [lemma, in HOU.firstorder]
decomp'_none_ind [lemma, in HOU.firstorder]
decomp'_some_ind [lemma, in HOU.firstorder]
decr [definition, in HOU.firstorder]
decr_unifies [lemma, in HOU.firstorder]
decr_typing [lemma, in HOU.firstorder]
decr_lambda_free [lemma, in HOU.firstorder]
dec_varof [instance, in HOU.calculus.syntax]
dec_normal [instance, in HOU.calculus.semantics]
dec_free [instance, in HOU.firstorder]
dec_enc [lemma, in HOU.second_order.goldfarb.encoding]
dec_enc_eq [lemma, in HOU.second_order.goldfarb.encoding]
dec_enc [lemma, in HOU.second_order.dowek.encoding]
dec_all [instance, in HOU.std.decidable]
dec_in [definition, in HOU.std.decidable]
dec_decb [lemma, in HOU.std.decidable]
dec_neg [instance, in HOU.std.decidable]
dec_iff [instance, in HOU.std.decidable]
dec_imp [instance, in HOU.std.decidable]
dec_disj [instance, in HOU.std.decidable]
dec_conj [instance, in HOU.std.decidable]
dec1 [projection, in HOU.std.decidable]
Dec1 [record, in HOU.std.decidable]
dec1 [constructor, in HOU.std.decidable]
Dec1 [inductive, in HOU.std.decidable]
dec1_neg [instance, in HOU.std.decidable]
dec1_iff [instance, in HOU.std.decidable]
dec1_imp [instance, in HOU.std.decidable]
dec1_disj [instance, in HOU.std.decidable]
dec1_conj [instance, in HOU.std.decidable]
dec1_dec [instance, in HOU.std.decidable]
dec2 [projection, in HOU.std.decidable]
Dec2 [record, in HOU.std.decidable]
dec2 [constructor, in HOU.std.decidable]
Dec2 [inductive, in HOU.std.decidable]
dec2_neg [instance, in HOU.std.decidable]
dec2_iff [instance, in HOU.std.decidable]
dec2_imp [instance, in HOU.std.decidable]
dec2_disj [instance, in HOU.std.decidable]
dec2_conj [instance, in HOU.std.decidable]
dec2_dec1' [instance, in HOU.std.decidable]
dec2_dec1 [instance, in HOU.std.decidable]
depdecomp' [lemma, in HOU.firstorder]
deq [inductive, in HOU.second_order.diophantine_equations]
diag [inductive, in HOU.std.countability]
diagB [constructor, in HOU.std.countability]
diagC [constructor, in HOU.std.countability]
diagId [definition, in HOU.std.countability]
diagS [constructor, in HOU.std.countability]
diagStepL [definition, in HOU.std.countability]
diagStepR [definition, in HOU.std.countability]
diagZero [definition, in HOU.std.countability]
diamond [definition, in HOU.std.ars.confluence]
diamond_ext [lemma, in HOU.std.ars.confluence]
diamond_confluent [lemma, in HOU.std.ars.confluence]
diamond_semi_confluent [lemma, in HOU.std.ars.confluence]
diophantine_equations [library]
Dis [record, in HOU.std.decidable]
Dis [inductive, in HOU.std.decidable]
DiscreteTypes [section, in HOU.calculus.syntax]
discrete_list [instance, in HOU.std.decidable]
discrete_prod [instance, in HOU.std.decidable]
discrete_sum [instance, in HOU.std.decidable]
discrete_option [instance, in HOU.std.decidable]
discrete_bool [instance, in HOU.std.decidable]
discrete_nat [instance, in HOU.std.decidable]
discrete_unit [instance, in HOU.std.decidable]
discrete_False [instance, in HOU.std.decidable]
disjoint_F_G [lemma, in HOU.second_order.goldfarb.encoding]
dis_retract [instance, in HOU.std.retracts]
dis_dec [instance, in HOU.std.decidable]
dom [definition, in HOU.calculus.prelim]
dom_lt_iff [lemma, in HOU.calculus.prelim]
dom_nth [lemma, in HOU.calculus.prelim]
dom_in [lemma, in HOU.calculus.prelim]
dom_map [lemma, in HOU.calculus.prelim]
dom_length [lemma, in HOU.calculus.prelim]
Dowek [lemma, in HOU.second_order.dowek.reduction]
downcast_constants [lemma, in HOU.concon.conservativity]
downcast_constants_ordered [lemma, in HOU.concon.conservativity]
downcast_variables [lemma, in HOU.concon.conservativity]
DWK_H10 [lemma, in HOU.second_order.dowek.reduction]
E
E [definition, in HOU.calculus.normalisation]E [definition, in HOU.std.ars.evaluator]
el_T [projection, in HOU.std.enumerable]
Enc [abbreviation, in HOU.third_order.encoding]
Enc [abbreviation, in HOU.third_order.encoding]
enc [definition, in HOU.third_order.encoding]
enc [definition, in HOU.second_order.goldfarb.encoding]
enc [definition, in HOU.second_order.dowek.encoding]
encb [definition, in HOU.third_order.encoding]
encb_eq [lemma, in HOU.third_order.encoding]
encb_subst_id [lemma, in HOU.third_order.encoding]
encb_typing [lemma, in HOU.third_order.encoding]
encodes [definition, in HOU.second_order.goldfarb.encoding]
encodes_characeristic [lemma, in HOU.second_order.goldfarb.encoding]
Encoding [section, in HOU.third_order.encoding]
Encoding [section, in HOU.second_order.goldfarb.encoding]
Encoding [section, in HOU.second_order.dowek.encoding]
encoding [library]
encoding [library]
encoding [library]
Encoding.Injectivity [section, in HOU.third_order.encoding]
Encoding.Reduction [section, in HOU.third_order.encoding]
Encoding.Substitution [section, in HOU.third_order.encoding]
Encoding.Typing [section, in HOU.third_order.encoding]
Encoding.Typing [section, in HOU.second_order.dowek.encoding]
Encoding.Typing.E [variable, in HOU.second_order.dowek.encoding]
Encoding.u [variable, in HOU.third_order.encoding]
Encoding.u_neq_v [variable, in HOU.third_order.encoding]
Encoding.v [variable, in HOU.third_order.encoding]
encs [definition, in HOU.second_order.dowek.reduction]
enc_eq [lemma, in HOU.third_order.encoding]
Enc_subst_id [lemma, in HOU.third_order.encoding]
enc_subst_id [lemma, in HOU.third_order.encoding]
enc_concat [lemma, in HOU.third_order.encoding]
enc_app [lemma, in HOU.third_order.encoding]
enc_cons [lemma, in HOU.third_order.encoding]
enc_nil [lemma, in HOU.third_order.encoding]
Enc_typing [lemma, in HOU.third_order.encoding]
enc_typing [lemma, in HOU.third_order.encoding]
enc_sol_GT [lemma, in HOU.second_order.goldfarb.reduction]
enc_sol_encodes [lemma, in HOU.second_order.goldfarb.reduction]
enc_sol [definition, in HOU.second_order.goldfarb.reduction]
enc_equiv [instance, in HOU.second_order.goldfarb.encoding]
enc_typing [lemma, in HOU.second_order.goldfarb.encoding]
enc_injective [lemma, in HOU.second_order.goldfarb.encoding]
enc_normal [lemma, in HOU.second_order.goldfarb.encoding]
enc_subst [lemma, in HOU.second_order.goldfarb.encoding]
enc_ren [lemma, in HOU.second_order.goldfarb.encoding]
enc_app [lemma, in HOU.second_order.goldfarb.encoding]
enc_succ [lemma, in HOU.second_order.goldfarb.encoding]
enc_zero [lemma, in HOU.second_order.goldfarb.encoding]
enc_characteristic [lemma, in HOU.second_order.dowek.encoding]
enc_equiv_injective [lemma, in HOU.second_order.dowek.encoding]
enc_injective [lemma, in HOU.second_order.dowek.encoding]
enc_mul [lemma, in HOU.second_order.dowek.encoding]
enc_mul' [lemma, in HOU.second_order.dowek.encoding]
enc_add [lemma, in HOU.second_order.dowek.encoding]
enc_add' [lemma, in HOU.second_order.dowek.encoding]
enc_eta [lemma, in HOU.second_order.dowek.encoding]
enc_succ [lemma, in HOU.second_order.dowek.encoding]
enc_zero [lemma, in HOU.second_order.dowek.encoding]
enc_app [lemma, in HOU.second_order.dowek.encoding]
enc_subst [lemma, in HOU.second_order.dowek.encoding]
enc_ren [lemma, in HOU.second_order.dowek.encoding]
enc_inv_motivation [lemma, in HOU.concon.constants]
enc_term_app [lemma, in HOU.concon.constants]
enc_subst_term_reduce [lemma, in HOU.concon.constants]
enc_proper [instance, in HOU.concon.constants]
end_is_var_typed [lemma, in HOU.third_order.encoding]
end_head_var [lemma, in HOU.third_order.encoding]
end_is_var [lemma, in HOU.third_order.huet]
enum [definition, in HOU.std.enumerable]
enumerability [library]
enumerability [library]
enumerable [definition, in HOU.std.enumerable]
enumerable [library]
enumerable_red2 [lemma, in HOU.std.reductions]
enumerable_red [lemma, in HOU.std.reductions]
enumerable_unification [lemma, in HOU.unification.enumerability]
enumerable_orderedsystemunification [lemma, in HOU.concon.enumerability]
enumerable_systemunification [lemma, in HOU.concon.enumerability]
enumerable_orderdunification [lemma, in HOU.concon.enumerability]
enumerable_iff [lemma, in HOU.std.enumerable]
enumerable_conj [lemma, in HOU.std.enumerable]
enumerable_disj [lemma, in HOU.std.enumerable]
enumerable__T_list [lemma, in HOU.std.enumerable]
enumerable_list [instance, in HOU.std.enumerable]
enumerable_list.fixL.LX [variable, in HOU.std.enumerable]
enumerable_list.fixL [section, in HOU.std.enumerable]
enumerable_list.X [variable, in HOU.std.enumerable]
enumerable_list [section, in HOU.std.enumerable]
enumerable__T_option [lemma, in HOU.std.enumerable]
enumerable__T_sum [lemma, in HOU.std.enumerable]
enumerable__T_prod [lemma, in HOU.std.enumerable]
enumerable_enum [lemma, in HOU.std.enumerable]
enumerable_nat_nat [lemma, in HOU.std.enumerable]
enumerable_prod.fixLs.L_Y [variable, in HOU.std.enumerable]
enumerable_prod.fixLs.L_X [variable, in HOU.std.enumerable]
enumerable_prod.fixLs [section, in HOU.std.enumerable]
enumerable_prod.Y [variable, in HOU.std.enumerable]
enumerable_prod.X [variable, in HOU.std.enumerable]
enumerable_prod [section, in HOU.std.enumerable]
enumerable_enum.e [variable, in HOU.std.enumerable]
enumerable_enum.p [variable, in HOU.std.enumerable]
enumerable_enum.X [variable, in HOU.std.enumerable]
enumerable_enum [section, in HOU.std.enumerable]
enumerable_enumerable_T [lemma, in HOU.std.enumerable]
enumerable__T [definition, in HOU.std.enumerable]
enumT [record, in HOU.std.enumerable]
enumT_uni [instance, in HOU.unification.enumerability]
enumT_typing [instance, in HOU.unification.enumerability]
enumT_type [instance, in HOU.unification.enumerability]
enumT_exp [instance, in HOU.unification.enumerability]
enumT_ordsys [instance, in HOU.concon.enumerability]
enumT_sys [instance, in HOU.concon.enumerability]
enumT_orduni [instance, in HOU.concon.enumerability]
enumT_ordertyping [instance, in HOU.concon.enumerability]
enumT_le [instance, in HOU.concon.enumerability]
enumT_sig_le [instance, in HOU.concon.enumerability]
enumT_nat [instance, in HOU.std.enumerable]
enum_red2 [lemma, in HOU.std.reductions]
enum_red2.LX [variable, in HOU.std.reductions]
enum_red2.d [variable, in HOU.std.reductions]
enum_red2.qe [variable, in HOU.std.reductions]
enum_red2.Lq [variable, in HOU.std.reductions]
enum_red2.Hg [variable, in HOU.std.reductions]
enum_red2.g [variable, in HOU.std.reductions]
enum_red2.Hf [variable, in HOU.std.reductions]
enum_red2.f [variable, in HOU.std.reductions]
enum_red2.q [variable, in HOU.std.reductions]
enum_red2.p [variable, in HOU.std.reductions]
enum_red2.Z [variable, in HOU.std.reductions]
enum_red2.Y [variable, in HOU.std.reductions]
enum_red2.X [variable, in HOU.std.reductions]
enum_red2 [section, in HOU.std.reductions]
enum_red [lemma, in HOU.std.reductions]
enum_red.d [variable, in HOU.std.reductions]
enum_red.x0 [variable, in HOU.std.reductions]
enum_red.qe [variable, in HOU.std.reductions]
enum_red.Lq [variable, in HOU.std.reductions]
enum_red.Hf [variable, in HOU.std.reductions]
enum_red.f [variable, in HOU.std.reductions]
enum_red.q [variable, in HOU.std.reductions]
enum_red.p [variable, in HOU.std.reductions]
enum_red.Y [variable, in HOU.std.reductions]
enum_red.X [variable, in HOU.std.reductions]
enum_red [section, in HOU.std.reductions]
enum_unification' [lemma, in HOU.unification.enumerability]
enum_substs [lemma, in HOU.unification.enumerability]
enum_typing [lemma, in HOU.unification.enumerability]
enum_enumT [lemma, in HOU.std.enumerable]
enum_count [lemma, in HOU.std.enumerable]
enum_enumerable [section, in HOU.std.enumerable]
enum_bool [instance, in HOU.std.enumerable]
enum_to_cumulative [lemma, in HOU.std.enumerable]
eq [definition, in HOU.unification.systemunification]
Eqs [abbreviation, in HOU.second_order.goldfarb.encoding]
Eqs [abbreviation, in HOU.second_order.goldfarb.encoding]
eqs [definition, in HOU.second_order.goldfarb.encoding]
Eqs [abbreviation, in HOU.second_order.dowek.encoding]
Eqs [abbreviation, in HOU.second_order.dowek.encoding]
eqs [definition, in HOU.second_order.dowek.encoding]
eqs [definition, in HOU.unification.systemunification]
eqs_ordertyping_strong_ind [definition, in HOU.concon.enumerability]
eqs_typing_strong_ind [definition, in HOU.concon.enumerability]
eqs_size_induction [lemma, in HOU.firstorder]
eqs_ordertyping_preservation_subst [lemma, in HOU.unification.nth_order_unification]
eqs_ordertyping_soundness [lemma, in HOU.unification.nth_order_unification]
eqs_ordertyping_monotone [lemma, in HOU.unification.nth_order_unification]
eqs_ordertyping_step [lemma, in HOU.unification.nth_order_unification]
eqs_ordertyping_cons [constructor, in HOU.unification.nth_order_unification]
eqs_ordertyping_nil [constructor, in HOU.unification.nth_order_unification]
eqs_ordertyping [inductive, in HOU.unification.nth_order_unification]
eqs_typing_preservation_subst [lemma, in HOU.unification.systemunification]
eqs_typing_cons [constructor, in HOU.unification.systemunification]
eqs_typing_nil [constructor, in HOU.unification.systemunification]
eqs_typing [inductive, in HOU.unification.systemunification]
EquationEquivalences [section, in HOU.second_order.dowek.reduction]
EquationEquivalences [section, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition [section, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition [section, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.c [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.EQx [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.EQy [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.EQz [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.Ex [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.Ey [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.Ez [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.m [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.m [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.n [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.n [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.p [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.p [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.x [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.x [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.y [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.y [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.z [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.z [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants [section, in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants [section, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.c [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.c [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.EQx [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.Ex [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.n [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.n [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.x [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.x [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication [section, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication [section, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.c [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.EQx [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.EQy [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.EQz [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.Ex [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.Ey [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.Ez [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.m [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.m [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationBackward [section, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationBackward.EQ1 [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationBackward.EQ2 [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationForward [section, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.n [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.n [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.p [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.p [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.x [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.x [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.y [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.y [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.z [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.z [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.σ1 [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.σ2 [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.τ1 [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.τ2 [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.N [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.N [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.sigma [variable, in HOU.second_order.dowek.reduction]
EquationEquivalences.sigma [variable, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Variables [section, in HOU.second_order.dowek.reduction]
EquationEquivalences.Variables [section, in HOU.second_order.goldfarb.reduction]
EquationEquivalences.X [variable, in HOU.second_order.dowek.reduction]
Equations [section, in HOU.second_order.goldfarb.encoding]
equiv [definition, in HOU.std.ars.basic]
Equivalence [section, in HOU.calculus.equivalence]
equivalence [library]
EquivalenceInversion [section, in HOU.third_order.encoding]
EquivalenceInversion.EQ [variable, in HOU.third_order.encoding]
EquivalenceInversion.H1 [variable, in HOU.third_order.encoding]
EquivalenceInversion.N [variable, in HOU.third_order.encoding]
EquivalenceInversion.S [variable, in HOU.third_order.encoding]
EquivalenceInversion.s [variable, in HOU.third_order.encoding]
EquivalenceInversion.sigma [variable, in HOU.third_order.encoding]
EquivalenceInversion.t [variable, in HOU.third_order.encoding]
EquivalenceInversion.x [variable, in HOU.third_order.encoding]
EquivalenceInversion.X [variable, in HOU.third_order.encoding]
Equivalence.CompatibilityProperties [section, in HOU.calculus.equivalence]
Equivalence.DisjointnessProperties [section, in HOU.calculus.equivalence]
Equivalence.HuetDefinition [section, in HOU.calculus.equivalence]
Equivalence.HuetDefinition.E1 [variable, in HOU.calculus.equivalence]
Equivalence.HuetDefinition.E2 [variable, in HOU.calculus.equivalence]
Equivalence.HuetDefinition.s [variable, in HOU.calculus.equivalence]
Equivalence.HuetDefinition.t [variable, in HOU.calculus.equivalence]
Equivalence.HuetDefinition.v1 [variable, in HOU.calculus.equivalence]
Equivalence.HuetDefinition.v2 [variable, in HOU.calculus.equivalence]
Equivalence.InjectivityProperties [section, in HOU.calculus.equivalence]
_ ≡ _ [notation, in HOU.calculus.equivalence]
equiv_subst_consts [instance, in HOU.concon.conservativity]
equiv_head_equal [lemma, in HOU.calculus.equivalence]
equiv_huet_backward [lemma, in HOU.calculus.equivalence]
equiv_huet_forward [lemma, in HOU.calculus.equivalence]
equiv_neq_const_app [lemma, in HOU.calculus.equivalence]
equiv_neq_const_lam [lemma, in HOU.calculus.equivalence]
equiv_neq_var_const [lemma, in HOU.calculus.equivalence]
equiv_neq_var_lambda [lemma, in HOU.calculus.equivalence]
equiv_neq_lambda_app [lemma, in HOU.calculus.equivalence]
equiv_neq_var_app [lemma, in HOU.calculus.equivalence]
equiv_anti_ren [lemma, in HOU.calculus.equivalence]
equiv_app_elim [lemma, in HOU.calculus.equivalence]
equiv_lam_elim [lemma, in HOU.calculus.equivalence]
equiv_const_eq [lemma, in HOU.calculus.equivalence]
equiv_var_eq [lemma, in HOU.calculus.equivalence]
equiv_app_proper [instance, in HOU.calculus.equivalence]
equiv_lam_proper [instance, in HOU.calculus.equivalence]
equiv_lstep_cons_proper [instance, in HOU.std.ars.list_reduction]
equiv_lstep_cons_inv [lemma, in HOU.std.ars.list_reduction]
equiv_join [lemma, in HOU.std.ars.basic]
equiv_equivalence [instance, in HOU.std.ars.basic]
equiv_reduce [lemma, in HOU.std.ars.basic]
equiv_expand [lemma, in HOU.std.ars.basic]
equiv_rel [instance, in HOU.std.ars.basic]
equiv_star [instance, in HOU.std.ars.basic]
equiv_symm [lemma, in HOU.std.ars.basic]
equiv_trans [lemma, in HOU.std.ars.basic]
equiv_unique_normal_forms [lemma, in HOU.std.ars.confluence]
equiv_AppL_elim [lemma, in HOU.calculus.terms_extension]
equiv_AppR_elim [lemma, in HOU.calculus.terms_extension]
equiv_Lambda_elim [lemma, in HOU.calculus.terms_extension]
equiv_AppR_proper [instance, in HOU.calculus.terms_extension]
equiv_AppL_proper [instance, in HOU.calculus.terms_extension]
equiv_pointwise_eqs [lemma, in HOU.unification.systemunification]
equiv_eqs_pointwise [lemma, in HOU.unification.systemunification]
equi_unifiable_decomp' [lemma, in HOU.firstorder]
equi_unifiable_decomp [lemma, in HOU.firstorder]
equi_unifiable_cons [lemma, in HOU.firstorder]
equi_unifiable_decompose_app [lemma, in HOU.firstorder]
equi_unifiable_comm [lemma, in HOU.firstorder]
equi_unifiable_refl [lemma, in HOU.firstorder]
equi_unifiable_app [instance, in HOU.firstorder]
equi_unifiable_equivalence [instance, in HOU.firstorder]
equi_unifiable [definition, in HOU.firstorder]
eq_equiv [lemma, in HOU.std.ars.basic]
eq_ordertyping [definition, in HOU.unification.nth_order_unification]
eq_typing [definition, in HOU.unification.systemunification]
eq_dec [projection, in HOU.std.decidable]
eq_dec [constructor, in HOU.std.decidable]
eta [definition, in HOU.calculus.evaluator]
eta_typing [lemma, in HOU.calculus.evaluator]
eta_normal [lemma, in HOU.calculus.evaluator]
eta_correct [lemma, in HOU.calculus.evaluator]
eta₀ [definition, in HOU.calculus.evaluator]
eta₀_typing [lemma, in HOU.calculus.evaluator]
eta₀_normal [lemma, in HOU.calculus.evaluator]
eta₀_correct [lemma, in HOU.calculus.evaluator]
evaluates [definition, in HOU.std.ars.basic]
evaluates_E [lemma, in HOU.std.ars.evaluator]
Evaluator [section, in HOU.calculus.evaluator]
Evaluator [section, in HOU.std.ars.evaluator]
evaluator [library]
evaluator [library]
EvaluatorTakahashi [section, in HOU.std.ars.evaluator]
EvaluatorTakahashi.D [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.H1 [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.H2 [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.R [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.refl [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.rho [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.S [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.tf [variable, in HOU.std.ars.evaluator]
EvaluatorTakahashi.X [variable, in HOU.std.ars.evaluator]
Evaluator.Correctness [section, in HOU.calculus.evaluator]
Evaluator.Correctness.A [variable, in HOU.calculus.evaluator]
Evaluator.Correctness.Gamma [variable, in HOU.calculus.evaluator]
Evaluator.Correctness.H [variable, in HOU.calculus.evaluator]
Evaluator.Correctness.H₀ [variable, in HOU.calculus.evaluator]
Evaluator.Correctness.n [variable, in HOU.calculus.evaluator]
Evaluator.Correctness.s [variable, in HOU.calculus.evaluator]
Evaluator.delta [variable, in HOU.std.ars.evaluator]
Evaluator.R [variable, in HOU.std.ars.evaluator]
Evaluator.red [variable, in HOU.std.ars.evaluator]
Evaluator.rho [variable, in HOU.std.ars.evaluator]
Evaluator.X [variable, in HOU.std.ars.evaluator]
eval_subrel [instance, in HOU.std.ars.basic]
exp [inductive, in HOU.calculus.terms]
exp_dis [instance, in HOU.calculus.syntax]
extRen_exp [definition, in HOU.calculus.terms]
ext_exp [definition, in HOU.calculus.terms]
E_var [lemma, in HOU.calculus.normalisation]
E_evaluates [lemma, in HOU.calculus.normalisation]
E_correct_tak [lemma, in HOU.std.ars.evaluator]
E_evaluates [lemma, in HOU.std.ars.evaluator]
E_monotone [lemma, in HOU.std.ars.evaluator]
E_step [lemma, in HOU.std.ars.evaluator]
E_stops [lemma, in HOU.std.ars.evaluator]
E_unique [lemma, in HOU.std.ars.evaluator]
E_correct [lemma, in HOU.std.ars.evaluator]
E_it [lemma, in HOU.std.ars.evaluator]
E_S [lemma, in HOU.std.ars.evaluator]
Eᵤ' [projection, in HOU.unification.systemunification]
E₀' [projection, in HOU.unification.nth_order_unification]
F
F [definition, in HOU.second_order.goldfarb.encoding]filter_seqteq_proper [instance, in HOU.std.lists.basics]
filter_incl_proper [instance, in HOU.std.lists.basics]
filter_length [lemma, in HOU.std.lists.basics]
fin [definition, in HOU.unscoped]
find [definition, in HOU.std.lists.advanced]
Find [section, in HOU.std.lists.advanced]
find_map_inv [lemma, in HOU.std.lists.advanced]
find_map [lemma, in HOU.std.lists.advanced]
find_not_in [lemma, in HOU.std.lists.advanced]
find_Some_nth [lemma, in HOU.std.lists.advanced]
find_in [lemma, in HOU.std.lists.advanced]
find_Some [lemma, in HOU.std.lists.advanced]
finst [definition, in HOU.third_order.encoding]
finst_equivalence [lemma, in HOU.third_order.encoding]
finst_typing [lemma, in HOU.third_order.encoding]
firstorder [library]
FirstOrderDecidable [section, in HOU.firstorder]
FirstOrderDecidable.free [variable, in HOU.firstorder]
FirstOrderDecidable.X [variable, in HOU.firstorder]
firstorder_decidable [lemma, in HOU.firstorder]
firstorder_decidable' [lemma, in HOU.firstorder]
FlatMap [section, in HOU.std.lists.advanced]
FlatMap.X [variable, in HOU.std.lists.advanced]
FlatMap.Y [variable, in HOU.std.lists.advanced]
flat_map_in_incl [lemma, in HOU.std.lists.advanced]
flat_map_incl [lemma, in HOU.std.lists.advanced]
flat_map_app [lemma, in HOU.std.lists.advanced]
Forward [section, in HOU.second_order.dowek.reduction]
Forward [section, in HOU.second_order.goldfarb.reduction]
forward [lemma, in HOU.second_order.goldfarb.motivation]
forward_typing [lemma, in HOU.second_order.dowek.reduction]
forward_mult [lemma, in HOU.second_order.dowek.reduction]
forward_add [lemma, in HOU.second_order.dowek.reduction]
forward_consts [lemma, in HOU.second_order.dowek.reduction]
forward_vars [lemma, in HOU.second_order.dowek.reduction]
forward_mul2 [lemma, in HOU.second_order.goldfarb.reduction]
forward_mul1 [lemma, in HOU.second_order.goldfarb.reduction]
forward_add [lemma, in HOU.second_order.goldfarb.reduction]
forward_consts [lemma, in HOU.second_order.goldfarb.reduction]
forward_vars [lemma, in HOU.second_order.goldfarb.reduction]
Forward.E [variable, in HOU.second_order.dowek.reduction]
Forward.E [variable, in HOU.second_order.goldfarb.reduction]
Forward.X [variable, in HOU.second_order.dowek.reduction]
FO_subst_equiv_eq [lemma, in HOU.firstorder]
FreeVariables [section, in HOU.calculus.syntax]
free' [definition, in HOU.firstorder]
Fs [definition, in HOU.second_order.goldfarb.encoding]
Fs_in [lemma, in HOU.second_order.goldfarb.encoding]
func [definition, in HOU.second_order.goldfarb.reduction]
funcomp [definition, in HOU.std.misc]
functional [definition, in HOU.std.ars.basic]
func_typing [lemma, in HOU.second_order.goldfarb.reduction]
F_not_in_G [lemma, in HOU.second_order.goldfarb.encoding]
F_injective [lemma, in HOU.second_order.goldfarb.encoding]
G
G [definition, in HOU.calculus.normalisation]G [definition, in HOU.second_order.goldfarb.encoding]
g [abbreviation, in HOU.second_order.goldfarb.encoding]
Gamma__deq_content [lemma, in HOU.second_order.goldfarb.encoding]
Gamma__deq_nth_G [lemma, in HOU.second_order.goldfarb.encoding]
Gamma__deq_nth_F [lemma, in HOU.second_order.goldfarb.encoding]
Gamma__deq [definition, in HOU.second_order.goldfarb.encoding]
Gamma__dwk_nth [lemma, in HOU.second_order.dowek.encoding]
Gamma__dwk [definition, in HOU.second_order.dowek.encoding]
Gammaᵤ [projection, in HOU.unification.higher_order_unification]
Gammaᵤ' [projection, in HOU.unification.systemunification]
Gamma₀ [projection, in HOU.unification.nth_order_unification]
Gamma₀' [projection, in HOU.unification.nth_order_unification]
ge_dec [instance, in HOU.std.decidable]
ginst [definition, in HOU.third_order.huet]
ginst_equivalence [lemma, in HOU.third_order.huet]
ginst_typing [lemma, in HOU.third_order.huet]
Goldfarb [lemma, in HOU.second_order.goldfarb.reduction]
Goldfarb_Huet [lemma, in HOU.concon.constants]
Goldfarb_sharp [lemma, in HOU.concon.constants]
Goldfarb_remove [lemma, in HOU.concon.constants]
Goldfarb' [lemma, in HOU.second_order.goldfarb.reduction]
gonly [definition, in HOU.concon.constants]
Gs [definition, in HOU.second_order.goldfarb.encoding]
Gs_in [lemma, in HOU.second_order.goldfarb.encoding]
GT [definition, in HOU.second_order.goldfarb.reduction]
GT_typing [lemma, in HOU.second_order.goldfarb.reduction]
GT_equiv [lemma, in HOU.second_order.goldfarb.reduction]
gt_dec [instance, in HOU.std.decidable]
G_up [lemma, in HOU.calculus.normalisation]
G_cons [lemma, in HOU.calculus.normalisation]
G_id [lemma, in HOU.calculus.normalisation]
G_not_in_F [lemma, in HOU.second_order.goldfarb.encoding]
G_injective [lemma, in HOU.second_order.goldfarb.encoding]
H
hd [abbreviation, in HOU.third_order.pcp]head [definition, in HOU.calculus.syntax]
heads [abbreviation, in HOU.third_order.pcp]
head_subst [lemma, in HOU.calculus.syntax]
head_preserved [lemma, in HOU.calculus.semantics]
head_atom [lemma, in HOU.calculus.semantics]
head_decompose [lemma, in HOU.calculus.terms_extension]
higher_order_unification [library]
huet [library]
HuetReduction [section, in HOU.third_order.huet]
HuetReduction.BackwardDirection [section, in HOU.third_order.huet]
HuetReduction.BackwardDirection.EQ [variable, in HOU.third_order.huet]
HuetReduction.BackwardDirection.H1 [variable, in HOU.third_order.huet]
HuetReduction.BackwardDirection.N [variable, in HOU.third_order.huet]
HuetReduction.BackwardDirection.S [variable, in HOU.third_order.huet]
HuetReduction.BackwardDirection.s [variable, in HOU.third_order.huet]
HuetReduction.BackwardDirection.sigma [variable, in HOU.third_order.huet]
HuetReduction.BackwardDirection.t [variable, in HOU.third_order.huet]
HuetReduction.BackwardDirection.x [variable, in HOU.third_order.huet]
HuetReduction.f [variable, in HOU.third_order.huet]
HuetReduction.ForwardDirection [section, in HOU.third_order.huet]
HuetReduction.g [variable, in HOU.third_order.huet]
HuetReduction.h [variable, in HOU.third_order.huet]
HuetReduction.u [variable, in HOU.third_order.huet]
HuetReduction.v [variable, in HOU.third_order.huet]
HuetReduction.X [variable, in HOU.third_order.huet]
H10 [definition, in HOU.second_order.diophantine_equations]
H10_DWK [lemma, in HOU.second_order.dowek.reduction]
H10_SU [lemma, in HOU.second_order.goldfarb.reduction]
H10_to_SOU [instance, in HOU.second_order.goldfarb.encoding]
H10_to_DWK [instance, in HOU.second_order.dowek.encoding]
H1ᵤ [projection, in HOU.unification.higher_order_unification]
H1₀ [projection, in HOU.unification.nth_order_unification]
H2ᵤ [projection, in HOU.unification.higher_order_unification]
H2₀ [projection, in HOU.unification.nth_order_unification]
Hᵤ' [projection, in HOU.unification.systemunification]
H₀' [projection, in HOU.unification.nth_order_unification]
I
I [projection, in HOU.std.retracts]iConsts [definition, in HOU.concon.constants]
id [definition, in HOU.unscoped]
idSubst_exp [definition, in HOU.calculus.terms]
iff_dec [lemma, in HOU.std.decidable]
incl_select_iff [lemma, in HOU.third_order.pcp]
incl_strict_incl [lemma, in HOU.std.lists.basics]
incl_cons_proper [instance, in HOU.std.lists.basics]
incl_app_build [lemma, in HOU.std.lists.basics]
incl_app_project_right [lemma, in HOU.std.lists.basics]
incl_app_project_left [lemma, in HOU.std.lists.basics]
incl_distr_right [lemma, in HOU.std.lists.basics]
incl_distr_left [lemma, in HOU.std.lists.basics]
incl_filter [lemma, in HOU.std.lists.basics]
incl_cons_drop [lemma, in HOU.std.lists.basics]
incl_cons_project_r [lemma, in HOU.std.lists.basics]
incl_cons_project_l [lemma, in HOU.std.lists.basics]
incl_cons_build [lemma, in HOU.std.lists.basics]
incl_cons [lemma, in HOU.std.lists.basics]
incl_nil [lemma, in HOU.std.lists.basics]
incl_seteq [lemma, in HOU.std.lists.basics]
incl_app [lemma, in HOU.std.lists.basics]
incl_seteq_proper [instance, in HOU.std.lists.basics]
incl_preorder [instance, in HOU.std.lists.basics]
incl_strict_incl_trans [lemma, in HOU.std.lists.basics]
incl_trans [lemma, in HOU.std.lists.basics]
incl_refl [lemma, in HOU.std.lists.basics]
incl_select [lemma, in HOU.std.lists.advanced]
incl_nats [lemma, in HOU.std.lists.advanced]
inhab [definition, in HOU.concon.conservativity]
InhabitingTypes [section, in HOU.concon.conservativity]
InhabitingTypes.X [variable, in HOU.concon.conservativity]
inhab_typing' [lemma, in HOU.concon.conservativity]
inhab_app [lemma, in HOU.concon.conservativity]
inhab_typing_inv [lemma, in HOU.concon.conservativity]
inhab_typing [lemma, in HOU.concon.conservativity]
inhab_ren [lemma, in HOU.concon.conservativity]
injective_upRen_exp_exp [lemma, in HOU.calculus.semantics]
injective_I__P [lemma, in HOU.std.countability]
injective_I__S [lemma, in HOU.std.countability]
inj_typing [lemma, in HOU.concon.constants]
inj_ren [lemma, in HOU.concon.constants]
instId_exp [lemma, in HOU.calculus.terms]
inv_proper [instance, in HOU.concon.constants]
inv_subst_typing [lemma, in HOU.concon.constants]
inv_term_typing [lemma, in HOU.concon.constants]
in_seteq_proper [instance, in HOU.std.lists.basics]
in_ind [lemma, in HOU.std.lists.basics]
in_Equations [lemma, in HOU.second_order.goldfarb.encoding]
in_Gs [lemma, in HOU.second_order.goldfarb.encoding]
in_Fs [lemma, in HOU.second_order.goldfarb.encoding]
in_Equations [lemma, in HOU.second_order.dowek.encoding]
in_concat_iff [lemma, in HOU.std.enumerable]
In_dec [instance, in HOU.std.decidable]
isApp [definition, in HOU.calculus.syntax]
isAtom [definition, in HOU.calculus.syntax]
isLam [definition, in HOU.calculus.syntax]
isVar [definition, in HOU.calculus.syntax]
it [definition, in HOU.std.misc]
ith [definition, in HOU.second_order.goldfarb.motivation]
it_up_var_sapp [lemma, in HOU.calculus.prelim]
it_up_ge [lemma, in HOU.calculus.prelim]
it_up_lt [lemma, in HOU.calculus.prelim]
it_up_spec [lemma, in HOU.calculus.prelim]
it_up_ren_ge [lemma, in HOU.calculus.prelim]
it_up_ren_lt [lemma, in HOU.calculus.prelim]
it_up_ren_spec [lemma, in HOU.calculus.prelim]
it_commute [lemma, in HOU.std.misc]
it_plus [lemma, in HOU.std.misc]
it_up_free' [lemma, in HOU.firstorder]
I__S_R__S [lemma, in HOU.std.countability]
I__S [definition, in HOU.std.countability]
I__P_R__P [lemma, in HOU.std.countability]
I__P [definition, in HOU.std.countability]
J
joinable [definition, in HOU.std.ars.confluence]joinable_ext [lemma, in HOU.std.ars.confluence]
L
L [definition, in HOU.std.reductions]Lalt [definition, in HOU.std.reductions]
lam [constructor, in HOU.calculus.terms]
Lambda [definition, in HOU.calculus.terms_extension]
LambdaFreeness [section, in HOU.firstorder]
lambda_free_normal [lemma, in HOU.firstorder]
lambda_free_subst_eqs [lemma, in HOU.firstorder]
lambda_free_substitution [lemma, in HOU.firstorder]
lambda_free_not_lam [lemma, in HOU.firstorder]
lambda_free_subst [lemma, in HOU.firstorder]
lambda_free_AppR [lemma, in HOU.firstorder]
lambda_free_app [constructor, in HOU.firstorder]
lambda_free_const [constructor, in HOU.firstorder]
lambda_free_var [constructor, in HOU.firstorder]
lambda_free [inductive, in HOU.firstorder]
Lambda_ordertyping_inv [lemma, in HOU.calculus.terms_extension]
Lambda_typing_inv [lemma, in HOU.calculus.terms_extension]
Lambda_ordertyping [lemma, in HOU.calculus.terms_extension]
Lambda_typing [lemma, in HOU.calculus.terms_extension]
Lambda_equiv_proper [instance, in HOU.calculus.terms_extension]
Lambda_steps_proper [instance, in HOU.calculus.terms_extension]
Lambda_step_proper [instance, in HOU.calculus.terms_extension]
Lambda_subst [lemma, in HOU.calculus.terms_extension]
Lambda_ren [lemma, in HOU.calculus.terms_extension]
Lambda_injective [lemma, in HOU.calculus.terms_extension]
Lambda_plus [lemma, in HOU.calculus.terms_extension]
lam_proper [instance, in HOU.calculus.semantics]
largest_lin [lemma, in HOU.second_order.goldfarb.encoding]
left_ordertyping [lemma, in HOU.unification.nth_order_unification]
left_subst_eqs [lemma, in HOU.unification.systemunification]
left_typing [lemma, in HOU.unification.systemunification]
left_side [definition, in HOU.unification.systemunification]
length_nats [lemma, in HOU.std.lists.advanced]
le_strong_ind [definition, in HOU.concon.enumerability]
le_dec [instance, in HOU.std.decidable]
lin [definition, in HOU.second_order.goldfarb.encoding]
Linearization [section, in HOU.second_order.goldfarb.encoding]
linearize_consts [lemma, in HOU.concon.conservativity]
linearize_terms_ordertyping [lemma, in HOU.unification.nth_order_unification]
linearize_vars [lemma, in HOU.unification.systemunification]
linearize_terms_typing [lemma, in HOU.unification.systemunification]
linearize_terms_equiv [lemma, in HOU.unification.systemunification]
linearize_terms_subst [lemma, in HOU.unification.systemunification]
linearize_terms [definition, in HOU.unification.systemunification]
lin_injective [lemma, in HOU.second_order.goldfarb.encoding]
lin_subst [lemma, in HOU.second_order.goldfarb.encoding]
lin_ren [lemma, in HOU.second_order.goldfarb.encoding]
lin_typing [lemma, in HOU.second_order.goldfarb.encoding]
lin_app [lemma, in HOU.second_order.goldfarb.encoding]
lin_cons [lemma, in HOU.second_order.goldfarb.encoding]
lin_nil [lemma, in HOU.second_order.goldfarb.encoding]
ListEnumerability [section, in HOU.unification.enumerability]
ListEnumerabilityOrdered [section, in HOU.concon.enumerability]
ListEnumerabilityOrderedSystems [section, in HOU.concon.enumerability]
ListEnumerabilityOrderedSystems.enumX [variable, in HOU.concon.enumerability]
ListEnumerabilityOrderedSystems.X [variable, in HOU.concon.enumerability]
ListEnumerabilityOrdered.enumX [variable, in HOU.concon.enumerability]
ListEnumerabilityOrdered.X [variable, in HOU.concon.enumerability]
ListEnumerabilitySystems [section, in HOU.concon.enumerability]
ListEnumerabilitySystems.enumX [variable, in HOU.concon.enumerability]
ListEnumerabilitySystems.X [variable, in HOU.concon.enumerability]
ListEnumerability.enumX [variable, in HOU.unification.enumerability]
ListEnumerability.X [variable, in HOU.unification.enumerability]
ListRelations [section, in HOU.std.ars.list_reduction]
ListRelations.R [variable, in HOU.std.ars.list_reduction]
ListRelations.X [variable, in HOU.std.ars.list_reduction]
listtyping [inductive, in HOU.calculus.terms_extension]
listtyping_preservation_under_renaming [lemma, in HOU.calculus.terms_extension]
listtyping_app [lemma, in HOU.calculus.terms_extension]
listtyping_cons [constructor, in HOU.calculus.terms_extension]
listtyping_nil [constructor, in HOU.calculus.terms_extension]
list_equiv_ind [lemma, in HOU.std.ars.list_reduction]
list_end_ind [lemma, in HOU.std.lists.misc]
list_pointwise_eq [lemma, in HOU.std.lists.misc]
list_decompose_strong [lemma, in HOU.std.lists.misc]
list_decompose_end [lemma, in HOU.std.lists.misc]
list_decompose_alt [lemma, in HOU.std.lists.misc]
list_decompose [lemma, in HOU.std.lists.misc]
list_subst_proper [instance, in HOU.calculus.terms_extension]
list_ren_proper [instance, in HOU.calculus.terms_extension]
list_equiv_anti_ren [lemma, in HOU.calculus.terms_extension]
list_equiv_subst [lemma, in HOU.calculus.terms_extension]
list_equiv_ren [lemma, in HOU.calculus.terms_extension]
list_reduction [library]
lstep [inductive, in HOU.std.ars.list_reduction]
lsteps_cons [instance, in HOU.std.ars.list_reduction]
lsteps_cons_inv [lemma, in HOU.std.ars.list_reduction]
lsteps_nil_cons [lemma, in HOU.std.ars.list_reduction]
lsteps_cons_nil [lemma, in HOU.std.ars.list_reduction]
lstep_normal_nil [lemma, in HOU.std.ars.list_reduction]
lstep_normal_cons [lemma, in HOU.std.ars.list_reduction]
lstep_normal_cons_r [lemma, in HOU.std.ars.list_reduction]
lstep_normal_cons_l [lemma, in HOU.std.ars.list_reduction]
lstep_nil_cons [lemma, in HOU.std.ars.list_reduction]
lstep_cons_nil [lemma, in HOU.std.ars.list_reduction]
lt_le_subrel [instance, in HOU.std.misc]
lt_nats [lemma, in HOU.std.lists.advanced]
lt_dec [instance, in HOU.std.decidable]
L_Uextended [definition, in HOU.unification.enumerability]
L_subst [definition, in HOU.unification.enumerability]
L_uni [definition, in HOU.unification.enumerability]
L_typing [definition, in HOU.unification.enumerability]
L_typingT [definition, in HOU.unification.enumerability]
L_type [definition, in HOU.unification.enumerability]
L_exp [definition, in HOU.unification.enumerability]
L_ordsys [definition, in HOU.concon.enumerability]
L_sys [definition, in HOU.concon.enumerability]
L_orduni [definition, in HOU.concon.enumerability]
L_ordertypingT [definition, in HOU.concon.enumerability]
L_le [definition, in HOU.concon.enumerability]
L_T [projection, in HOU.std.enumerable]
Lᵤ' [projection, in HOU.unification.systemunification]
L₀' [projection, in HOU.unification.nth_order_unification]
M
map_seteq_proper [instance, in HOU.std.lists.basics]map_incl_proper [instance, in HOU.std.lists.basics]
map_nil [lemma, in HOU.std.lists.basics]
map_id [lemma, in HOU.std.lists.basics]
map_id_list [lemma, in HOU.std.lists.basics]
map_var_typing [lemma, in HOU.calculus.terms_extension]
max_le_right [lemma, in HOU.calculus.prelim]
max_le_left [lemma, in HOU.calculus.prelim]
max_proper [instance, in HOU.std.misc]
misc [library]
misc [library]
morphism [definition, in HOU.std.ars.normalisation]
Motivation [section, in HOU.second_order.goldfarb.motivation]
motivation [library]
Motivation.a [variable, in HOU.second_order.goldfarb.motivation]
Motivation.b [variable, in HOU.second_order.goldfarb.motivation]
Motivation.FiniteSequences [section, in HOU.second_order.goldfarb.motivation]
Motivation.m [variable, in HOU.second_order.goldfarb.motivation]
Motivation.n [variable, in HOU.second_order.goldfarb.motivation]
Motivation.p [variable, in HOU.second_order.goldfarb.motivation]
Motivation.Streams [section, in HOU.second_order.goldfarb.motivation]
Motivation.Streams.X [variable, in HOU.second_order.goldfarb.motivation]
_ ≈ _ ⟶ _ [notation, in HOU.second_order.goldfarb.motivation]
MPCP [definition, in HOU.third_order.pcp]
MPCPsimp [definition, in HOU.third_order.pcp]
MPCPsimp_MPCP [lemma, in HOU.third_order.pcp]
MPCP_U [lemma, in HOU.concon.conservativity]
MPCP_U3 [lemma, in HOU.third_order.simplified]
MPCP_U3.X [variable, in HOU.third_order.simplified]
MPCP_U3 [section, in HOU.third_order.simplified]
MPCP_MPCP' [lemma, in HOU.third_order.simplified]
MPCP' [definition, in HOU.third_order.simplified]
MPCP'_U3 [lemma, in HOU.third_order.simplified]
MPCP'_to_U [instance, in HOU.third_order.simplified]
Mul [constructor, in HOU.second_order.diophantine_equations]
mul [definition, in HOU.second_order.dowek.encoding]
mulEQ [definition, in HOU.second_order.dowek.encoding]
mulEQ₁ [definition, in HOU.second_order.goldfarb.encoding]
mulEQ₂ [definition, in HOU.second_order.goldfarb.encoding]
multiple [inductive, in HOU.std.ars.basic]
multipleSingle [constructor, in HOU.std.ars.basic]
multipleStep [constructor, in HOU.std.ars.basic]
multiple_fixpoint [lemma, in HOU.std.ars.basic]
multiple_idem [lemma, in HOU.std.ars.basic]
multiple_mono [instance, in HOU.std.ars.basic]
multiple_star_step [lemma, in HOU.std.ars.basic]
multiple_destruct [lemma, in HOU.std.ars.basic]
multiple_star [instance, in HOU.std.ars.basic]
multiple_exp [instance, in HOU.std.ars.basic]
multiple_transitive [instance, in HOU.std.ars.basic]
multiple_trans [lemma, in HOU.std.ars.basic]
multiplication_lambdas [lemma, in HOU.second_order.goldfarb.reduction]
mul_subst [lemma, in HOU.second_order.dowek.encoding]
mul_ren [lemma, in HOU.second_order.dowek.encoding]
MU_PCP [lemma, in HOU.third_order.huet]
mu_enum [definition, in HOU.std.enumerable]
N
nats [definition, in HOU.std.lists.advanced]Nats [section, in HOU.std.lists.advanced]
nats_incl [lemma, in HOU.std.lists.advanced]
nats_lt [lemma, in HOU.std.lists.advanced]
Neg [definition, in HOU.std.reductions]
nf [inductive, in HOU.calculus.terms_extension]
nfc [constructor, in HOU.calculus.terms_extension]
nodup_seteq [lemma, in HOU.std.lists.basics]
Normal [definition, in HOU.std.ars.basic]
normal [abbreviation, in HOU.calculus.semantics]
normal [abbreviation, in HOU.calculus.semantics]
Normalisation [section, in HOU.unification.higher_order_unification]
Normalisation [section, in HOU.unification.nth_order_unification]
normalisation [library]
normalisation [library]
Normalisation.X [variable, in HOU.unification.higher_order_unification]
Normalisation.X [variable, in HOU.unification.nth_order_unification]
normalise_subst [lemma, in HOU.unification.higher_order_unification]
normal_inhab [lemma, in HOU.concon.conservativity]
normal_in_lstep [lemma, in HOU.std.ars.list_reduction]
normal_lstep_in [lemma, in HOU.std.ars.list_reduction]
Normal_star_stops [lemma, in HOU.std.ars.basic]
normal_subst [lemma, in HOU.calculus.semantics]
normal_ren [lemma, in HOU.calculus.semantics]
normal_app_intro [lemma, in HOU.calculus.semantics]
normal_app_not_lam [lemma, in HOU.calculus.semantics]
normal_app_r [lemma, in HOU.calculus.semantics]
normal_app_l [lemma, in HOU.calculus.semantics]
normal_lam_elim [lemma, in HOU.calculus.semantics]
normal_lam_intro [lemma, in HOU.calculus.semantics]
normal_const [lemma, in HOU.calculus.semantics]
normal_var [lemma, in HOU.calculus.semantics]
normal_forms_encodes [lemma, in HOU.second_order.goldfarb.encoding]
normal_enc [lemma, in HOU.second_order.dowek.encoding]
normal_retyping [lemma, in HOU.concon.retyping]
Normal_star_stops [lemma, in HOU.std.ars.normalisation]
Normal_SN [lemma, in HOU.std.ars.normalisation]
normal_nf [lemma, in HOU.calculus.terms_extension]
normal_AppR_left [lemma, in HOU.calculus.terms_extension]
normal_AppR_right [lemma, in HOU.calculus.terms_extension]
normal_AppL_right [lemma, in HOU.calculus.terms_extension]
normal_AppL_left [lemma, in HOU.calculus.terms_extension]
normal_Lambda [lemma, in HOU.calculus.terms_extension]
not_equiv_lstep_nil_cons [lemma, in HOU.std.ars.list_reduction]
NOU [definition, in HOU.unification.nth_order_unification]
NSOU [definition, in HOU.unification.nth_order_unification]
Nth [section, in HOU.std.lists.advanced]
nth [abbreviation, in HOU.std.lists.advanced]
NthOrderSystemUnification [section, in HOU.unification.nth_order_unification]
NthOrderSystemUnification.X [variable, in HOU.unification.nth_order_unification]
_ ⊢₊₊( _ ) _ : _ [notation, in HOU.unification.nth_order_unification]
_ ⊢₂( _ ) _ : _ [notation, in HOU.unification.nth_order_unification]
NthOrderUnificationDefinition [section, in HOU.unification.nth_order_unification]
nth_error_sapp [lemma, in HOU.calculus.prelim]
nth_Gamma__deq_G [lemma, in HOU.second_order.goldfarb.encoding]
nth_Gamma__deq_F [lemma, in HOU.second_order.goldfarb.encoding]
nth_error_repeated [lemma, in HOU.std.lists.advanced]
nth_nats [lemma, in HOU.std.lists.advanced]
nth_error_Some_lt [lemma, in HOU.std.lists.advanced]
nth_error_lt_Some [lemma, in HOU.std.lists.advanced]
nth_error_map_option [lemma, in HOU.std.lists.advanced]
nth_order_unification [library]
Nth.X [variable, in HOU.std.lists.advanced]
Nth.Y [variable, in HOU.std.lists.advanced]
NU [definition, in HOU.unification.higher_order_unification]
O
ofNat [definition, in HOU.std.enumerable]ord [definition, in HOU.calculus.order]
order [library]
orderlisttyping [inductive, in HOU.calculus.terms_extension]
orderlisttyping_element [lemma, in HOU.calculus.terms_extension]
orderlisttyping_preservation_under_substitution [lemma, in HOU.calculus.terms_extension]
orderlisttyping_preservation_under_renaming [lemma, in HOU.calculus.terms_extension]
orderlisttyping_app [lemma, in HOU.calculus.terms_extension]
orderlisttyping_cons [constructor, in HOU.calculus.terms_extension]
orderlisttyping_nil [constructor, in HOU.calculus.terms_extension]
ordertyping [inductive, in HOU.calculus.order]
OrderTyping [section, in HOU.calculus.order]
ordertypingApp [constructor, in HOU.calculus.order]
ordertypingConst [constructor, in HOU.calculus.order]
ordertypingLam [constructor, in HOU.calculus.order]
ordertypingSubst [definition, in HOU.calculus.order]
ordertypingSubst_complete [lemma, in HOU.calculus.order]
ordertypingSubst_soundness [lemma, in HOU.calculus.order]
ordertypingSubst_monotone [lemma, in HOU.calculus.order]
ordertypingVar [constructor, in HOU.calculus.order]
ordertyping_weak_ordertyping [lemma, in HOU.concon.conservativity]
ordertyping_from_basetyping [lemma, in HOU.concon.conservativity]
ordertyping_preservation_consts [lemma, in HOU.concon.conservativity]
ordertyping_preservation_under_steps [lemma, in HOU.calculus.order]
ordertyping_preservation_under_reduction [lemma, in HOU.calculus.order]
ordertyping_preservation_under_substitution [lemma, in HOU.calculus.order]
ordertyping_weak_preservation_under_substitution [lemma, in HOU.calculus.order]
ordertyping_preservation_under_renaming [lemma, in HOU.calculus.order]
ordertyping_weak_preservation_under_renaming [lemma, in HOU.calculus.order]
ordertyping_completeness [lemma, in HOU.calculus.order]
ordertyping_soundness [lemma, in HOU.calculus.order]
ordertyping_monotone [lemma, in HOU.calculus.order]
ordertyping_step [lemma, in HOU.calculus.order]
ordertyping_termination_steps [lemma, in HOU.calculus.normalisation]
ordertyping_strong_ind [definition, in HOU.concon.enumerability]
ordertyping_one_atom [lemma, in HOU.firstorder]
ordertyping_normalise_subst [lemma, in HOU.unification.nth_order_unification]
ordertyping_combine [lemma, in HOU.unification.nth_order_unification]
OrderTyping.Order [section, in HOU.calculus.order]
OrderTyping.PreservationOrdertyping [section, in HOU.calculus.order]
_ ⊩( _ ) _ : _ [notation, in HOU.calculus.order]
_ ⊢( _ ) _ : _ [notation, in HOU.calculus.order]
order_head [lemma, in HOU.calculus.order]
order_one_lambda_free [lemma, in HOU.firstorder]
ordsysuni [record, in HOU.unification.nth_order_unification]
ordsysuni_orduni [instance, in HOU.unification.nth_order_unification]
orduni [record, in HOU.unification.nth_order_unification]
orduni_normalise_correct [lemma, in HOU.unification.nth_order_unification]
orduni_normalise [instance, in HOU.unification.nth_order_unification]
orduni_ordsysuni [instance, in HOU.unification.nth_order_unification]
ord_target' [lemma, in HOU.calculus.order]
ord_target [lemma, in HOU.calculus.order]
ord_arr_one [lemma, in HOU.calculus.order]
ord_arr [lemma, in HOU.calculus.order]
ord_1 [lemma, in HOU.calculus.order]
ord_Gamma__deq [lemma, in HOU.second_order.goldfarb.encoding]
ord_repeated [lemma, in HOU.calculus.terms_extension]
ord_Arr [lemma, in HOU.calculus.terms_extension]
ord' [definition, in HOU.calculus.order]
ord'_cons [lemma, in HOU.calculus.order]
ord'_elements [lemma, in HOU.calculus.order]
ord'_in [lemma, in HOU.calculus.order]
ord'_rev [lemma, in HOU.calculus.order]
ord'_app [lemma, in HOU.calculus.order]
OU [definition, in HOU.unification.nth_order_unification]
OU_reduction [lemma, in HOU.unification.nth_order_unification]
OU_NOU [lemma, in HOU.unification.nth_order_unification]
OU_SOU [lemma, in HOU.unification.nth_order_unification]
P
pairs_retract [lemma, in HOU.std.enumerable]par [inductive, in HOU.calculus.confluence]
parApp [constructor, in HOU.calculus.confluence]
parBeta [constructor, in HOU.calculus.confluence]
parConst [constructor, in HOU.calculus.confluence]
parLam [constructor, in HOU.calculus.confluence]
partition_F_G [lemma, in HOU.second_order.goldfarb.encoding]
parVar [constructor, in HOU.calculus.confluence]
par_app_proper [instance, in HOU.calculus.confluence]
par_lam_proper [instance, in HOU.calculus.confluence]
PCP [definition, in HOU.third_order.pcp]
pcp [library]
PCPEquivalence [section, in HOU.third_order.pcp]
PCPsimp [definition, in HOU.third_order.pcp]
PCPsimp_PCP [lemma, in HOU.third_order.pcp]
PCP_U [lemma, in HOU.concon.conservativity]
PCP_U3 [lemma, in HOU.third_order.huet]
PCP_MU [lemma, in HOU.third_order.huet]
PCP_to_U [instance, in HOU.third_order.huet]
plus_proper [instance, in HOU.std.misc]
prelim [library]
preservation_consts [lemma, in HOU.concon.conservativity]
preservation_under_steps [lemma, in HOU.calculus.typing]
preservation_under_reduction [lemma, in HOU.calculus.typing]
preservation_under_substitution [lemma, in HOU.calculus.typing]
preservation_under_renaming [lemma, in HOU.calculus.typing]
prod_enumerable [instance, in HOU.std.enumerable]
projection [lemma, in HOU.std.enumerable]
projection' [lemma, in HOU.std.enumerable]
Properties [section, in HOU.std.retracts]
Properties.r [variable, in HOU.std.retracts]
Properties.X [variable, in HOU.std.retracts]
Properties.Y [variable, in HOU.std.retracts]
proper_rev_seteq [instance, in HOU.std.lists.basics]
proper_rev_incl [instance, in HOU.std.lists.basics]
proper_incl_seteq [instance, in HOU.std.lists.basics]
proper_app_seteq [instance, in HOU.std.lists.basics]
proper_app_incl [instance, in HOU.std.lists.basics]
proper_in_incl [instance, in HOU.std.lists.basics]
R
R [projection, in HOU.std.retracts]redctx [definition, in HOU.third_order.simplified]
redtm [definition, in HOU.third_order.simplified]
redtm_typing [lemma, in HOU.third_order.simplified]
reduction [definition, in HOU.std.reductions]
reduction [library]
reduction [library]
ReductionEncodings [section, in HOU.third_order.encoding]
Reductions [section, in HOU.std.reductions]
reductions [library]
Reductions.X [variable, in HOU.std.reductions]
Reductions.Y [variable, in HOU.std.reductions]
Reductions.Z [variable, in HOU.std.reductions]
_ ⪯ _ [notation, in HOU.std.reductions]
reduction_neg [lemma, in HOU.std.reductions]
reduction_reflexive [lemma, in HOU.std.reductions]
reduction_transitive [lemma, in HOU.std.reductions]
red_fun_rho [lemma, in HOU.std.ars.evaluator]
red_fun_normal [lemma, in HOU.std.ars.evaluator]
red_fun_fp_it [lemma, in HOU.std.ars.evaluator]
red_fun_fp [lemma, in HOU.std.ars.evaluator]
red_fun [definition, in HOU.std.ars.evaluator]
refl_equiv [lemma, in HOU.std.ars.basic]
refl_star [lemma, in HOU.std.ars.basic]
refl_par_inst [instance, in HOU.calculus.confluence]
refl_par [lemma, in HOU.calculus.confluence]
Remove [section, in HOU.std.lists.advanced]
RemoveConstants [section, in HOU.concon.constants]
RemoveConstants.consts_agree [variable, in HOU.concon.constants]
RemoveConstants.EncodingLemmas [section, in HOU.concon.constants]
RemoveConstants.EncodingLemmas.C [variable, in HOU.concon.constants]
RemoveConstants.EncodingLemmas.n [variable, in HOU.concon.constants]
RemoveConstants.EncodingLemmas.O [variable, in HOU.concon.constants]
RemoveConstants.enc_subst [variable, in HOU.concon.constants]
RemoveConstants.enc_ctx [variable, in HOU.concon.constants]
RemoveConstants.enc_type [variable, in HOU.concon.constants]
RemoveConstants.enc_term [variable, in HOU.concon.constants]
RemoveConstants.enc_var [variable, in HOU.concon.constants]
RemoveConstants.enc_const [variable, in HOU.concon.constants]
RemoveConstants.inv_subst [variable, in HOU.concon.constants]
RemoveConstants.inv_term [variable, in HOU.concon.constants]
RemoveConstants.RE [variable, in HOU.concon.constants]
RemoveConstants.R' [variable, in HOU.concon.constants]
RemoveConstants.X [variable, in HOU.concon.constants]
RemoveConstants.Y [variable, in HOU.concon.constants]
RemoveConstants.ι [variable, in HOU.concon.constants]
remove_constants_reduction [lemma, in HOU.concon.constants]
remove_constants_backward [lemma, in HOU.concon.constants]
remove_constants_forward [lemma, in HOU.concon.constants]
remove_constants [instance, in HOU.concon.constants]
remove_constants_ordertypingSubst [lemma, in HOU.concon.constants]
remove_constants_ordertyping [lemma, in HOU.concon.constants]
remove_prev [lemma, in HOU.std.lists.advanced]
remove_remain [lemma, in HOU.std.lists.advanced]
Remove.D [variable, in HOU.std.lists.advanced]
Remove.X [variable, in HOU.std.lists.advanced]
ren [abbreviation, in HOU.calculus.prelim]
renL [abbreviation, in HOU.calculus.terms_extension]
ren_plus_combine [lemma, in HOU.calculus.prelim]
ren_comp [lemma, in HOU.calculus.prelim]
ren_plus_base [lemma, in HOU.calculus.prelim]
ren_vars [lemma, in HOU.calculus.syntax]
ren_varof [lemma, in HOU.calculus.syntax]
ren_subst_consts_commute [lemma, in HOU.concon.conservativity]
ren_equiv_proper [instance, in HOU.calculus.equivalence]
ren_equiv [lemma, in HOU.calculus.equivalence]
ren_closed_G [lemma, in HOU.calculus.normalisation]
ren_closed_E [lemma, in HOU.calculus.normalisation]
ren_closed_V [lemma, in HOU.calculus.normalisation]
ren_closed_C [lemma, in HOU.calculus.normalisation]
ren_closed [definition, in HOU.calculus.normalisation]
ren_compatible_par [lemma, in HOU.calculus.confluence]
ren_exp [definition, in HOU.calculus.terms]
ren_steps_proper [instance, in HOU.calculus.semantics]
ren_step_proper [instance, in HOU.calculus.semantics]
ren_steps [lemma, in HOU.calculus.semantics]
ren_step [lemma, in HOU.calculus.semantics]
Repeated [section, in HOU.std.lists.advanced]
repeated_ordertyping [lemma, in HOU.calculus.terms_extension]
repeated_typing [lemma, in HOU.calculus.terms_extension]
repeated_app_inv [lemma, in HOU.std.lists.advanced]
repeated_tab [lemma, in HOU.std.lists.advanced]
repeated_incl [lemma, in HOU.std.lists.advanced]
repeated_equal [lemma, in HOU.std.lists.advanced]
repeated_length [lemma, in HOU.std.lists.advanced]
repeated_map [lemma, in HOU.std.lists.advanced]
repeated_rev [lemma, in HOU.std.lists.advanced]
repeated_plus [lemma, in HOU.std.lists.advanced]
repeated_in [lemma, in HOU.std.lists.advanced]
Repeated.X [variable, in HOU.std.lists.advanced]
Repeated.Y [variable, in HOU.std.lists.advanced]
retr [projection, in HOU.std.retracts]
retract [record, in HOU.std.retracts]
Retracts [section, in HOU.concon.constants]
retracts [library]
Retracts.consts_agree [variable, in HOU.concon.constants]
Retracts.inj [variable, in HOU.concon.constants]
Retracts.re [variable, in HOU.concon.constants]
Retracts.RE [variable, in HOU.concon.constants]
Retracts.X [variable, in HOU.concon.constants]
Retracts.Y [variable, in HOU.concon.constants]
retract_injective [lemma, in HOU.std.retracts]
retract_False [instance, in HOU.std.retracts]
retract_trans [instance, in HOU.std.retracts]
retract_refl [instance, in HOU.std.retracts]
retype [instance, in HOU.concon.retyping]
retype_iff [lemma, in HOU.concon.retyping]
retype_Arr [lemma, in HOU.concon.retyping]
retype_type_id [lemma, in HOU.concon.retyping]
retype_type_ord [lemma, in HOU.concon.retyping]
retype_type [definition, in HOU.concon.retyping]
retype_ctx_ord [lemma, in HOU.concon.retyping]
retype_ctx [definition, in HOU.concon.retyping]
Retyping [section, in HOU.concon.retyping]
retyping [library]
Retyping.X [variable, in HOU.concon.retyping]
rev_seteq [lemma, in HOU.std.lists.basics]
RE_cfree [instance, in HOU.concon.constants]
RE_abg_gonly [instance, in HOU.concon.constants]
re_typing [lemma, in HOU.concon.constants]
re_ren [lemma, in HOU.concon.constants]
rho [definition, in HOU.calculus.confluence]
rho_evaluates [lemma, in HOU.std.ars.evaluator]
right_ordertyping [lemma, in HOU.unification.nth_order_unification]
right_subst_eqs [lemma, in HOU.unification.systemunification]
right_typing [lemma, in HOU.unification.systemunification]
right_side [definition, in HOU.unification.systemunification]
rinstInst_exp [lemma, in HOU.calculus.terms]
rinstInst_up_exp_exp [definition, in HOU.calculus.terms]
rinst_inst_exp [definition, in HOU.calculus.terms]
R_nat_nat [definition, in HOU.std.enumerable]
R__S_I__S [lemma, in HOU.std.countability]
R__S [definition, in HOU.std.countability]
R__P_injective [lemma, in HOU.std.countability]
R__P_I__P [lemma, in HOU.std.countability]
R__P [definition, in HOU.std.countability]
S
sandwich_steps [instance, in HOU.calculus.confluence]sandwich_step [instance, in HOU.calculus.confluence]
sandwich_confluent [lemma, in HOU.std.ars.confluence]
sandwich_equiv [lemma, in HOU.std.ars.confluence]
sapp [definition, in HOU.calculus.prelim]
sapp_ge_in [lemma, in HOU.calculus.prelim]
sapp_lt_in [lemma, in HOU.calculus.prelim]
sapp_app [lemma, in HOU.calculus.prelim]
scons [definition, in HOU.unscoped]
scons_comp [lemma, in HOU.unscoped]
scons_eta_id [lemma, in HOU.unscoped]
scons_eta [lemma, in HOU.unscoped]
select [definition, in HOU.std.lists.advanced]
Select [section, in HOU.std.lists.advanced]
select_variables_subst [lemma, in HOU.calculus.prelim]
select_map [lemma, in HOU.std.lists.advanced]
select_incl [lemma, in HOU.std.lists.advanced]
select_repeated [lemma, in HOU.std.lists.advanced]
select_nats [lemma, in HOU.std.lists.advanced]
select_S [lemma, in HOU.std.lists.advanced]
select_nil [lemma, in HOU.std.lists.advanced]
Semantics [section, in HOU.calculus.semantics]
semantics [library]
Semantics.CompatibilityProperties [section, in HOU.calculus.semantics]
Semantics.InversionLemmas [section, in HOU.calculus.semantics]
Semantics.Normality [section, in HOU.calculus.semantics]
_ ▷ _ [notation, in HOU.calculus.semantics]
_ >* _ [notation, in HOU.calculus.semantics]
_ > _ [notation, in HOU.calculus.semantics]
SemanticTyping [section, in HOU.calculus.normalisation]
SemanticTyping.X [variable, in HOU.calculus.normalisation]
semantic_soundness [lemma, in HOU.calculus.normalisation]
semi_confluent [definition, in HOU.std.ars.confluence]
SemType [definition, in HOU.calculus.normalisation]
semtyping [definition, in HOU.calculus.normalisation]
seteq [definition, in HOU.std.lists.basics]
seteq_cons_proper [instance, in HOU.std.lists.basics]
seteq_incl_right [lemma, in HOU.std.lists.basics]
seteq_incl_left [lemma, in HOU.std.lists.basics]
seteq_equivalence [instance, in HOU.std.lists.basics]
seteq_preorder [instance, in HOU.std.lists.basics]
seteq_sym [lemma, in HOU.std.lists.basics]
seteq_trans [lemma, in HOU.std.lists.basics]
seteq_refl [lemma, in HOU.std.lists.basics]
shift [definition, in HOU.unscoped]
simplified [library]
singlepoint_subst_Vars'_variable [lemma, in HOU.firstorder]
singlepoint_subst_Vars' [lemma, in HOU.firstorder]
singlepoint_subst_vars_variable [lemma, in HOU.firstorder]
singlepoint_subst_vars [lemma, in HOU.firstorder]
size [definition, in HOU.firstorder]
size_exp [definition, in HOU.second_order.goldfarb.reduction]
size_subst [lemma, in HOU.firstorder]
size_ren [lemma, in HOU.firstorder]
SN [inductive, in HOU.std.ars.normalisation]
SNC [constructor, in HOU.std.ars.normalisation]
SNU [definition, in HOU.unification.systemunification]
SN_finite_steps [lemma, in HOU.std.ars.normalisation]
SN_morphism [lemma, in HOU.std.ars.normalisation]
SN_multiple [lemma, in HOU.std.ars.normalisation]
SN_unfold [lemma, in HOU.std.ars.normalisation]
SN_ext [lemma, in HOU.std.ars.normalisation]
Sol [definition, in HOU.second_order.diophantine_equations]
sol [inductive, in HOU.second_order.diophantine_equations]
solA [constructor, in HOU.second_order.diophantine_equations]
solC [constructor, in HOU.second_order.diophantine_equations]
solM [constructor, in HOU.second_order.diophantine_equations]
SOU [definition, in HOU.unification.nth_order_unification]
Soundness [section, in HOU.calculus.normalisation]
_ ⊨ _ : _ [notation, in HOU.calculus.normalisation]
SOU_NSOU [lemma, in HOU.unification.nth_order_unification]
SOU_OU [lemma, in HOU.unification.nth_order_unification]
stack [abbreviation, in HOU.third_order.pcp]
star [inductive, in HOU.std.ars.basic]
starL [inductive, in HOU.std.ars.basic]
starRefl [constructor, in HOU.std.ars.basic]
starReflL [constructor, in HOU.std.ars.basic]
starStep [constructor, in HOU.std.ars.basic]
starStepL [constructor, in HOU.std.ars.basic]
star_starL [lemma, in HOU.std.ars.basic]
star_absorbtion [lemma, in HOU.std.ars.basic]
star_idem [lemma, in HOU.std.ars.basic]
star_closure [lemma, in HOU.std.ars.basic]
star_mono [instance, in HOU.std.ars.basic]
star_exp [instance, in HOU.std.ars.basic]
star_preorder [instance, in HOU.std.ars.basic]
star_trans [lemma, in HOU.std.ars.basic]
std [library]
step [inductive, in HOU.calculus.semantics]
stepAppL [constructor, in HOU.calculus.semantics]
stepAppR [constructor, in HOU.calculus.semantics]
stepBeta [constructor, in HOU.calculus.semantics]
stepHead [constructor, in HOU.std.ars.list_reduction]
stepLam [constructor, in HOU.calculus.semantics]
steps_subst_consts [instance, in HOU.concon.conservativity]
steps_u_mult [lemma, in HOU.second_order.goldfarb.reduction]
steps_u [lemma, in HOU.second_order.goldfarb.reduction]
steps_anti_ren [lemma, in HOU.calculus.semantics]
steps_app_atom [lemma, in HOU.calculus.semantics]
steps_app [lemma, in HOU.calculus.semantics]
steps_lam [lemma, in HOU.calculus.semantics]
stepTail [constructor, in HOU.std.ars.list_reduction]
step_subst_consts [instance, in HOU.concon.conservativity]
step_star_multiple [lemma, in HOU.std.ars.basic]
step_u [lemma, in HOU.second_order.goldfarb.reduction]
step_anti_ren [lemma, in HOU.calculus.semantics]
strict_incl_incl_subrel [instance, in HOU.std.lists.basics]
strict_incl_project [lemma, in HOU.std.lists.basics]
strict_incl_eq [lemma, in HOU.std.lists.basics]
strict_incl_incl [lemma, in HOU.std.lists.basics]
strict_incl_transitive [instance, in HOU.std.lists.basics]
strict_incl_incl_trans [lemma, in HOU.std.lists.basics]
strict_incl_trans [lemma, in HOU.std.lists.basics]
strict_incl [definition, in HOU.std.lists.basics]
StrongNormalisation [section, in HOU.std.ars.normalisation]
StrongNormalisation.A [variable, in HOU.std.ars.normalisation]
StrongNormalisation.R [variable, in HOU.std.ars.normalisation]
StrongNormalisation.S [variable, in HOU.std.ars.normalisation]
StrongNormalisation.X [variable, in HOU.std.ars.normalisation]
SU [definition, in HOU.unification.systemunification]
subrel_unfold [lemma, in HOU.std.ars.basic]
subrel_incl_seteq [instance, in HOU.std.lists.basics]
SubstitutionTransformations [section, in HOU.unification.higher_order_unification]
SubstitutionTransformations [section, in HOU.unification.nth_order_unification]
SubstitutionTransformations.A [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.A [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.Gamma [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.Gamma [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.Leq [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.Leq [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.n [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.n [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.s [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.s [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.t [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.t [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.T1 [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.T1 [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.T2 [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.T2 [variable, in HOU.unification.nth_order_unification]
SubstitutionTransformations.X [variable, in HOU.unification.higher_order_unification]
SubstitutionTransformations.X [variable, in HOU.unification.nth_order_unification]
subst_vars [lemma, in HOU.calculus.syntax]
subst_varof [lemma, in HOU.calculus.syntax]
subst_extensional [lemma, in HOU.calculus.syntax]
subst_consts_AppR [lemma, in HOU.concon.conservativity]
subst_consts_AppL [lemma, in HOU.concon.conservativity]
subst_consts_Lambda [lemma, in HOU.concon.conservativity]
subst_const_comm_id [lemma, in HOU.concon.conservativity]
subst_consts_up [lemma, in HOU.concon.conservativity]
subst_consts_consts [lemma, in HOU.concon.conservativity]
subst_const_comm [lemma, in HOU.concon.conservativity]
subst_consts_ident [lemma, in HOU.concon.conservativity]
subst_consts_comp [lemma, in HOU.concon.conservativity]
subst_consts [definition, in HOU.concon.conservativity]
subst_pointwise_equiv [lemma, in HOU.calculus.equivalence]
subst_equiv_proper [instance, in HOU.calculus.equivalence]
subst_equiv [lemma, in HOU.calculus.equivalence]
subst_compatible_par [lemma, in HOU.calculus.confluence]
subst_exp [definition, in HOU.calculus.terms]
subst_T [lemma, in HOU.second_order.goldfarb.reduction]
subst_enc_step [lemma, in HOU.second_order.goldfarb.reduction]
subst_var_b [lemma, in HOU.second_order.goldfarb.reduction]
subst_var_a [lemma, in HOU.second_order.goldfarb.reduction]
subst_var [lemma, in HOU.second_order.goldfarb.reduction]
subst_steps_proper [instance, in HOU.calculus.semantics]
subst_step_proper [instance, in HOU.calculus.semantics]
subst_steps [lemma, in HOU.calculus.semantics]
subst_step [lemma, in HOU.calculus.semantics]
subst_consts_subst [lemma, in HOU.concon.constants]
subst_consts_inject_backwards [lemma, in HOU.concon.constants]
subst_consts_inject_forward [lemma, in HOU.concon.constants]
subst_eq [definition, in HOU.unification.systemunification]
subvars [definition, in HOU.firstorder]
sub_sol_enc [lemma, in HOU.second_order.dowek.reduction]
sub_sol [definition, in HOU.second_order.dowek.reduction]
Succ [definition, in HOU.second_order.goldfarb.motivation]
succ [definition, in HOU.second_order.goldfarb.motivation]
succ' [abbreviation, in HOU.second_order.goldfarb.motivation]
Sum [definition, in HOU.std.misc]
Sum_app [lemma, in HOU.std.misc]
Sum_in [lemma, in HOU.std.misc]
SU_conservative_backward [lemma, in HOU.concon.conservativity]
SU_conservative_forward [lemma, in HOU.concon.conservativity]
SU_conservative [instance, in HOU.concon.conservativity]
SU_monotone_backward [lemma, in HOU.concon.conservativity]
SU_monotone_forward [lemma, in HOU.concon.conservativity]
SU_monotone [instance, in HOU.concon.conservativity]
SU_H10 [lemma, in HOU.second_order.goldfarb.reduction]
SU_SNU [lemma, in HOU.unification.systemunification]
SU_U [lemma, in HOU.unification.systemunification]
sym [inductive, in HOU.std.ars.basic]
symbol [abbreviation, in HOU.third_order.pcp]
symId [constructor, in HOU.std.ars.basic]
symInv [constructor, in HOU.std.ars.basic]
sym_Symmetric [instance, in HOU.std.ars.basic]
sym_symmetric [lemma, in HOU.std.ars.basic]
syntax [library]
SystemUnification [section, in HOU.unification.systemunification]
systemunification [library]
systemunification_conserve [lemma, in HOU.concon.conservativity]
systemunification_steps [lemma, in HOU.concon.conservativity]
systemunification_step [lemma, in HOU.concon.conservativity]
SystemUnification.X [variable, in HOU.unification.systemunification]
_ •₊₊ _ [notation, in HOU.unification.systemunification]
_ ⊢₊₊ _ : _ [notation, in HOU.unification.systemunification]
_ ⊢₂ _ : _ [notation, in HOU.unification.systemunification]
sysuni [record, in HOU.unification.systemunification]
sysuni_uni [instance, in HOU.unification.systemunification]
sᵤ [projection, in HOU.unification.higher_order_unification]
s₀ [projection, in HOU.unification.nth_order_unification]
T
T [definition, in HOU.second_order.goldfarb.reduction]tab [definition, in HOU.std.lists.advanced]
Tabulate [section, in HOU.std.lists.advanced]
tab_typing [lemma, in HOU.second_order.goldfarb.reduction]
tab_subst [lemma, in HOU.calculus.terms_extension]
tab_nth [lemma, in HOU.std.lists.advanced]
tab_id_nats [lemma, in HOU.std.lists.advanced]
tab_map_nats [lemma, in HOU.std.lists.advanced]
tab_plus [lemma, in HOU.std.lists.advanced]
tab_S [lemma, in HOU.std.lists.advanced]
tab_map [lemma, in HOU.std.lists.advanced]
tab_length [lemma, in HOU.std.lists.advanced]
tactics [library]
tails [abbreviation, in HOU.third_order.pcp]
Takahashi [section, in HOU.std.ars.confluence]
Takahashi.R [variable, in HOU.std.ars.confluence]
Takahashi.rho [variable, in HOU.std.ars.confluence]
Takahashi.tak [variable, in HOU.std.ars.confluence]
Takahashi.X [variable, in HOU.std.ars.confluence]
_ >* _ [notation, in HOU.std.ars.confluence]
_ > _ [notation, in HOU.std.ars.confluence]
tak_fun_rho [lemma, in HOU.calculus.confluence]
tak_cofinal [lemma, in HOU.std.ars.confluence]
tak_mono_n [lemma, in HOU.std.ars.confluence]
tak_mono [lemma, in HOU.std.ars.confluence]
tak_sound [lemma, in HOU.std.ars.confluence]
tak_diamond [lemma, in HOU.std.ars.confluence]
tak_fun [definition, in HOU.std.ars.confluence]
target [definition, in HOU.calculus.syntax]
target_Arr [lemma, in HOU.calculus.terms_extension]
target_ord [lemma, in HOU.calculus.terms_extension]
target' [definition, in HOU.calculus.syntax]
termination_steps [lemma, in HOU.calculus.normalisation]
Terms [section, in HOU.calculus.terms]
terms [library]
TermsExtension [section, in HOU.calculus.terms_extension]
TermsExtension.ArrowProperties [section, in HOU.calculus.terms_extension]
TermsExtension.EquivalenceInversions [section, in HOU.calculus.terms_extension]
TermsExtension.ListOperatorsCompatibilityProperties [section, in HOU.calculus.terms_extension]
TermsExtension.ListOperatorsSubstitutionRenaming [section, in HOU.calculus.terms_extension]
TermsExtension.ListOperatorsTyping [section, in HOU.calculus.terms_extension]
TermsExtension.ListSemanticProperties [section, in HOU.calculus.terms_extension]
TermsExtension.ListTypingProperties [section, in HOU.calculus.terms_extension]
TermsExtension.Normality [section, in HOU.calculus.terms_extension]
TermsExtension.Utilities [section, in HOU.calculus.terms_extension]
_ ≡₊ _ [notation, in HOU.calculus.terms_extension]
_ >₊* _ [notation, in HOU.calculus.terms_extension]
_ >₊ _ [notation, in HOU.calculus.terms_extension]
_ ⊢₊( _ ) _ : _ [notation, in HOU.calculus.terms_extension]
_ ⊢₊ _ : _ [notation, in HOU.calculus.terms_extension]
terms_extension [library]
tight [definition, in HOU.std.retracts]
tight_retr [lemma, in HOU.std.retracts]
tight_is_tight [lemma, in HOU.std.retracts]
tl [abbreviation, in HOU.third_order.pcp]
TMT [lemma, in HOU.std.ars.confluence]
TMT [section, in HOU.std.ars.confluence]
TMT.H1 [variable, in HOU.std.ars.confluence]
TMT.H2 [variable, in HOU.std.ars.confluence]
TMT.R [variable, in HOU.std.ars.confluence]
TMT.S [variable, in HOU.std.ars.confluence]
TMT.X [variable, in HOU.std.ars.confluence]
_ === _ [notation, in HOU.std.ars.confluence]
_ <<= _ [notation, in HOU.std.ars.confluence]
type [inductive, in HOU.calculus.terms]
TypeFunctions [section, in HOU.calculus.syntax]
typevar [constructor, in HOU.calculus.terms]
type_dis [instance, in HOU.calculus.syntax]
type_decompose [lemma, in HOU.calculus.terms_extension]
Typing [section, in HOU.second_order.goldfarb.encoding]
typing [inductive, in HOU.calculus.typing]
Typing [section, in HOU.calculus.typing]
typing [library]
typingApp [constructor, in HOU.calculus.typing]
typingConst [constructor, in HOU.calculus.typing]
typingLam [constructor, in HOU.calculus.typing]
typingRen [definition, in HOU.calculus.typing]
typingSubst [definition, in HOU.calculus.typing]
typingSubst_cons [lemma, in HOU.calculus.typing]
typingVar [constructor, in HOU.calculus.typing]
typing_Consts [lemma, in HOU.concon.conservativity]
typing_constants [lemma, in HOU.concon.conservativity]
typing_strong_ind [definition, in HOU.unification.enumerability]
typing_forward [lemma, in HOU.second_order.goldfarb.reduction]
typing_equations [lemma, in HOU.second_order.goldfarb.encoding]
typing_mul2 [lemma, in HOU.second_order.goldfarb.encoding]
typing_mul1 [lemma, in HOU.second_order.goldfarb.encoding]
typing_add [lemma, in HOU.second_order.goldfarb.encoding]
typing_const [lemma, in HOU.second_order.goldfarb.encoding]
typing_var_eq [lemma, in HOU.second_order.goldfarb.encoding]
typing_G [lemma, in HOU.second_order.goldfarb.encoding]
typing_F [lemma, in HOU.second_order.goldfarb.encoding]
typing_g [lemma, in HOU.second_order.goldfarb.encoding]
typing_b [lemma, in HOU.second_order.goldfarb.encoding]
typing_a [lemma, in HOU.second_order.goldfarb.encoding]
typing_equations [lemma, in HOU.second_order.dowek.encoding]
typing_mulEQ [lemma, in HOU.second_order.dowek.encoding]
typing_addEQ [lemma, in HOU.second_order.dowek.encoding]
typing_constEQ [lemma, in HOU.second_order.dowek.encoding]
typing_varEQ [lemma, in HOU.second_order.dowek.encoding]
typing_enc [lemma, in HOU.second_order.dowek.encoding]
typing_variables [lemma, in HOU.calculus.typing]
typing_combine [lemma, in HOU.unification.systemunification]
Typing.E [variable, in HOU.second_order.goldfarb.encoding]
Typing.Preservation [section, in HOU.calculus.typing]
_ ⊩ _ : _ [notation, in HOU.calculus.typing]
_ ⊫ _ : _ [notation, in HOU.calculus.typing]
_ ⊢ _ : _ [notation, in HOU.calculus.typing]
T_step_tau2_sigma2 [lemma, in HOU.second_order.goldfarb.reduction]
T_step_tau1_sigma1 [lemma, in HOU.second_order.goldfarb.reduction]
T_list_el [lemma, in HOU.std.enumerable]
T_list_cum [lemma, in HOU.std.enumerable]
T_list [definition, in HOU.std.enumerable]
T_prod_el [lemma, in HOU.std.enumerable]
T_prod_cum [lemma, in HOU.std.enumerable]
T_prod [definition, in HOU.std.enumerable]
T_nat_length [lemma, in HOU.std.enumerable]
T_nat_in [lemma, in HOU.std.enumerable]
T_ [definition, in HOU.std.enumerable]
tᵤ [projection, in HOU.unification.higher_order_unification]
t₀ [projection, in HOU.unification.nth_order_unification]
U
U [definition, in HOU.unification.higher_order_unification]Uextended [definition, in HOU.unification.enumerability]
uni [record, in HOU.unification.higher_order_unification]
unif [definition, in HOU.firstorder]
Unification [section, in HOU.firstorder]
unification [library]
UnificationDefinitions [section, in HOU.unification.higher_order_unification]
unification_conserve [lemma, in HOU.concon.conservativity]
unification_steps [lemma, in HOU.concon.conservativity]
unification_step [lemma, in HOU.concon.conservativity]
unification_conservative_backward [lemma, in HOU.concon.conservativity]
unification_conservative_forward [lemma, in HOU.concon.conservativity]
unification_conservative [instance, in HOU.concon.conservativity]
unification_monotone_backward [lemma, in HOU.concon.conservativity]
unification_monotone_forward [lemma, in HOU.concon.conservativity]
unification_monotone [instance, in HOU.concon.conservativity]
unification_downcast_eqs [lemma, in HOU.concon.conservativity]
unification_downcast [lemma, in HOU.concon.conservativity]
unification_constants_monotone [lemma, in HOU.concon.constants]
unification_retract_backward [lemma, in HOU.concon.constants]
unification_retract_forward [lemma, in HOU.concon.constants]
unification_retract [instance, in HOU.concon.constants]
Unification.Completeness [section, in HOU.firstorder]
Unification.Computability [section, in HOU.firstorder]
Unification.Decomposition [section, in HOU.firstorder]
Unification.Equations [section, in HOU.firstorder]
Unification.free [variable, in HOU.firstorder]
Unification.isFree [variable, in HOU.firstorder]
Unification.Soundness [section, in HOU.firstorder]
Unification.Soundness.Gamma [variable, in HOU.firstorder]
Unification.Soundness.HO [variable, in HOU.firstorder]
Unification.Unifiability [section, in HOU.firstorder]
_ ≈ _ [notation, in HOU.firstorder]
Unification.X [variable, in HOU.firstorder]
_ ↦ _ [notation, in HOU.firstorder]
Unifies [definition, in HOU.firstorder]
unifies [definition, in HOU.firstorder]
unifies_free_all [lemma, in HOU.firstorder]
unifies_free [lemma, in HOU.firstorder]
unifies_not_var [lemma, in HOU.firstorder]
Unifies_app [lemma, in HOU.firstorder]
Unifies_nil [lemma, in HOU.firstorder]
Unifies_cons [lemma, in HOU.firstorder]
unifies_equiv [instance, in HOU.firstorder]
unifiy_computable [lemma, in HOU.firstorder]
unify [inductive, in HOU.firstorder]
unifyId [constructor, in HOU.firstorder]
unifyStep [constructor, in HOU.firstorder]
unify_complete [lemma, in HOU.firstorder]
unify_typing [lemma, in HOU.firstorder]
unify_free' [lemma, in HOU.firstorder]
unify_unifiable [lemma, in HOU.firstorder]
unify_lambda_free [lemma, in HOU.firstorder]
unif_correct [lemma, in HOU.firstorder]
uni_normalise_correct [lemma, in HOU.unification.higher_order_unification]
uni_normalise [instance, in HOU.unification.higher_order_unification]
uni_sysuni [instance, in HOU.unification.systemunification]
unscoped [library]
up [abbreviation, in HOU.calculus.prelim]
update [definition, in HOU.firstorder]
Update [section, in HOU.firstorder]
update_typing [lemma, in HOU.firstorder]
update_irrelevant [lemma, in HOU.firstorder]
upExtRen_exp_exp [definition, in HOU.calculus.terms]
upExt_exp_exp [definition, in HOU.calculus.terms]
upId_exp_exp [definition, in HOU.calculus.terms]
upRen_exp_exp [definition, in HOU.calculus.terms]
up_ren_ren [lemma, in HOU.unscoped]
up_ren [definition, in HOU.unscoped]
up_subst_subst_exp_exp [definition, in HOU.calculus.terms]
up_subst_ren_exp_exp [definition, in HOU.calculus.terms]
up_ren_subst_exp_exp [definition, in HOU.calculus.terms]
up_exp_exp [definition, in HOU.calculus.terms]
U_reduction [lemma, in HOU.unification.higher_order_unification]
U_NU [lemma, in HOU.unification.higher_order_unification]
U_NU [lemma, in HOU.unification.nth_order_unification]
U_SU [lemma, in HOU.unification.systemunification]
U3_MPCP' [lemma, in HOU.third_order.simplified]
V
V [definition, in HOU.calculus.normalisation]var [abbreviation, in HOU.calculus.prelim]
varEQ [definition, in HOU.second_order.goldfarb.encoding]
varEQ [definition, in HOU.second_order.dowek.encoding]
Variables [section, in HOU.second_order.goldfarb.encoding]
varL_exp [lemma, in HOU.calculus.terms]
varof [inductive, in HOU.calculus.syntax]
varofAppL [constructor, in HOU.calculus.syntax]
varofAppR [constructor, in HOU.calculus.syntax]
varofLambda [constructor, in HOU.calculus.syntax]
varofVar [constructor, in HOU.calculus.syntax]
varof_subst [lemma, in HOU.calculus.syntax]
varof_ren [lemma, in HOU.calculus.syntax]
varof_vars [lemma, in HOU.calculus.syntax]
vars [definition, in HOU.calculus.syntax]
Vars [abbreviation, in HOU.calculus.terms_extension]
vars_subst [lemma, in HOU.calculus.syntax]
vars_ren [lemma, in HOU.calculus.syntax]
vars_varof [lemma, in HOU.calculus.syntax]
vars_subst_consts [lemma, in HOU.concon.conservativity]
vars_ordertyping_nth [lemma, in HOU.calculus.order]
vars_ordertyping [lemma, in HOU.calculus.order]
Vars__de_in [lemma, in HOU.second_order.diophantine_equations]
Vars__de [definition, in HOU.second_order.diophantine_equations]
vars__de [definition, in HOU.second_order.diophantine_equations]
Vars_decomp' [lemma, in HOU.firstorder]
vars_decomp [lemma, in HOU.firstorder]
Vars_listordertyping [lemma, in HOU.calculus.terms_extension]
Vars_listtyping [lemma, in HOU.calculus.terms_extension]
Vars' [definition, in HOU.unification.systemunification]
vars' [definition, in HOU.unification.systemunification]
Vars'_app [lemma, in HOU.unification.systemunification]
Vars'_cons [lemma, in HOU.unification.systemunification]
var_head [lemma, in HOU.calculus.syntax]
var_zero [definition, in HOU.unscoped]
var_exp [constructor, in HOU.calculus.terms]
var_typing [lemma, in HOU.calculus.terms_extension]
W
weakening_ordertyping_app [lemma, in HOU.calculus.order]weakening_app [lemma, in HOU.calculus.typing]
wf_strict_incl [lemma, in HOU.std.lists.basics]
wf_subvars [instance, in HOU.firstorder]
word [abbreviation, in HOU.third_order.pcp]
w1 [abbreviation, in HOU.second_order.goldfarb.reduction]
w2 [abbreviation, in HOU.second_order.goldfarb.reduction]
w3 [abbreviation, in HOU.second_order.goldfarb.reduction]
X
xi [definition, in HOU.calculus.evaluator]xi_monotone [lemma, in HOU.calculus.evaluator]
xi_correct [lemma, in HOU.calculus.evaluator]
X_unique [lemma, in HOU.second_order.goldfarb.motivation]
X_satisfies [lemma, in HOU.second_order.goldfarb.motivation]
other
_ • _ [notation, in HOU.calculus.prelim]_ → _ [notation, in HOU.calculus.prelim]
_ .+ _ [notation, in HOU.calculus.prelim]
_ ≡ _ [notation, in HOU.calculus.equivalence]
_ ⊩( _ ) _ : _ [notation, in HOU.calculus.order]
_ ⊢( _ ) _ : _ [notation, in HOU.calculus.order]
_ >> _ [notation, in HOU.std.misc]
_ ≫ _ [notation, in HOU.calculus.confluence]
_ .: _ [notation, in HOU.unscoped]
_ === _ [notation, in HOU.std.lists.basics]
_ ⊊ _ [notation, in HOU.std.lists.basics]
_ ⊆ _ [notation, in HOU.std.lists.basics]
_ ∈ _ [notation, in HOU.std.lists.basics]
_ ⪯ _ [notation, in HOU.std.reductions]
_ ⊢⁺ₑ _ [notation, in HOU.second_order.diophantine_equations]
_ ⊢ₑ _ [notation, in HOU.second_order.diophantine_equations]
_ *ₑ _ =ₑ _ [notation, in HOU.second_order.diophantine_equations]
_ +ₑ _ =ₑ _ [notation, in HOU.second_order.diophantine_equations]
_ =ₑ _ [notation, in HOU.second_order.diophantine_equations]
_ ▷ _ [notation, in HOU.calculus.semantics]
_ >* _ [notation, in HOU.calculus.semantics]
_ > _ [notation, in HOU.calculus.semantics]
_ ⊩ _ : _ [notation, in HOU.calculus.typing]
_ ⊫ _ : _ [notation, in HOU.calculus.typing]
_ ⊢ _ : _ [notation, in HOU.calculus.typing]
_ ⊢₂( _ ) _ : _ [notation, in HOU.unification.nth_order_unification]
_ ⊢₊₊( _ ) _ : _ [notation, in HOU.unification.nth_order_unification]
_ ⊢₊( _ ) _ : _ [notation, in HOU.calculus.terms_extension]
_ ⊢₊ _ : _ [notation, in HOU.calculus.terms_extension]
_ ≡₊ _ [notation, in HOU.calculus.terms_extension]
_ >₊* _ [notation, in HOU.calculus.terms_extension]
_ >₊ _ [notation, in HOU.calculus.terms_extension]
_ •₊ _ [notation, in HOU.calculus.terms_extension]
_ ⊢₂ _ : _ [notation, in HOU.unification.systemunification]
_ ⊢₊₊ _ : _ [notation, in HOU.unification.systemunification]
_ •₊₊ _ [notation, in HOU.unification.systemunification]
_ el _ [notation, in HOU.std.decidable]
_ == _ [notation, in HOU.std.decidable]
lambda _ [notation, in HOU.calculus.prelim]
( _ × _ × .. × _ ) [notation, in HOU.std.enumerable]
[ _ | _ ∈ _ & _ ∈ _ where _ : _ ] [notation, in HOU.std.enumerable]
[ _ | _ ∈ _ & _ ∈ _ ] [notation, in HOU.std.enumerable]
[ _ | _ ∈ _ where _ : _ ] [notation, in HOU.std.enumerable]
[ _ where _ : _ ] [notation, in HOU.std.enumerable]
[ _ | _ ∈ _ ] [notation, in HOU.std.enumerable]
[ _ | _ ∈ _ , _ ] [notation, in HOU.std.enumerable]
| _ | [notation, in HOU.std.lists.basics]
Notation Index
C
_ === _ [in HOU.std.ars.basic]_ <<= _ [in HOU.std.ars.basic]
_ ≫ _ [in HOU.calculus.confluence]
_ === _ [in HOU.std.ars.confluence]
_ <<= _ [in HOU.std.ars.confluence]
E
_ ≡ _ [in HOU.calculus.equivalence]M
_ ≈ _ ⟶ _ [in HOU.second_order.goldfarb.motivation]N
_ ⊢₊₊( _ ) _ : _ [in HOU.unification.nth_order_unification]_ ⊢₂( _ ) _ : _ [in HOU.unification.nth_order_unification]
O
_ ⊩( _ ) _ : _ [in HOU.calculus.order]_ ⊢( _ ) _ : _ [in HOU.calculus.order]
R
_ ⪯ _ [in HOU.std.reductions]S
_ ▷ _ [in HOU.calculus.semantics]_ >* _ [in HOU.calculus.semantics]
_ > _ [in HOU.calculus.semantics]
_ ⊨ _ : _ [in HOU.calculus.normalisation]
_ •₊₊ _ [in HOU.unification.systemunification]
_ ⊢₊₊ _ : _ [in HOU.unification.systemunification]
_ ⊢₂ _ : _ [in HOU.unification.systemunification]
T
_ >* _ [in HOU.std.ars.confluence]_ > _ [in HOU.std.ars.confluence]
_ ≡₊ _ [in HOU.calculus.terms_extension]
_ >₊* _ [in HOU.calculus.terms_extension]
_ >₊ _ [in HOU.calculus.terms_extension]
_ ⊢₊( _ ) _ : _ [in HOU.calculus.terms_extension]
_ ⊢₊ _ : _ [in HOU.calculus.terms_extension]
_ === _ [in HOU.std.ars.confluence]
_ <<= _ [in HOU.std.ars.confluence]
_ ⊩ _ : _ [in HOU.calculus.typing]
_ ⊫ _ : _ [in HOU.calculus.typing]
_ ⊢ _ : _ [in HOU.calculus.typing]
U
_ ≈ _ [in HOU.firstorder]_ ↦ _ [in HOU.firstorder]
other
_ • _ [in HOU.calculus.prelim]_ → _ [in HOU.calculus.prelim]
_ .+ _ [in HOU.calculus.prelim]
_ ≡ _ [in HOU.calculus.equivalence]
_ ⊩( _ ) _ : _ [in HOU.calculus.order]
_ ⊢( _ ) _ : _ [in HOU.calculus.order]
_ >> _ [in HOU.std.misc]
_ ≫ _ [in HOU.calculus.confluence]
_ .: _ [in HOU.unscoped]
_ === _ [in HOU.std.lists.basics]
_ ⊊ _ [in HOU.std.lists.basics]
_ ⊆ _ [in HOU.std.lists.basics]
_ ∈ _ [in HOU.std.lists.basics]
_ ⪯ _ [in HOU.std.reductions]
_ ⊢⁺ₑ _ [in HOU.second_order.diophantine_equations]
_ ⊢ₑ _ [in HOU.second_order.diophantine_equations]
_ *ₑ _ =ₑ _ [in HOU.second_order.diophantine_equations]
_ +ₑ _ =ₑ _ [in HOU.second_order.diophantine_equations]
_ =ₑ _ [in HOU.second_order.diophantine_equations]
_ ▷ _ [in HOU.calculus.semantics]
_ >* _ [in HOU.calculus.semantics]
_ > _ [in HOU.calculus.semantics]
_ ⊩ _ : _ [in HOU.calculus.typing]
_ ⊫ _ : _ [in HOU.calculus.typing]
_ ⊢ _ : _ [in HOU.calculus.typing]
_ ⊢₂( _ ) _ : _ [in HOU.unification.nth_order_unification]
_ ⊢₊₊( _ ) _ : _ [in HOU.unification.nth_order_unification]
_ ⊢₊( _ ) _ : _ [in HOU.calculus.terms_extension]
_ ⊢₊ _ : _ [in HOU.calculus.terms_extension]
_ ≡₊ _ [in HOU.calculus.terms_extension]
_ >₊* _ [in HOU.calculus.terms_extension]
_ >₊ _ [in HOU.calculus.terms_extension]
_ •₊ _ [in HOU.calculus.terms_extension]
_ ⊢₂ _ : _ [in HOU.unification.systemunification]
_ ⊢₊₊ _ : _ [in HOU.unification.systemunification]
_ •₊₊ _ [in HOU.unification.systemunification]
_ el _ [in HOU.std.decidable]
_ == _ [in HOU.std.decidable]
lambda _ [in HOU.calculus.prelim]
( _ × _ × .. × _ ) [in HOU.std.enumerable]
[ _ | _ ∈ _ & _ ∈ _ where _ : _ ] [in HOU.std.enumerable]
[ _ | _ ∈ _ & _ ∈ _ ] [in HOU.std.enumerable]
[ _ | _ ∈ _ where _ : _ ] [in HOU.std.enumerable]
[ _ where _ : _ ] [in HOU.std.enumerable]
[ _ | _ ∈ _ ] [in HOU.std.enumerable]
[ _ | _ ∈ _ , _ ] [in HOU.std.enumerable]
| _ | [in HOU.std.lists.basics]
Variable Index
A
ApplicativeHead.X [in HOU.calculus.syntax]Atoms.X [in HOU.calculus.syntax]
B
Backward.X [in HOU.second_order.dowek.reduction]BasicLemmas.X [in HOU.std.lists.basics]
BasicLemmas.Y [in HOU.std.lists.basics]
C
ClosureRelations.X [in HOU.std.ars.basic]Confluence.X [in HOU.std.ars.confluence]
Conservativity.DowncastLemmas.Leq [in HOU.concon.conservativity]
Conservativity.DowncastLemmas.n [in HOU.concon.conservativity]
Conservativity.X [in HOU.concon.conservativity]
E
Encoding.Typing.E [in HOU.second_order.dowek.encoding]Encoding.u [in HOU.third_order.encoding]
Encoding.u_neq_v [in HOU.third_order.encoding]
Encoding.v [in HOU.third_order.encoding]
enumerable_list.fixL.LX [in HOU.std.enumerable]
enumerable_list.X [in HOU.std.enumerable]
enumerable_prod.fixLs.L_Y [in HOU.std.enumerable]
enumerable_prod.fixLs.L_X [in HOU.std.enumerable]
enumerable_prod.Y [in HOU.std.enumerable]
enumerable_prod.X [in HOU.std.enumerable]
enumerable_enum.e [in HOU.std.enumerable]
enumerable_enum.p [in HOU.std.enumerable]
enumerable_enum.X [in HOU.std.enumerable]
enum_red2.LX [in HOU.std.reductions]
enum_red2.d [in HOU.std.reductions]
enum_red2.qe [in HOU.std.reductions]
enum_red2.Lq [in HOU.std.reductions]
enum_red2.Hg [in HOU.std.reductions]
enum_red2.g [in HOU.std.reductions]
enum_red2.Hf [in HOU.std.reductions]
enum_red2.f [in HOU.std.reductions]
enum_red2.q [in HOU.std.reductions]
enum_red2.p [in HOU.std.reductions]
enum_red2.Z [in HOU.std.reductions]
enum_red2.Y [in HOU.std.reductions]
enum_red2.X [in HOU.std.reductions]
enum_red.d [in HOU.std.reductions]
enum_red.x0 [in HOU.std.reductions]
enum_red.qe [in HOU.std.reductions]
enum_red.Lq [in HOU.std.reductions]
enum_red.Hf [in HOU.std.reductions]
enum_red.f [in HOU.std.reductions]
enum_red.q [in HOU.std.reductions]
enum_red.p [in HOU.std.reductions]
enum_red.Y [in HOU.std.reductions]
enum_red.X [in HOU.std.reductions]
EquationEquivalences.Addition.c [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.EQx [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.EQy [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.EQz [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.Ex [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.Ey [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.Ez [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.m [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.m [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.n [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.n [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.p [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.p [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.x [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.x [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.y [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.y [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition.z [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition.z [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.c [in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.c [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.EQx [in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.Ex [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.n [in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.n [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants.x [in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants.x [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.c [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.EQx [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.EQy [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.EQz [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.Ex [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.Ey [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.Ez [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.m [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.m [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationBackward.EQ1 [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationBackward.EQ2 [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.n [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.n [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.p [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.p [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.x [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.x [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.y [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.y [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.z [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication.z [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.σ1 [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.σ2 [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.τ1 [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.τ2 [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.N [in HOU.second_order.dowek.reduction]
EquationEquivalences.N [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.sigma [in HOU.second_order.dowek.reduction]
EquationEquivalences.sigma [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.X [in HOU.second_order.dowek.reduction]
EquivalenceInversion.EQ [in HOU.third_order.encoding]
EquivalenceInversion.H1 [in HOU.third_order.encoding]
EquivalenceInversion.N [in HOU.third_order.encoding]
EquivalenceInversion.S [in HOU.third_order.encoding]
EquivalenceInversion.s [in HOU.third_order.encoding]
EquivalenceInversion.sigma [in HOU.third_order.encoding]
EquivalenceInversion.t [in HOU.third_order.encoding]
EquivalenceInversion.x [in HOU.third_order.encoding]
EquivalenceInversion.X [in HOU.third_order.encoding]
Equivalence.HuetDefinition.E1 [in HOU.calculus.equivalence]
Equivalence.HuetDefinition.E2 [in HOU.calculus.equivalence]
Equivalence.HuetDefinition.s [in HOU.calculus.equivalence]
Equivalence.HuetDefinition.t [in HOU.calculus.equivalence]
Equivalence.HuetDefinition.v1 [in HOU.calculus.equivalence]
Equivalence.HuetDefinition.v2 [in HOU.calculus.equivalence]
EvaluatorTakahashi.D [in HOU.std.ars.evaluator]
EvaluatorTakahashi.H1 [in HOU.std.ars.evaluator]
EvaluatorTakahashi.H2 [in HOU.std.ars.evaluator]
EvaluatorTakahashi.R [in HOU.std.ars.evaluator]
EvaluatorTakahashi.refl [in HOU.std.ars.evaluator]
EvaluatorTakahashi.rho [in HOU.std.ars.evaluator]
EvaluatorTakahashi.S [in HOU.std.ars.evaluator]
EvaluatorTakahashi.tf [in HOU.std.ars.evaluator]
EvaluatorTakahashi.X [in HOU.std.ars.evaluator]
Evaluator.Correctness.A [in HOU.calculus.evaluator]
Evaluator.Correctness.Gamma [in HOU.calculus.evaluator]
Evaluator.Correctness.H [in HOU.calculus.evaluator]
Evaluator.Correctness.H₀ [in HOU.calculus.evaluator]
Evaluator.Correctness.n [in HOU.calculus.evaluator]
Evaluator.Correctness.s [in HOU.calculus.evaluator]
Evaluator.delta [in HOU.std.ars.evaluator]
Evaluator.R [in HOU.std.ars.evaluator]
Evaluator.red [in HOU.std.ars.evaluator]
Evaluator.rho [in HOU.std.ars.evaluator]
Evaluator.X [in HOU.std.ars.evaluator]
F
FirstOrderDecidable.free [in HOU.firstorder]FirstOrderDecidable.X [in HOU.firstorder]
FlatMap.X [in HOU.std.lists.advanced]
FlatMap.Y [in HOU.std.lists.advanced]
Forward.E [in HOU.second_order.dowek.reduction]
Forward.E [in HOU.second_order.goldfarb.reduction]
Forward.X [in HOU.second_order.dowek.reduction]
H
HuetReduction.BackwardDirection.EQ [in HOU.third_order.huet]HuetReduction.BackwardDirection.H1 [in HOU.third_order.huet]
HuetReduction.BackwardDirection.N [in HOU.third_order.huet]
HuetReduction.BackwardDirection.S [in HOU.third_order.huet]
HuetReduction.BackwardDirection.s [in HOU.third_order.huet]
HuetReduction.BackwardDirection.sigma [in HOU.third_order.huet]
HuetReduction.BackwardDirection.t [in HOU.third_order.huet]
HuetReduction.BackwardDirection.x [in HOU.third_order.huet]
HuetReduction.f [in HOU.third_order.huet]
HuetReduction.g [in HOU.third_order.huet]
HuetReduction.h [in HOU.third_order.huet]
HuetReduction.u [in HOU.third_order.huet]
HuetReduction.v [in HOU.third_order.huet]
HuetReduction.X [in HOU.third_order.huet]
I
InhabitingTypes.X [in HOU.concon.conservativity]L
ListEnumerabilityOrderedSystems.enumX [in HOU.concon.enumerability]ListEnumerabilityOrderedSystems.X [in HOU.concon.enumerability]
ListEnumerabilityOrdered.enumX [in HOU.concon.enumerability]
ListEnumerabilityOrdered.X [in HOU.concon.enumerability]
ListEnumerabilitySystems.enumX [in HOU.concon.enumerability]
ListEnumerabilitySystems.X [in HOU.concon.enumerability]
ListEnumerability.enumX [in HOU.unification.enumerability]
ListEnumerability.X [in HOU.unification.enumerability]
ListRelations.R [in HOU.std.ars.list_reduction]
ListRelations.X [in HOU.std.ars.list_reduction]
M
Motivation.a [in HOU.second_order.goldfarb.motivation]Motivation.b [in HOU.second_order.goldfarb.motivation]
Motivation.m [in HOU.second_order.goldfarb.motivation]
Motivation.n [in HOU.second_order.goldfarb.motivation]
Motivation.p [in HOU.second_order.goldfarb.motivation]
Motivation.Streams.X [in HOU.second_order.goldfarb.motivation]
MPCP_U3.X [in HOU.third_order.simplified]
N
Normalisation.X [in HOU.unification.higher_order_unification]Normalisation.X [in HOU.unification.nth_order_unification]
NthOrderSystemUnification.X [in HOU.unification.nth_order_unification]
Nth.X [in HOU.std.lists.advanced]
Nth.Y [in HOU.std.lists.advanced]
P
Properties.r [in HOU.std.retracts]Properties.X [in HOU.std.retracts]
Properties.Y [in HOU.std.retracts]
R
Reductions.X [in HOU.std.reductions]Reductions.Y [in HOU.std.reductions]
Reductions.Z [in HOU.std.reductions]
RemoveConstants.consts_agree [in HOU.concon.constants]
RemoveConstants.EncodingLemmas.C [in HOU.concon.constants]
RemoveConstants.EncodingLemmas.n [in HOU.concon.constants]
RemoveConstants.EncodingLemmas.O [in HOU.concon.constants]
RemoveConstants.enc_subst [in HOU.concon.constants]
RemoveConstants.enc_ctx [in HOU.concon.constants]
RemoveConstants.enc_type [in HOU.concon.constants]
RemoveConstants.enc_term [in HOU.concon.constants]
RemoveConstants.enc_var [in HOU.concon.constants]
RemoveConstants.enc_const [in HOU.concon.constants]
RemoveConstants.inv_subst [in HOU.concon.constants]
RemoveConstants.inv_term [in HOU.concon.constants]
RemoveConstants.RE [in HOU.concon.constants]
RemoveConstants.R' [in HOU.concon.constants]
RemoveConstants.X [in HOU.concon.constants]
RemoveConstants.Y [in HOU.concon.constants]
RemoveConstants.ι [in HOU.concon.constants]
Remove.D [in HOU.std.lists.advanced]
Remove.X [in HOU.std.lists.advanced]
Repeated.X [in HOU.std.lists.advanced]
Repeated.Y [in HOU.std.lists.advanced]
Retracts.consts_agree [in HOU.concon.constants]
Retracts.inj [in HOU.concon.constants]
Retracts.re [in HOU.concon.constants]
Retracts.RE [in HOU.concon.constants]
Retracts.X [in HOU.concon.constants]
Retracts.Y [in HOU.concon.constants]
Retyping.X [in HOU.concon.retyping]
S
SemanticTyping.X [in HOU.calculus.normalisation]StrongNormalisation.A [in HOU.std.ars.normalisation]
StrongNormalisation.R [in HOU.std.ars.normalisation]
StrongNormalisation.S [in HOU.std.ars.normalisation]
StrongNormalisation.X [in HOU.std.ars.normalisation]
SubstitutionTransformations.A [in HOU.unification.higher_order_unification]
SubstitutionTransformations.A [in HOU.unification.nth_order_unification]
SubstitutionTransformations.Gamma [in HOU.unification.higher_order_unification]
SubstitutionTransformations.Gamma [in HOU.unification.nth_order_unification]
SubstitutionTransformations.Leq [in HOU.unification.higher_order_unification]
SubstitutionTransformations.Leq [in HOU.unification.nth_order_unification]
SubstitutionTransformations.n [in HOU.unification.higher_order_unification]
SubstitutionTransformations.n [in HOU.unification.nth_order_unification]
SubstitutionTransformations.s [in HOU.unification.higher_order_unification]
SubstitutionTransformations.s [in HOU.unification.nth_order_unification]
SubstitutionTransformations.t [in HOU.unification.higher_order_unification]
SubstitutionTransformations.t [in HOU.unification.nth_order_unification]
SubstitutionTransformations.T1 [in HOU.unification.higher_order_unification]
SubstitutionTransformations.T1 [in HOU.unification.nth_order_unification]
SubstitutionTransformations.T2 [in HOU.unification.higher_order_unification]
SubstitutionTransformations.T2 [in HOU.unification.nth_order_unification]
SubstitutionTransformations.X [in HOU.unification.higher_order_unification]
SubstitutionTransformations.X [in HOU.unification.nth_order_unification]
SystemUnification.X [in HOU.unification.systemunification]
T
Takahashi.R [in HOU.std.ars.confluence]Takahashi.rho [in HOU.std.ars.confluence]
Takahashi.tak [in HOU.std.ars.confluence]
Takahashi.X [in HOU.std.ars.confluence]
TMT.H1 [in HOU.std.ars.confluence]
TMT.H2 [in HOU.std.ars.confluence]
TMT.R [in HOU.std.ars.confluence]
TMT.S [in HOU.std.ars.confluence]
TMT.X [in HOU.std.ars.confluence]
Typing.E [in HOU.second_order.goldfarb.encoding]
U
Unification.free [in HOU.firstorder]Unification.isFree [in HOU.firstorder]
Unification.Soundness.Gamma [in HOU.firstorder]
Unification.Soundness.HO [in HOU.firstorder]
Unification.X [in HOU.firstorder]
Library Index
A
advancedaxioms
B
basicbasics
C
calculusconcon
confluence
confluence
conservativity
constants
countability
D
decidablediophantine_equations
E
encodingencoding
encoding
enumerability
enumerability
enumerable
equivalence
evaluator
evaluator
F
firstorderH
higher_order_unificationhuet
L
list_reductionM
miscmisc
motivation
N
normalisationnormalisation
nth_order_unification
O
orderP
pcpprelim
R
reductionreduction
reductions
retracts
retyping
S
semanticssimplified
std
syntax
systemunification
T
tacticsterms
terms_extension
typing
U
unificationunscoped
Lemma Index
A
add_subst [in HOU.second_order.dowek.encoding]add_ren [in HOU.second_order.dowek.encoding]
all_terms_app [in HOU.unification.systemunification]
all_terms_nil [in HOU.unification.systemunification]
all_terms_cons_iff [in HOU.unification.systemunification]
all_terms_cons [in HOU.unification.systemunification]
anti_ren [in HOU.calculus.semantics]
AppL_largest [in HOU.calculus.terms_extension]
AppL_ordertyping_inv [in HOU.calculus.terms_extension]
AppL_typing_inv [in HOU.calculus.terms_extension]
AppL_ordertyping_repeated [in HOU.calculus.terms_extension]
AppL_typing_repeated [in HOU.calculus.terms_extension]
AppL_subst [in HOU.calculus.terms_extension]
AppL_ren [in HOU.calculus.terms_extension]
AppL_app [in HOU.calculus.terms_extension]
AppR_ordertyping_inv [in HOU.calculus.terms_extension]
AppR_typing_inv [in HOU.calculus.terms_extension]
AppR_ordertyping [in HOU.calculus.terms_extension]
AppR_typing [in HOU.calculus.terms_extension]
AppR_Lambda' [in HOU.calculus.terms_extension]
AppR_Lambda [in HOU.calculus.terms_extension]
AppR_subst [in HOU.calculus.terms_extension]
AppR_ren [in HOU.calculus.terms_extension]
AppR_head [in HOU.calculus.terms_extension]
AppR_vars [in HOU.calculus.terms_extension]
AppR_app [in HOU.calculus.terms_extension]
app_injective_right [in HOU.std.lists.misc]
app_injective [in HOU.std.lists.misc]
app_comm [in HOU.std.lists.basics]
arity_decomposed [in HOU.calculus.terms_extension]
arity_Arr [in HOU.calculus.terms_extension]
Arr_left_injective [in HOU.calculus.terms_extension]
Arr_inversion [in HOU.calculus.terms_extension]
Arr_app [in HOU.calculus.terms_extension]
atom_head_lifting [in HOU.calculus.syntax]
atom_head [in HOU.calculus.syntax]
atom_var [in HOU.calculus.syntax]
atom_lifting [in HOU.calculus.syntax]
B
backward [in HOU.second_order.goldfarb.motivation]backward_mult [in HOU.second_order.dowek.reduction]
backward_add [in HOU.second_order.dowek.reduction]
backward_consts [in HOU.second_order.dowek.reduction]
backward_vars [in HOU.second_order.dowek.reduction]
backward_mult [in HOU.second_order.goldfarb.reduction]
backward_add [in HOU.second_order.goldfarb.reduction]
backward_consts [in HOU.second_order.goldfarb.reduction]
backward_vars [in HOU.second_order.goldfarb.reduction]
backward' [in HOU.second_order.goldfarb.motivation]
C
church_rosser [in HOU.std.ars.confluence]church_commute [in HOU.second_order.dowek.encoding]
closure_under_reduction [in HOU.calculus.normalisation]
closure_under_expansion [in HOU.calculus.normalisation]
compat_app [in HOU.calculus.normalisation]
compat_lambda [in HOU.calculus.normalisation]
compat_const [in HOU.calculus.normalisation]
compat_var [in HOU.calculus.normalisation]
compComp_exp [in HOU.calculus.terms]
compComp'_exp [in HOU.calculus.terms]
compute_evaluation_step [in HOU.calculus.evaluator]
compute_evaluation [in HOU.std.ars.evaluator]
confluence_lstep [in HOU.std.ars.list_reduction]
confluence_step [in HOU.calculus.confluence]
confluence_unique_normal_forms [in HOU.std.ars.confluence]
confluence_normal_right [in HOU.std.ars.confluence]
confluence_normal_left [in HOU.std.ars.confluence]
confluent_semi [in HOU.std.ars.confluence]
congr_app [in HOU.calculus.terms]
congr_lam [in HOU.calculus.terms]
congr_const [in HOU.calculus.terms]
congr_arr [in HOU.calculus.terms]
congr_typevar [in HOU.calculus.terms]
consts_inhab [in HOU.concon.conservativity]
consts_in_subst_consts [in HOU.concon.conservativity]
consts_AppR [in HOU.concon.conservativity]
consts_AppL [in HOU.concon.conservativity]
consts_Lam [in HOU.concon.conservativity]
consts_subst_vars [in HOU.concon.conservativity]
consts_subset_steps [in HOU.concon.conservativity]
consts_subset_step [in HOU.concon.conservativity]
consts_subst_in [in HOU.concon.conservativity]
consts_ren [in HOU.concon.conservativity]
Consts_montone [in HOU.concon.conservativity]
Consts_consts [in HOU.concon.conservativity]
const_ordertyping_list [in HOU.calculus.terms_extension]
counted_exp [in HOU.std.ars.basic]
counted_trans [in HOU.std.ars.basic]
count_nat [in HOU.std.enumerable]
count_bool [in HOU.std.enumerable]
count_enum' [in HOU.std.enumerable]
cum_ge' [in HOU.std.enumerable]
cum_ge [in HOU.std.enumerable]
C_longenough [in HOU.std.enumerable]
C_exhaustive [in HOU.std.enumerable]
D
decb_dec [in HOU.std.decidable]decode_subst_encodes [in HOU.second_order.goldfarb.reduction]
decomp_irrefl [in HOU.firstorder]
decomp_some_var [in HOU.firstorder]
decomp_none_not_unifiable [in HOU.firstorder]
decomp_lambda_free [in HOU.firstorder]
decomp_typing [in HOU.firstorder]
decomp_some_head_consts [in HOU.firstorder]
decomp_none_ind [in HOU.firstorder]
decomp_some_ind [in HOU.firstorder]
decomp'_irrefl [in HOU.firstorder]
decomp'_some_var [in HOU.firstorder]
decomp'_none_not_unifiable [in HOU.firstorder]
decomp'_lambda_free [in HOU.firstorder]
decomp'_typing [in HOU.firstorder]
decomp'_none_ind [in HOU.firstorder]
decomp'_some_ind [in HOU.firstorder]
decr_unifies [in HOU.firstorder]
decr_typing [in HOU.firstorder]
decr_lambda_free [in HOU.firstorder]
dec_enc [in HOU.second_order.goldfarb.encoding]
dec_enc_eq [in HOU.second_order.goldfarb.encoding]
dec_enc [in HOU.second_order.dowek.encoding]
dec_decb [in HOU.std.decidable]
depdecomp' [in HOU.firstorder]
diamond_ext [in HOU.std.ars.confluence]
diamond_confluent [in HOU.std.ars.confluence]
diamond_semi_confluent [in HOU.std.ars.confluence]
disjoint_F_G [in HOU.second_order.goldfarb.encoding]
dom_lt_iff [in HOU.calculus.prelim]
dom_nth [in HOU.calculus.prelim]
dom_in [in HOU.calculus.prelim]
dom_map [in HOU.calculus.prelim]
dom_length [in HOU.calculus.prelim]
Dowek [in HOU.second_order.dowek.reduction]
downcast_constants [in HOU.concon.conservativity]
downcast_constants_ordered [in HOU.concon.conservativity]
downcast_variables [in HOU.concon.conservativity]
DWK_H10 [in HOU.second_order.dowek.reduction]
E
encb_eq [in HOU.third_order.encoding]encb_subst_id [in HOU.third_order.encoding]
encb_typing [in HOU.third_order.encoding]
encodes_characeristic [in HOU.second_order.goldfarb.encoding]
enc_eq [in HOU.third_order.encoding]
Enc_subst_id [in HOU.third_order.encoding]
enc_subst_id [in HOU.third_order.encoding]
enc_concat [in HOU.third_order.encoding]
enc_app [in HOU.third_order.encoding]
enc_cons [in HOU.third_order.encoding]
enc_nil [in HOU.third_order.encoding]
Enc_typing [in HOU.third_order.encoding]
enc_typing [in HOU.third_order.encoding]
enc_sol_GT [in HOU.second_order.goldfarb.reduction]
enc_sol_encodes [in HOU.second_order.goldfarb.reduction]
enc_typing [in HOU.second_order.goldfarb.encoding]
enc_injective [in HOU.second_order.goldfarb.encoding]
enc_normal [in HOU.second_order.goldfarb.encoding]
enc_subst [in HOU.second_order.goldfarb.encoding]
enc_ren [in HOU.second_order.goldfarb.encoding]
enc_app [in HOU.second_order.goldfarb.encoding]
enc_succ [in HOU.second_order.goldfarb.encoding]
enc_zero [in HOU.second_order.goldfarb.encoding]
enc_characteristic [in HOU.second_order.dowek.encoding]
enc_equiv_injective [in HOU.second_order.dowek.encoding]
enc_injective [in HOU.second_order.dowek.encoding]
enc_mul [in HOU.second_order.dowek.encoding]
enc_mul' [in HOU.second_order.dowek.encoding]
enc_add [in HOU.second_order.dowek.encoding]
enc_add' [in HOU.second_order.dowek.encoding]
enc_eta [in HOU.second_order.dowek.encoding]
enc_succ [in HOU.second_order.dowek.encoding]
enc_zero [in HOU.second_order.dowek.encoding]
enc_app [in HOU.second_order.dowek.encoding]
enc_subst [in HOU.second_order.dowek.encoding]
enc_ren [in HOU.second_order.dowek.encoding]
enc_inv_motivation [in HOU.concon.constants]
enc_term_app [in HOU.concon.constants]
enc_subst_term_reduce [in HOU.concon.constants]
end_is_var_typed [in HOU.third_order.encoding]
end_head_var [in HOU.third_order.encoding]
end_is_var [in HOU.third_order.huet]
enumerable_red2 [in HOU.std.reductions]
enumerable_red [in HOU.std.reductions]
enumerable_unification [in HOU.unification.enumerability]
enumerable_orderedsystemunification [in HOU.concon.enumerability]
enumerable_systemunification [in HOU.concon.enumerability]
enumerable_orderdunification [in HOU.concon.enumerability]
enumerable_iff [in HOU.std.enumerable]
enumerable_conj [in HOU.std.enumerable]
enumerable_disj [in HOU.std.enumerable]
enumerable__T_list [in HOU.std.enumerable]
enumerable__T_option [in HOU.std.enumerable]
enumerable__T_sum [in HOU.std.enumerable]
enumerable__T_prod [in HOU.std.enumerable]
enumerable_enum [in HOU.std.enumerable]
enumerable_nat_nat [in HOU.std.enumerable]
enumerable_enumerable_T [in HOU.std.enumerable]
enum_red2 [in HOU.std.reductions]
enum_red [in HOU.std.reductions]
enum_unification' [in HOU.unification.enumerability]
enum_substs [in HOU.unification.enumerability]
enum_typing [in HOU.unification.enumerability]
enum_enumT [in HOU.std.enumerable]
enum_count [in HOU.std.enumerable]
enum_to_cumulative [in HOU.std.enumerable]
eqs_size_induction [in HOU.firstorder]
eqs_ordertyping_preservation_subst [in HOU.unification.nth_order_unification]
eqs_ordertyping_soundness [in HOU.unification.nth_order_unification]
eqs_ordertyping_monotone [in HOU.unification.nth_order_unification]
eqs_ordertyping_step [in HOU.unification.nth_order_unification]
eqs_typing_preservation_subst [in HOU.unification.systemunification]
equiv_head_equal [in HOU.calculus.equivalence]
equiv_huet_backward [in HOU.calculus.equivalence]
equiv_huet_forward [in HOU.calculus.equivalence]
equiv_neq_const_app [in HOU.calculus.equivalence]
equiv_neq_const_lam [in HOU.calculus.equivalence]
equiv_neq_var_const [in HOU.calculus.equivalence]
equiv_neq_var_lambda [in HOU.calculus.equivalence]
equiv_neq_lambda_app [in HOU.calculus.equivalence]
equiv_neq_var_app [in HOU.calculus.equivalence]
equiv_anti_ren [in HOU.calculus.equivalence]
equiv_app_elim [in HOU.calculus.equivalence]
equiv_lam_elim [in HOU.calculus.equivalence]
equiv_const_eq [in HOU.calculus.equivalence]
equiv_var_eq [in HOU.calculus.equivalence]
equiv_lstep_cons_inv [in HOU.std.ars.list_reduction]
equiv_join [in HOU.std.ars.basic]
equiv_reduce [in HOU.std.ars.basic]
equiv_expand [in HOU.std.ars.basic]
equiv_symm [in HOU.std.ars.basic]
equiv_trans [in HOU.std.ars.basic]
equiv_unique_normal_forms [in HOU.std.ars.confluence]
equiv_AppL_elim [in HOU.calculus.terms_extension]
equiv_AppR_elim [in HOU.calculus.terms_extension]
equiv_Lambda_elim [in HOU.calculus.terms_extension]
equiv_pointwise_eqs [in HOU.unification.systemunification]
equiv_eqs_pointwise [in HOU.unification.systemunification]
equi_unifiable_decomp' [in HOU.firstorder]
equi_unifiable_decomp [in HOU.firstorder]
equi_unifiable_cons [in HOU.firstorder]
equi_unifiable_decompose_app [in HOU.firstorder]
equi_unifiable_comm [in HOU.firstorder]
equi_unifiable_refl [in HOU.firstorder]
eq_equiv [in HOU.std.ars.basic]
eta_typing [in HOU.calculus.evaluator]
eta_normal [in HOU.calculus.evaluator]
eta_correct [in HOU.calculus.evaluator]
eta₀_typing [in HOU.calculus.evaluator]
eta₀_normal [in HOU.calculus.evaluator]
eta₀_correct [in HOU.calculus.evaluator]
evaluates_E [in HOU.std.ars.evaluator]
E_var [in HOU.calculus.normalisation]
E_evaluates [in HOU.calculus.normalisation]
E_correct_tak [in HOU.std.ars.evaluator]
E_evaluates [in HOU.std.ars.evaluator]
E_monotone [in HOU.std.ars.evaluator]
E_step [in HOU.std.ars.evaluator]
E_stops [in HOU.std.ars.evaluator]
E_unique [in HOU.std.ars.evaluator]
E_correct [in HOU.std.ars.evaluator]
E_it [in HOU.std.ars.evaluator]
E_S [in HOU.std.ars.evaluator]
F
filter_length [in HOU.std.lists.basics]find_map_inv [in HOU.std.lists.advanced]
find_map [in HOU.std.lists.advanced]
find_not_in [in HOU.std.lists.advanced]
find_Some_nth [in HOU.std.lists.advanced]
find_in [in HOU.std.lists.advanced]
find_Some [in HOU.std.lists.advanced]
finst_equivalence [in HOU.third_order.encoding]
finst_typing [in HOU.third_order.encoding]
firstorder_decidable [in HOU.firstorder]
firstorder_decidable' [in HOU.firstorder]
flat_map_in_incl [in HOU.std.lists.advanced]
flat_map_incl [in HOU.std.lists.advanced]
flat_map_app [in HOU.std.lists.advanced]
forward [in HOU.second_order.goldfarb.motivation]
forward_typing [in HOU.second_order.dowek.reduction]
forward_mult [in HOU.second_order.dowek.reduction]
forward_add [in HOU.second_order.dowek.reduction]
forward_consts [in HOU.second_order.dowek.reduction]
forward_vars [in HOU.second_order.dowek.reduction]
forward_mul2 [in HOU.second_order.goldfarb.reduction]
forward_mul1 [in HOU.second_order.goldfarb.reduction]
forward_add [in HOU.second_order.goldfarb.reduction]
forward_consts [in HOU.second_order.goldfarb.reduction]
forward_vars [in HOU.second_order.goldfarb.reduction]
FO_subst_equiv_eq [in HOU.firstorder]
Fs_in [in HOU.second_order.goldfarb.encoding]
func_typing [in HOU.second_order.goldfarb.reduction]
F_not_in_G [in HOU.second_order.goldfarb.encoding]
F_injective [in HOU.second_order.goldfarb.encoding]
G
Gamma__deq_content [in HOU.second_order.goldfarb.encoding]Gamma__deq_nth_G [in HOU.second_order.goldfarb.encoding]
Gamma__deq_nth_F [in HOU.second_order.goldfarb.encoding]
Gamma__dwk_nth [in HOU.second_order.dowek.encoding]
ginst_equivalence [in HOU.third_order.huet]
ginst_typing [in HOU.third_order.huet]
Goldfarb [in HOU.second_order.goldfarb.reduction]
Goldfarb_Huet [in HOU.concon.constants]
Goldfarb_sharp [in HOU.concon.constants]
Goldfarb_remove [in HOU.concon.constants]
Goldfarb' [in HOU.second_order.goldfarb.reduction]
Gs_in [in HOU.second_order.goldfarb.encoding]
GT_typing [in HOU.second_order.goldfarb.reduction]
GT_equiv [in HOU.second_order.goldfarb.reduction]
G_up [in HOU.calculus.normalisation]
G_cons [in HOU.calculus.normalisation]
G_id [in HOU.calculus.normalisation]
G_not_in_F [in HOU.second_order.goldfarb.encoding]
G_injective [in HOU.second_order.goldfarb.encoding]
H
head_subst [in HOU.calculus.syntax]head_preserved [in HOU.calculus.semantics]
head_atom [in HOU.calculus.semantics]
head_decompose [in HOU.calculus.terms_extension]
H10_DWK [in HOU.second_order.dowek.reduction]
H10_SU [in HOU.second_order.goldfarb.reduction]
I
iff_dec [in HOU.std.decidable]incl_select_iff [in HOU.third_order.pcp]
incl_strict_incl [in HOU.std.lists.basics]
incl_app_build [in HOU.std.lists.basics]
incl_app_project_right [in HOU.std.lists.basics]
incl_app_project_left [in HOU.std.lists.basics]
incl_distr_right [in HOU.std.lists.basics]
incl_distr_left [in HOU.std.lists.basics]
incl_filter [in HOU.std.lists.basics]
incl_cons_drop [in HOU.std.lists.basics]
incl_cons_project_r [in HOU.std.lists.basics]
incl_cons_project_l [in HOU.std.lists.basics]
incl_cons_build [in HOU.std.lists.basics]
incl_cons [in HOU.std.lists.basics]
incl_nil [in HOU.std.lists.basics]
incl_seteq [in HOU.std.lists.basics]
incl_app [in HOU.std.lists.basics]
incl_strict_incl_trans [in HOU.std.lists.basics]
incl_trans [in HOU.std.lists.basics]
incl_refl [in HOU.std.lists.basics]
incl_select [in HOU.std.lists.advanced]
incl_nats [in HOU.std.lists.advanced]
inhab_typing' [in HOU.concon.conservativity]
inhab_app [in HOU.concon.conservativity]
inhab_typing_inv [in HOU.concon.conservativity]
inhab_typing [in HOU.concon.conservativity]
inhab_ren [in HOU.concon.conservativity]
injective_upRen_exp_exp [in HOU.calculus.semantics]
injective_I__P [in HOU.std.countability]
injective_I__S [in HOU.std.countability]
inj_typing [in HOU.concon.constants]
inj_ren [in HOU.concon.constants]
instId_exp [in HOU.calculus.terms]
inv_subst_typing [in HOU.concon.constants]
inv_term_typing [in HOU.concon.constants]
in_ind [in HOU.std.lists.basics]
in_Equations [in HOU.second_order.goldfarb.encoding]
in_Gs [in HOU.second_order.goldfarb.encoding]
in_Fs [in HOU.second_order.goldfarb.encoding]
in_Equations [in HOU.second_order.dowek.encoding]
in_concat_iff [in HOU.std.enumerable]
it_up_var_sapp [in HOU.calculus.prelim]
it_up_ge [in HOU.calculus.prelim]
it_up_lt [in HOU.calculus.prelim]
it_up_spec [in HOU.calculus.prelim]
it_up_ren_ge [in HOU.calculus.prelim]
it_up_ren_lt [in HOU.calculus.prelim]
it_up_ren_spec [in HOU.calculus.prelim]
it_commute [in HOU.std.misc]
it_plus [in HOU.std.misc]
it_up_free' [in HOU.firstorder]
I__S_R__S [in HOU.std.countability]
I__P_R__P [in HOU.std.countability]
J
joinable_ext [in HOU.std.ars.confluence]L
lambda_free_normal [in HOU.firstorder]lambda_free_subst_eqs [in HOU.firstorder]
lambda_free_substitution [in HOU.firstorder]
lambda_free_not_lam [in HOU.firstorder]
lambda_free_subst [in HOU.firstorder]
lambda_free_AppR [in HOU.firstorder]
Lambda_ordertyping_inv [in HOU.calculus.terms_extension]
Lambda_typing_inv [in HOU.calculus.terms_extension]
Lambda_ordertyping [in HOU.calculus.terms_extension]
Lambda_typing [in HOU.calculus.terms_extension]
Lambda_subst [in HOU.calculus.terms_extension]
Lambda_ren [in HOU.calculus.terms_extension]
Lambda_injective [in HOU.calculus.terms_extension]
Lambda_plus [in HOU.calculus.terms_extension]
largest_lin [in HOU.second_order.goldfarb.encoding]
left_ordertyping [in HOU.unification.nth_order_unification]
left_subst_eqs [in HOU.unification.systemunification]
left_typing [in HOU.unification.systemunification]
length_nats [in HOU.std.lists.advanced]
linearize_consts [in HOU.concon.conservativity]
linearize_terms_ordertyping [in HOU.unification.nth_order_unification]
linearize_vars [in HOU.unification.systemunification]
linearize_terms_typing [in HOU.unification.systemunification]
linearize_terms_equiv [in HOU.unification.systemunification]
linearize_terms_subst [in HOU.unification.systemunification]
lin_injective [in HOU.second_order.goldfarb.encoding]
lin_subst [in HOU.second_order.goldfarb.encoding]
lin_ren [in HOU.second_order.goldfarb.encoding]
lin_typing [in HOU.second_order.goldfarb.encoding]
lin_app [in HOU.second_order.goldfarb.encoding]
lin_cons [in HOU.second_order.goldfarb.encoding]
lin_nil [in HOU.second_order.goldfarb.encoding]
listtyping_preservation_under_renaming [in HOU.calculus.terms_extension]
listtyping_app [in HOU.calculus.terms_extension]
list_equiv_ind [in HOU.std.ars.list_reduction]
list_end_ind [in HOU.std.lists.misc]
list_pointwise_eq [in HOU.std.lists.misc]
list_decompose_strong [in HOU.std.lists.misc]
list_decompose_end [in HOU.std.lists.misc]
list_decompose_alt [in HOU.std.lists.misc]
list_decompose [in HOU.std.lists.misc]
list_equiv_anti_ren [in HOU.calculus.terms_extension]
list_equiv_subst [in HOU.calculus.terms_extension]
list_equiv_ren [in HOU.calculus.terms_extension]
lsteps_cons_inv [in HOU.std.ars.list_reduction]
lsteps_nil_cons [in HOU.std.ars.list_reduction]
lsteps_cons_nil [in HOU.std.ars.list_reduction]
lstep_normal_nil [in HOU.std.ars.list_reduction]
lstep_normal_cons [in HOU.std.ars.list_reduction]
lstep_normal_cons_r [in HOU.std.ars.list_reduction]
lstep_normal_cons_l [in HOU.std.ars.list_reduction]
lstep_nil_cons [in HOU.std.ars.list_reduction]
lstep_cons_nil [in HOU.std.ars.list_reduction]
lt_nats [in HOU.std.lists.advanced]
M
map_nil [in HOU.std.lists.basics]map_id [in HOU.std.lists.basics]
map_id_list [in HOU.std.lists.basics]
map_var_typing [in HOU.calculus.terms_extension]
max_le_right [in HOU.calculus.prelim]
max_le_left [in HOU.calculus.prelim]
MPCPsimp_MPCP [in HOU.third_order.pcp]
MPCP_U [in HOU.concon.conservativity]
MPCP_U3 [in HOU.third_order.simplified]
MPCP_MPCP' [in HOU.third_order.simplified]
MPCP'_U3 [in HOU.third_order.simplified]
multiple_fixpoint [in HOU.std.ars.basic]
multiple_idem [in HOU.std.ars.basic]
multiple_star_step [in HOU.std.ars.basic]
multiple_destruct [in HOU.std.ars.basic]
multiple_trans [in HOU.std.ars.basic]
multiplication_lambdas [in HOU.second_order.goldfarb.reduction]
mul_subst [in HOU.second_order.dowek.encoding]
mul_ren [in HOU.second_order.dowek.encoding]
MU_PCP [in HOU.third_order.huet]
N
nats_incl [in HOU.std.lists.advanced]nats_lt [in HOU.std.lists.advanced]
nodup_seteq [in HOU.std.lists.basics]
normalise_subst [in HOU.unification.higher_order_unification]
normal_inhab [in HOU.concon.conservativity]
normal_in_lstep [in HOU.std.ars.list_reduction]
normal_lstep_in [in HOU.std.ars.list_reduction]
Normal_star_stops [in HOU.std.ars.basic]
normal_subst [in HOU.calculus.semantics]
normal_ren [in HOU.calculus.semantics]
normal_app_intro [in HOU.calculus.semantics]
normal_app_not_lam [in HOU.calculus.semantics]
normal_app_r [in HOU.calculus.semantics]
normal_app_l [in HOU.calculus.semantics]
normal_lam_elim [in HOU.calculus.semantics]
normal_lam_intro [in HOU.calculus.semantics]
normal_const [in HOU.calculus.semantics]
normal_var [in HOU.calculus.semantics]
normal_forms_encodes [in HOU.second_order.goldfarb.encoding]
normal_enc [in HOU.second_order.dowek.encoding]
normal_retyping [in HOU.concon.retyping]
Normal_star_stops [in HOU.std.ars.normalisation]
Normal_SN [in HOU.std.ars.normalisation]
normal_nf [in HOU.calculus.terms_extension]
normal_AppR_left [in HOU.calculus.terms_extension]
normal_AppR_right [in HOU.calculus.terms_extension]
normal_AppL_right [in HOU.calculus.terms_extension]
normal_AppL_left [in HOU.calculus.terms_extension]
normal_Lambda [in HOU.calculus.terms_extension]
not_equiv_lstep_nil_cons [in HOU.std.ars.list_reduction]
nth_error_sapp [in HOU.calculus.prelim]
nth_Gamma__deq_G [in HOU.second_order.goldfarb.encoding]
nth_Gamma__deq_F [in HOU.second_order.goldfarb.encoding]
nth_error_repeated [in HOU.std.lists.advanced]
nth_nats [in HOU.std.lists.advanced]
nth_error_Some_lt [in HOU.std.lists.advanced]
nth_error_lt_Some [in HOU.std.lists.advanced]
nth_error_map_option [in HOU.std.lists.advanced]
O
orderlisttyping_element [in HOU.calculus.terms_extension]orderlisttyping_preservation_under_substitution [in HOU.calculus.terms_extension]
orderlisttyping_preservation_under_renaming [in HOU.calculus.terms_extension]
orderlisttyping_app [in HOU.calculus.terms_extension]
ordertypingSubst_complete [in HOU.calculus.order]
ordertypingSubst_soundness [in HOU.calculus.order]
ordertypingSubst_monotone [in HOU.calculus.order]
ordertyping_weak_ordertyping [in HOU.concon.conservativity]
ordertyping_from_basetyping [in HOU.concon.conservativity]
ordertyping_preservation_consts [in HOU.concon.conservativity]
ordertyping_preservation_under_steps [in HOU.calculus.order]
ordertyping_preservation_under_reduction [in HOU.calculus.order]
ordertyping_preservation_under_substitution [in HOU.calculus.order]
ordertyping_weak_preservation_under_substitution [in HOU.calculus.order]
ordertyping_preservation_under_renaming [in HOU.calculus.order]
ordertyping_weak_preservation_under_renaming [in HOU.calculus.order]
ordertyping_completeness [in HOU.calculus.order]
ordertyping_soundness [in HOU.calculus.order]
ordertyping_monotone [in HOU.calculus.order]
ordertyping_step [in HOU.calculus.order]
ordertyping_termination_steps [in HOU.calculus.normalisation]
ordertyping_one_atom [in HOU.firstorder]
ordertyping_normalise_subst [in HOU.unification.nth_order_unification]
ordertyping_combine [in HOU.unification.nth_order_unification]
order_head [in HOU.calculus.order]
order_one_lambda_free [in HOU.firstorder]
orduni_normalise_correct [in HOU.unification.nth_order_unification]
ord_target' [in HOU.calculus.order]
ord_target [in HOU.calculus.order]
ord_arr_one [in HOU.calculus.order]
ord_arr [in HOU.calculus.order]
ord_1 [in HOU.calculus.order]
ord_Gamma__deq [in HOU.second_order.goldfarb.encoding]
ord_repeated [in HOU.calculus.terms_extension]
ord_Arr [in HOU.calculus.terms_extension]
ord'_cons [in HOU.calculus.order]
ord'_elements [in HOU.calculus.order]
ord'_in [in HOU.calculus.order]
ord'_rev [in HOU.calculus.order]
ord'_app [in HOU.calculus.order]
OU_reduction [in HOU.unification.nth_order_unification]
OU_NOU [in HOU.unification.nth_order_unification]
OU_SOU [in HOU.unification.nth_order_unification]
P
pairs_retract [in HOU.std.enumerable]partition_F_G [in HOU.second_order.goldfarb.encoding]
PCPsimp_PCP [in HOU.third_order.pcp]
PCP_U [in HOU.concon.conservativity]
PCP_U3 [in HOU.third_order.huet]
PCP_MU [in HOU.third_order.huet]
preservation_consts [in HOU.concon.conservativity]
preservation_under_steps [in HOU.calculus.typing]
preservation_under_reduction [in HOU.calculus.typing]
preservation_under_substitution [in HOU.calculus.typing]
preservation_under_renaming [in HOU.calculus.typing]
projection [in HOU.std.enumerable]
projection' [in HOU.std.enumerable]
R
redtm_typing [in HOU.third_order.simplified]reduction_neg [in HOU.std.reductions]
reduction_reflexive [in HOU.std.reductions]
reduction_transitive [in HOU.std.reductions]
red_fun_rho [in HOU.std.ars.evaluator]
red_fun_normal [in HOU.std.ars.evaluator]
red_fun_fp_it [in HOU.std.ars.evaluator]
red_fun_fp [in HOU.std.ars.evaluator]
refl_equiv [in HOU.std.ars.basic]
refl_star [in HOU.std.ars.basic]
refl_par [in HOU.calculus.confluence]
remove_constants_reduction [in HOU.concon.constants]
remove_constants_backward [in HOU.concon.constants]
remove_constants_forward [in HOU.concon.constants]
remove_constants_ordertypingSubst [in HOU.concon.constants]
remove_constants_ordertyping [in HOU.concon.constants]
remove_prev [in HOU.std.lists.advanced]
remove_remain [in HOU.std.lists.advanced]
ren_plus_combine [in HOU.calculus.prelim]
ren_comp [in HOU.calculus.prelim]
ren_plus_base [in HOU.calculus.prelim]
ren_vars [in HOU.calculus.syntax]
ren_varof [in HOU.calculus.syntax]
ren_subst_consts_commute [in HOU.concon.conservativity]
ren_equiv [in HOU.calculus.equivalence]
ren_closed_G [in HOU.calculus.normalisation]
ren_closed_E [in HOU.calculus.normalisation]
ren_closed_V [in HOU.calculus.normalisation]
ren_closed_C [in HOU.calculus.normalisation]
ren_compatible_par [in HOU.calculus.confluence]
ren_steps [in HOU.calculus.semantics]
ren_step [in HOU.calculus.semantics]
repeated_ordertyping [in HOU.calculus.terms_extension]
repeated_typing [in HOU.calculus.terms_extension]
repeated_app_inv [in HOU.std.lists.advanced]
repeated_tab [in HOU.std.lists.advanced]
repeated_incl [in HOU.std.lists.advanced]
repeated_equal [in HOU.std.lists.advanced]
repeated_length [in HOU.std.lists.advanced]
repeated_map [in HOU.std.lists.advanced]
repeated_rev [in HOU.std.lists.advanced]
repeated_plus [in HOU.std.lists.advanced]
repeated_in [in HOU.std.lists.advanced]
retract_injective [in HOU.std.retracts]
retype_iff [in HOU.concon.retyping]
retype_Arr [in HOU.concon.retyping]
retype_type_id [in HOU.concon.retyping]
retype_type_ord [in HOU.concon.retyping]
retype_ctx_ord [in HOU.concon.retyping]
rev_seteq [in HOU.std.lists.basics]
re_typing [in HOU.concon.constants]
re_ren [in HOU.concon.constants]
rho_evaluates [in HOU.std.ars.evaluator]
right_ordertyping [in HOU.unification.nth_order_unification]
right_subst_eqs [in HOU.unification.systemunification]
right_typing [in HOU.unification.systemunification]
rinstInst_exp [in HOU.calculus.terms]
R__S_I__S [in HOU.std.countability]
R__P_injective [in HOU.std.countability]
R__P_I__P [in HOU.std.countability]
S
sandwich_confluent [in HOU.std.ars.confluence]sandwich_equiv [in HOU.std.ars.confluence]
sapp_ge_in [in HOU.calculus.prelim]
sapp_lt_in [in HOU.calculus.prelim]
sapp_app [in HOU.calculus.prelim]
scons_comp [in HOU.unscoped]
scons_eta_id [in HOU.unscoped]
scons_eta [in HOU.unscoped]
select_variables_subst [in HOU.calculus.prelim]
select_map [in HOU.std.lists.advanced]
select_incl [in HOU.std.lists.advanced]
select_repeated [in HOU.std.lists.advanced]
select_nats [in HOU.std.lists.advanced]
select_S [in HOU.std.lists.advanced]
select_nil [in HOU.std.lists.advanced]
semantic_soundness [in HOU.calculus.normalisation]
seteq_incl_right [in HOU.std.lists.basics]
seteq_incl_left [in HOU.std.lists.basics]
seteq_sym [in HOU.std.lists.basics]
seteq_trans [in HOU.std.lists.basics]
seteq_refl [in HOU.std.lists.basics]
singlepoint_subst_Vars'_variable [in HOU.firstorder]
singlepoint_subst_Vars' [in HOU.firstorder]
singlepoint_subst_vars_variable [in HOU.firstorder]
singlepoint_subst_vars [in HOU.firstorder]
size_subst [in HOU.firstorder]
size_ren [in HOU.firstorder]
SN_finite_steps [in HOU.std.ars.normalisation]
SN_morphism [in HOU.std.ars.normalisation]
SN_multiple [in HOU.std.ars.normalisation]
SN_unfold [in HOU.std.ars.normalisation]
SN_ext [in HOU.std.ars.normalisation]
SOU_NSOU [in HOU.unification.nth_order_unification]
SOU_OU [in HOU.unification.nth_order_unification]
star_starL [in HOU.std.ars.basic]
star_absorbtion [in HOU.std.ars.basic]
star_idem [in HOU.std.ars.basic]
star_closure [in HOU.std.ars.basic]
star_trans [in HOU.std.ars.basic]
steps_u_mult [in HOU.second_order.goldfarb.reduction]
steps_u [in HOU.second_order.goldfarb.reduction]
steps_anti_ren [in HOU.calculus.semantics]
steps_app_atom [in HOU.calculus.semantics]
steps_app [in HOU.calculus.semantics]
steps_lam [in HOU.calculus.semantics]
step_star_multiple [in HOU.std.ars.basic]
step_u [in HOU.second_order.goldfarb.reduction]
step_anti_ren [in HOU.calculus.semantics]
strict_incl_project [in HOU.std.lists.basics]
strict_incl_eq [in HOU.std.lists.basics]
strict_incl_incl [in HOU.std.lists.basics]
strict_incl_incl_trans [in HOU.std.lists.basics]
strict_incl_trans [in HOU.std.lists.basics]
subrel_unfold [in HOU.std.ars.basic]
subst_vars [in HOU.calculus.syntax]
subst_varof [in HOU.calculus.syntax]
subst_extensional [in HOU.calculus.syntax]
subst_consts_AppR [in HOU.concon.conservativity]
subst_consts_AppL [in HOU.concon.conservativity]
subst_consts_Lambda [in HOU.concon.conservativity]
subst_const_comm_id [in HOU.concon.conservativity]
subst_consts_up [in HOU.concon.conservativity]
subst_consts_consts [in HOU.concon.conservativity]
subst_const_comm [in HOU.concon.conservativity]
subst_consts_ident [in HOU.concon.conservativity]
subst_consts_comp [in HOU.concon.conservativity]
subst_pointwise_equiv [in HOU.calculus.equivalence]
subst_equiv [in HOU.calculus.equivalence]
subst_compatible_par [in HOU.calculus.confluence]
subst_T [in HOU.second_order.goldfarb.reduction]
subst_enc_step [in HOU.second_order.goldfarb.reduction]
subst_var_b [in HOU.second_order.goldfarb.reduction]
subst_var_a [in HOU.second_order.goldfarb.reduction]
subst_var [in HOU.second_order.goldfarb.reduction]
subst_steps [in HOU.calculus.semantics]
subst_step [in HOU.calculus.semantics]
subst_consts_subst [in HOU.concon.constants]
subst_consts_inject_backwards [in HOU.concon.constants]
subst_consts_inject_forward [in HOU.concon.constants]
sub_sol_enc [in HOU.second_order.dowek.reduction]
Sum_app [in HOU.std.misc]
Sum_in [in HOU.std.misc]
SU_conservative_backward [in HOU.concon.conservativity]
SU_conservative_forward [in HOU.concon.conservativity]
SU_monotone_backward [in HOU.concon.conservativity]
SU_monotone_forward [in HOU.concon.conservativity]
SU_H10 [in HOU.second_order.goldfarb.reduction]
SU_SNU [in HOU.unification.systemunification]
SU_U [in HOU.unification.systemunification]
sym_symmetric [in HOU.std.ars.basic]
systemunification_conserve [in HOU.concon.conservativity]
systemunification_steps [in HOU.concon.conservativity]
systemunification_step [in HOU.concon.conservativity]
T
tab_typing [in HOU.second_order.goldfarb.reduction]tab_subst [in HOU.calculus.terms_extension]
tab_nth [in HOU.std.lists.advanced]
tab_id_nats [in HOU.std.lists.advanced]
tab_map_nats [in HOU.std.lists.advanced]
tab_plus [in HOU.std.lists.advanced]
tab_S [in HOU.std.lists.advanced]
tab_map [in HOU.std.lists.advanced]
tab_length [in HOU.std.lists.advanced]
tak_fun_rho [in HOU.calculus.confluence]
tak_cofinal [in HOU.std.ars.confluence]
tak_mono_n [in HOU.std.ars.confluence]
tak_mono [in HOU.std.ars.confluence]
tak_sound [in HOU.std.ars.confluence]
tak_diamond [in HOU.std.ars.confluence]
target_Arr [in HOU.calculus.terms_extension]
target_ord [in HOU.calculus.terms_extension]
termination_steps [in HOU.calculus.normalisation]
tight_retr [in HOU.std.retracts]
tight_is_tight [in HOU.std.retracts]
TMT [in HOU.std.ars.confluence]
type_decompose [in HOU.calculus.terms_extension]
typingSubst_cons [in HOU.calculus.typing]
typing_Consts [in HOU.concon.conservativity]
typing_constants [in HOU.concon.conservativity]
typing_forward [in HOU.second_order.goldfarb.reduction]
typing_equations [in HOU.second_order.goldfarb.encoding]
typing_mul2 [in HOU.second_order.goldfarb.encoding]
typing_mul1 [in HOU.second_order.goldfarb.encoding]
typing_add [in HOU.second_order.goldfarb.encoding]
typing_const [in HOU.second_order.goldfarb.encoding]
typing_var_eq [in HOU.second_order.goldfarb.encoding]
typing_G [in HOU.second_order.goldfarb.encoding]
typing_F [in HOU.second_order.goldfarb.encoding]
typing_g [in HOU.second_order.goldfarb.encoding]
typing_b [in HOU.second_order.goldfarb.encoding]
typing_a [in HOU.second_order.goldfarb.encoding]
typing_equations [in HOU.second_order.dowek.encoding]
typing_mulEQ [in HOU.second_order.dowek.encoding]
typing_addEQ [in HOU.second_order.dowek.encoding]
typing_constEQ [in HOU.second_order.dowek.encoding]
typing_varEQ [in HOU.second_order.dowek.encoding]
typing_enc [in HOU.second_order.dowek.encoding]
typing_variables [in HOU.calculus.typing]
typing_combine [in HOU.unification.systemunification]
T_step_tau2_sigma2 [in HOU.second_order.goldfarb.reduction]
T_step_tau1_sigma1 [in HOU.second_order.goldfarb.reduction]
T_list_el [in HOU.std.enumerable]
T_list_cum [in HOU.std.enumerable]
T_prod_el [in HOU.std.enumerable]
T_prod_cum [in HOU.std.enumerable]
T_nat_length [in HOU.std.enumerable]
T_nat_in [in HOU.std.enumerable]
U
unification_conserve [in HOU.concon.conservativity]unification_steps [in HOU.concon.conservativity]
unification_step [in HOU.concon.conservativity]
unification_conservative_backward [in HOU.concon.conservativity]
unification_conservative_forward [in HOU.concon.conservativity]
unification_monotone_backward [in HOU.concon.conservativity]
unification_monotone_forward [in HOU.concon.conservativity]
unification_downcast_eqs [in HOU.concon.conservativity]
unification_downcast [in HOU.concon.conservativity]
unification_constants_monotone [in HOU.concon.constants]
unification_retract_backward [in HOU.concon.constants]
unification_retract_forward [in HOU.concon.constants]
unifies_free_all [in HOU.firstorder]
unifies_free [in HOU.firstorder]
unifies_not_var [in HOU.firstorder]
Unifies_app [in HOU.firstorder]
Unifies_nil [in HOU.firstorder]
Unifies_cons [in HOU.firstorder]
unifiy_computable [in HOU.firstorder]
unify_complete [in HOU.firstorder]
unify_typing [in HOU.firstorder]
unify_free' [in HOU.firstorder]
unify_unifiable [in HOU.firstorder]
unify_lambda_free [in HOU.firstorder]
unif_correct [in HOU.firstorder]
uni_normalise_correct [in HOU.unification.higher_order_unification]
update_typing [in HOU.firstorder]
update_irrelevant [in HOU.firstorder]
up_ren_ren [in HOU.unscoped]
U_reduction [in HOU.unification.higher_order_unification]
U_NU [in HOU.unification.higher_order_unification]
U_NU [in HOU.unification.nth_order_unification]
U_SU [in HOU.unification.systemunification]
U3_MPCP' [in HOU.third_order.simplified]
V
varL_exp [in HOU.calculus.terms]varof_subst [in HOU.calculus.syntax]
varof_ren [in HOU.calculus.syntax]
varof_vars [in HOU.calculus.syntax]
vars_subst [in HOU.calculus.syntax]
vars_ren [in HOU.calculus.syntax]
vars_varof [in HOU.calculus.syntax]
vars_subst_consts [in HOU.concon.conservativity]
vars_ordertyping_nth [in HOU.calculus.order]
vars_ordertyping [in HOU.calculus.order]
Vars__de_in [in HOU.second_order.diophantine_equations]
Vars_decomp' [in HOU.firstorder]
vars_decomp [in HOU.firstorder]
Vars_listordertyping [in HOU.calculus.terms_extension]
Vars_listtyping [in HOU.calculus.terms_extension]
Vars'_app [in HOU.unification.systemunification]
Vars'_cons [in HOU.unification.systemunification]
var_head [in HOU.calculus.syntax]
var_typing [in HOU.calculus.terms_extension]
W
weakening_ordertyping_app [in HOU.calculus.order]weakening_app [in HOU.calculus.typing]
wf_strict_incl [in HOU.std.lists.basics]
X
xi_monotone [in HOU.calculus.evaluator]xi_correct [in HOU.calculus.evaluator]
X_unique [in HOU.second_order.goldfarb.motivation]
X_satisfies [in HOU.second_order.goldfarb.motivation]
Constructor Index
A
Add [in HOU.second_order.diophantine_equations]app [in HOU.calculus.terms]
arr [in HOU.calculus.terms]
C
Con [in HOU.second_order.diophantine_equations]const [in HOU.calculus.terms]
countedRefl [in HOU.std.ars.basic]
countedStep [in HOU.std.ars.basic]
D
dec [in HOU.std.decidable]dec1 [in HOU.std.decidable]
dec2 [in HOU.std.decidable]
diagB [in HOU.std.countability]
diagC [in HOU.std.countability]
diagS [in HOU.std.countability]
E
eqs_ordertyping_cons [in HOU.unification.nth_order_unification]eqs_ordertyping_nil [in HOU.unification.nth_order_unification]
eqs_typing_cons [in HOU.unification.systemunification]
eqs_typing_nil [in HOU.unification.systemunification]
eq_dec [in HOU.std.decidable]
L
lam [in HOU.calculus.terms]lambda_free_app [in HOU.firstorder]
lambda_free_const [in HOU.firstorder]
lambda_free_var [in HOU.firstorder]
listtyping_cons [in HOU.calculus.terms_extension]
listtyping_nil [in HOU.calculus.terms_extension]
M
Mul [in HOU.second_order.diophantine_equations]multipleSingle [in HOU.std.ars.basic]
multipleStep [in HOU.std.ars.basic]
N
nfc [in HOU.calculus.terms_extension]O
orderlisttyping_cons [in HOU.calculus.terms_extension]orderlisttyping_nil [in HOU.calculus.terms_extension]
ordertypingApp [in HOU.calculus.order]
ordertypingConst [in HOU.calculus.order]
ordertypingLam [in HOU.calculus.order]
ordertypingVar [in HOU.calculus.order]
P
parApp [in HOU.calculus.confluence]parBeta [in HOU.calculus.confluence]
parConst [in HOU.calculus.confluence]
parLam [in HOU.calculus.confluence]
parVar [in HOU.calculus.confluence]
S
SNC [in HOU.std.ars.normalisation]solA [in HOU.second_order.diophantine_equations]
solC [in HOU.second_order.diophantine_equations]
solM [in HOU.second_order.diophantine_equations]
starRefl [in HOU.std.ars.basic]
starReflL [in HOU.std.ars.basic]
starStep [in HOU.std.ars.basic]
starStepL [in HOU.std.ars.basic]
stepAppL [in HOU.calculus.semantics]
stepAppR [in HOU.calculus.semantics]
stepBeta [in HOU.calculus.semantics]
stepHead [in HOU.std.ars.list_reduction]
stepLam [in HOU.calculus.semantics]
stepTail [in HOU.std.ars.list_reduction]
symId [in HOU.std.ars.basic]
symInv [in HOU.std.ars.basic]
T
typevar [in HOU.calculus.terms]typingApp [in HOU.calculus.typing]
typingConst [in HOU.calculus.typing]
typingLam [in HOU.calculus.typing]
typingVar [in HOU.calculus.typing]
U
unifyId [in HOU.firstorder]unifyStep [in HOU.firstorder]
V
varofAppL [in HOU.calculus.syntax]varofAppR [in HOU.calculus.syntax]
varofLambda [in HOU.calculus.syntax]
varofVar [in HOU.calculus.syntax]
var_exp [in HOU.calculus.terms]
Projection Index
A
Aᵤ [in HOU.unification.higher_order_unification]A₀ [in HOU.unification.nth_order_unification]
C
const_dis [in HOU.calculus.terms]const_type [in HOU.calculus.terms]
ctype [in HOU.calculus.terms]
cum_T [in HOU.std.enumerable]
D
dec [in HOU.std.decidable]dec1 [in HOU.std.decidable]
dec2 [in HOU.std.decidable]
E
el_T [in HOU.std.enumerable]eq_dec [in HOU.std.decidable]
Eᵤ' [in HOU.unification.systemunification]
E₀' [in HOU.unification.nth_order_unification]
G
Gammaᵤ [in HOU.unification.higher_order_unification]Gammaᵤ' [in HOU.unification.systemunification]
Gamma₀ [in HOU.unification.nth_order_unification]
Gamma₀' [in HOU.unification.nth_order_unification]
H
H1ᵤ [in HOU.unification.higher_order_unification]H1₀ [in HOU.unification.nth_order_unification]
H2ᵤ [in HOU.unification.higher_order_unification]
H2₀ [in HOU.unification.nth_order_unification]
Hᵤ' [in HOU.unification.systemunification]
H₀' [in HOU.unification.nth_order_unification]
I
I [in HOU.std.retracts]L
L_T [in HOU.std.enumerable]Lᵤ' [in HOU.unification.systemunification]
L₀' [in HOU.unification.nth_order_unification]
R
R [in HOU.std.retracts]retr [in HOU.std.retracts]
S
sᵤ [in HOU.unification.higher_order_unification]s₀ [in HOU.unification.nth_order_unification]
T
tᵤ [in HOU.unification.higher_order_unification]t₀ [in HOU.unification.nth_order_unification]
Inductive Index
C
counted [in HOU.std.ars.basic]D
Dec [in HOU.std.decidable]Dec1 [in HOU.std.decidable]
Dec2 [in HOU.std.decidable]
deq [in HOU.second_order.diophantine_equations]
diag [in HOU.std.countability]
Dis [in HOU.std.decidable]
E
eqs_ordertyping [in HOU.unification.nth_order_unification]eqs_typing [in HOU.unification.systemunification]
exp [in HOU.calculus.terms]
L
lambda_free [in HOU.firstorder]listtyping [in HOU.calculus.terms_extension]
lstep [in HOU.std.ars.list_reduction]
M
multiple [in HOU.std.ars.basic]N
nf [in HOU.calculus.terms_extension]O
orderlisttyping [in HOU.calculus.terms_extension]ordertyping [in HOU.calculus.order]
P
par [in HOU.calculus.confluence]S
SN [in HOU.std.ars.normalisation]sol [in HOU.second_order.diophantine_equations]
star [in HOU.std.ars.basic]
starL [in HOU.std.ars.basic]
step [in HOU.calculus.semantics]
sym [in HOU.std.ars.basic]
T
type [in HOU.calculus.terms]typing [in HOU.calculus.typing]
U
unify [in HOU.firstorder]V
varof [in HOU.calculus.syntax]Instance Index
A
AppL_proper [in HOU.calculus.terms_extension]AppL_lstep_proper [in HOU.calculus.terms_extension]
AppL_step_proper [in HOU.calculus.terms_extension]
AppR_proper [in HOU.calculus.terms_extension]
AppR_lstep_proper [in HOU.calculus.terms_extension]
AppR_step_proper [in HOU.calculus.terms_extension]
app_proper [in HOU.calculus.semantics]
C
Const_dis [in HOU.calculus.syntax]D
decidable_E [in HOU.std.ars.evaluator]dec_varof [in HOU.calculus.syntax]
dec_normal [in HOU.calculus.semantics]
dec_free [in HOU.firstorder]
dec_all [in HOU.std.decidable]
dec_neg [in HOU.std.decidable]
dec_iff [in HOU.std.decidable]
dec_imp [in HOU.std.decidable]
dec_disj [in HOU.std.decidable]
dec_conj [in HOU.std.decidable]
dec1_neg [in HOU.std.decidable]
dec1_iff [in HOU.std.decidable]
dec1_imp [in HOU.std.decidable]
dec1_disj [in HOU.std.decidable]
dec1_conj [in HOU.std.decidable]
dec1_dec [in HOU.std.decidable]
dec2_neg [in HOU.std.decidable]
dec2_iff [in HOU.std.decidable]
dec2_imp [in HOU.std.decidable]
dec2_disj [in HOU.std.decidable]
dec2_conj [in HOU.std.decidable]
dec2_dec1' [in HOU.std.decidable]
dec2_dec1 [in HOU.std.decidable]
discrete_list [in HOU.std.decidable]
discrete_prod [in HOU.std.decidable]
discrete_sum [in HOU.std.decidable]
discrete_option [in HOU.std.decidable]
discrete_bool [in HOU.std.decidable]
discrete_nat [in HOU.std.decidable]
discrete_unit [in HOU.std.decidable]
discrete_False [in HOU.std.decidable]
dis_retract [in HOU.std.retracts]
dis_dec [in HOU.std.decidable]
E
enc_equiv [in HOU.second_order.goldfarb.encoding]enc_proper [in HOU.concon.constants]
enumerable_list [in HOU.std.enumerable]
enumT_uni [in HOU.unification.enumerability]
enumT_typing [in HOU.unification.enumerability]
enumT_type [in HOU.unification.enumerability]
enumT_exp [in HOU.unification.enumerability]
enumT_ordsys [in HOU.concon.enumerability]
enumT_sys [in HOU.concon.enumerability]
enumT_orduni [in HOU.concon.enumerability]
enumT_ordertyping [in HOU.concon.enumerability]
enumT_le [in HOU.concon.enumerability]
enumT_sig_le [in HOU.concon.enumerability]
enumT_nat [in HOU.std.enumerable]
enum_bool [in HOU.std.enumerable]
equiv_subst_consts [in HOU.concon.conservativity]
equiv_app_proper [in HOU.calculus.equivalence]
equiv_lam_proper [in HOU.calculus.equivalence]
equiv_lstep_cons_proper [in HOU.std.ars.list_reduction]
equiv_equivalence [in HOU.std.ars.basic]
equiv_rel [in HOU.std.ars.basic]
equiv_star [in HOU.std.ars.basic]
equiv_AppR_proper [in HOU.calculus.terms_extension]
equiv_AppL_proper [in HOU.calculus.terms_extension]
equi_unifiable_app [in HOU.firstorder]
equi_unifiable_equivalence [in HOU.firstorder]
eval_subrel [in HOU.std.ars.basic]
exp_dis [in HOU.calculus.syntax]
F
filter_seqteq_proper [in HOU.std.lists.basics]filter_incl_proper [in HOU.std.lists.basics]
G
ge_dec [in HOU.std.decidable]gt_dec [in HOU.std.decidable]
H
H10_to_SOU [in HOU.second_order.goldfarb.encoding]H10_to_DWK [in HOU.second_order.dowek.encoding]
I
incl_cons_proper [in HOU.std.lists.basics]incl_seteq_proper [in HOU.std.lists.basics]
incl_preorder [in HOU.std.lists.basics]
inv_proper [in HOU.concon.constants]
in_seteq_proper [in HOU.std.lists.basics]
In_dec [in HOU.std.decidable]
L
Lambda_equiv_proper [in HOU.calculus.terms_extension]Lambda_steps_proper [in HOU.calculus.terms_extension]
Lambda_step_proper [in HOU.calculus.terms_extension]
lam_proper [in HOU.calculus.semantics]
le_dec [in HOU.std.decidable]
list_subst_proper [in HOU.calculus.terms_extension]
list_ren_proper [in HOU.calculus.terms_extension]
lsteps_cons [in HOU.std.ars.list_reduction]
lt_le_subrel [in HOU.std.misc]
lt_dec [in HOU.std.decidable]
M
map_seteq_proper [in HOU.std.lists.basics]map_incl_proper [in HOU.std.lists.basics]
max_proper [in HOU.std.misc]
MPCP'_to_U [in HOU.third_order.simplified]
multiple_mono [in HOU.std.ars.basic]
multiple_star [in HOU.std.ars.basic]
multiple_exp [in HOU.std.ars.basic]
multiple_transitive [in HOU.std.ars.basic]
O
ordsysuni_orduni [in HOU.unification.nth_order_unification]orduni_normalise [in HOU.unification.nth_order_unification]
orduni_ordsysuni [in HOU.unification.nth_order_unification]
P
par_app_proper [in HOU.calculus.confluence]par_lam_proper [in HOU.calculus.confluence]
PCP_to_U [in HOU.third_order.huet]
plus_proper [in HOU.std.misc]
prod_enumerable [in HOU.std.enumerable]
proper_rev_seteq [in HOU.std.lists.basics]
proper_rev_incl [in HOU.std.lists.basics]
proper_incl_seteq [in HOU.std.lists.basics]
proper_app_seteq [in HOU.std.lists.basics]
proper_app_incl [in HOU.std.lists.basics]
proper_in_incl [in HOU.std.lists.basics]
R
refl_par_inst [in HOU.calculus.confluence]remove_constants [in HOU.concon.constants]
ren_equiv_proper [in HOU.calculus.equivalence]
ren_steps_proper [in HOU.calculus.semantics]
ren_step_proper [in HOU.calculus.semantics]
retract_False [in HOU.std.retracts]
retract_trans [in HOU.std.retracts]
retract_refl [in HOU.std.retracts]
retype [in HOU.concon.retyping]
RE_cfree [in HOU.concon.constants]
RE_abg_gonly [in HOU.concon.constants]
S
sandwich_steps [in HOU.calculus.confluence]sandwich_step [in HOU.calculus.confluence]
seteq_cons_proper [in HOU.std.lists.basics]
seteq_equivalence [in HOU.std.lists.basics]
seteq_preorder [in HOU.std.lists.basics]
star_mono [in HOU.std.ars.basic]
star_exp [in HOU.std.ars.basic]
star_preorder [in HOU.std.ars.basic]
steps_subst_consts [in HOU.concon.conservativity]
step_subst_consts [in HOU.concon.conservativity]
strict_incl_incl_subrel [in HOU.std.lists.basics]
strict_incl_transitive [in HOU.std.lists.basics]
subrel_incl_seteq [in HOU.std.lists.basics]
subst_equiv_proper [in HOU.calculus.equivalence]
subst_steps_proper [in HOU.calculus.semantics]
subst_step_proper [in HOU.calculus.semantics]
SU_conservative [in HOU.concon.conservativity]
SU_monotone [in HOU.concon.conservativity]
sym_Symmetric [in HOU.std.ars.basic]
sysuni_uni [in HOU.unification.systemunification]
T
type_dis [in HOU.calculus.syntax]U
unification_conservative [in HOU.concon.conservativity]unification_monotone [in HOU.concon.conservativity]
unification_retract [in HOU.concon.constants]
unifies_equiv [in HOU.firstorder]
uni_normalise [in HOU.unification.higher_order_unification]
uni_sysuni [in HOU.unification.systemunification]
W
wf_subvars [in HOU.firstorder]Section Index
A
ApplicativeHead [in HOU.calculus.syntax]Atoms [in HOU.calculus.syntax]
B
Backward [in HOU.second_order.dowek.reduction]Backward [in HOU.second_order.goldfarb.reduction]
BasicLemmas [in HOU.std.lists.basics]
BasicLemmas.WellFoundedStrictInclusion [in HOU.std.lists.basics]
C
Choice [in HOU.std.enumerable]ChurchEncoding [in HOU.second_order.dowek.encoding]
ChurchEncoding.Substitution [in HOU.second_order.dowek.encoding]
ClosureRelations [in HOU.std.ars.basic]
Confluence [in HOU.calculus.confluence]
Confluence [in HOU.std.ars.confluence]
Conservativity [in HOU.concon.conservativity]
Conservativity.DowncastLemmas [in HOU.concon.conservativity]
Constants [in HOU.concon.conservativity]
Constants.ConstantsOfTerm [in HOU.concon.conservativity]
Constants.ConstantSubstitution [in HOU.concon.conservativity]
D
DecBool [in HOU.std.decidable]DiscreteTypes [in HOU.calculus.syntax]
E
Encoding [in HOU.third_order.encoding]Encoding [in HOU.second_order.goldfarb.encoding]
Encoding [in HOU.second_order.dowek.encoding]
Encoding.Injectivity [in HOU.third_order.encoding]
Encoding.Reduction [in HOU.third_order.encoding]
Encoding.Substitution [in HOU.third_order.encoding]
Encoding.Typing [in HOU.third_order.encoding]
Encoding.Typing [in HOU.second_order.dowek.encoding]
enumerable_list.fixL [in HOU.std.enumerable]
enumerable_list [in HOU.std.enumerable]
enumerable_prod.fixLs [in HOU.std.enumerable]
enumerable_prod [in HOU.std.enumerable]
enumerable_enum [in HOU.std.enumerable]
enum_red2 [in HOU.std.reductions]
enum_red [in HOU.std.reductions]
enum_enumerable [in HOU.std.enumerable]
EquationEquivalences [in HOU.second_order.dowek.reduction]
EquationEquivalences [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Addition [in HOU.second_order.dowek.reduction]
EquationEquivalences.Addition [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Constants [in HOU.second_order.dowek.reduction]
EquationEquivalences.Constants [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication [in HOU.second_order.dowek.reduction]
EquationEquivalences.Multiplication [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationBackward [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Multiplication.MultiplicationForward [in HOU.second_order.goldfarb.reduction]
EquationEquivalences.Variables [in HOU.second_order.dowek.reduction]
EquationEquivalences.Variables [in HOU.second_order.goldfarb.reduction]
Equations [in HOU.second_order.goldfarb.encoding]
Equivalence [in HOU.calculus.equivalence]
EquivalenceInversion [in HOU.third_order.encoding]
Equivalence.CompatibilityProperties [in HOU.calculus.equivalence]
Equivalence.DisjointnessProperties [in HOU.calculus.equivalence]
Equivalence.HuetDefinition [in HOU.calculus.equivalence]
Equivalence.InjectivityProperties [in HOU.calculus.equivalence]
Evaluator [in HOU.calculus.evaluator]
Evaluator [in HOU.std.ars.evaluator]
EvaluatorTakahashi [in HOU.std.ars.evaluator]
Evaluator.Correctness [in HOU.calculus.evaluator]
F
Find [in HOU.std.lists.advanced]FirstOrderDecidable [in HOU.firstorder]
FlatMap [in HOU.std.lists.advanced]
Forward [in HOU.second_order.dowek.reduction]
Forward [in HOU.second_order.goldfarb.reduction]
FreeVariables [in HOU.calculus.syntax]
H
HuetReduction [in HOU.third_order.huet]HuetReduction.BackwardDirection [in HOU.third_order.huet]
HuetReduction.ForwardDirection [in HOU.third_order.huet]
I
InhabitingTypes [in HOU.concon.conservativity]L
LambdaFreeness [in HOU.firstorder]Linearization [in HOU.second_order.goldfarb.encoding]
ListEnumerability [in HOU.unification.enumerability]
ListEnumerabilityOrdered [in HOU.concon.enumerability]
ListEnumerabilityOrderedSystems [in HOU.concon.enumerability]
ListEnumerabilitySystems [in HOU.concon.enumerability]
ListRelations [in HOU.std.ars.list_reduction]
M
Motivation [in HOU.second_order.goldfarb.motivation]Motivation.FiniteSequences [in HOU.second_order.goldfarb.motivation]
Motivation.Streams [in HOU.second_order.goldfarb.motivation]
MPCP_U3 [in HOU.third_order.simplified]
N
Nats [in HOU.std.lists.advanced]Normalisation [in HOU.unification.higher_order_unification]
Normalisation [in HOU.unification.nth_order_unification]
Nth [in HOU.std.lists.advanced]
NthOrderSystemUnification [in HOU.unification.nth_order_unification]
NthOrderUnificationDefinition [in HOU.unification.nth_order_unification]
O
OrderTyping [in HOU.calculus.order]OrderTyping.Order [in HOU.calculus.order]
OrderTyping.PreservationOrdertyping [in HOU.calculus.order]
P
PCPEquivalence [in HOU.third_order.pcp]Properties [in HOU.std.retracts]
R
ReductionEncodings [in HOU.third_order.encoding]Reductions [in HOU.std.reductions]
Remove [in HOU.std.lists.advanced]
RemoveConstants [in HOU.concon.constants]
RemoveConstants.EncodingLemmas [in HOU.concon.constants]
Repeated [in HOU.std.lists.advanced]
Retracts [in HOU.concon.constants]
Retyping [in HOU.concon.retyping]
S
Select [in HOU.std.lists.advanced]Semantics [in HOU.calculus.semantics]
Semantics.CompatibilityProperties [in HOU.calculus.semantics]
Semantics.InversionLemmas [in HOU.calculus.semantics]
Semantics.Normality [in HOU.calculus.semantics]
SemanticTyping [in HOU.calculus.normalisation]
Soundness [in HOU.calculus.normalisation]
StrongNormalisation [in HOU.std.ars.normalisation]
SubstitutionTransformations [in HOU.unification.higher_order_unification]
SubstitutionTransformations [in HOU.unification.nth_order_unification]
SystemUnification [in HOU.unification.systemunification]
T
Tabulate [in HOU.std.lists.advanced]Takahashi [in HOU.std.ars.confluence]
Terms [in HOU.calculus.terms]
TermsExtension [in HOU.calculus.terms_extension]
TermsExtension.ArrowProperties [in HOU.calculus.terms_extension]
TermsExtension.EquivalenceInversions [in HOU.calculus.terms_extension]
TermsExtension.ListOperatorsCompatibilityProperties [in HOU.calculus.terms_extension]
TermsExtension.ListOperatorsSubstitutionRenaming [in HOU.calculus.terms_extension]
TermsExtension.ListOperatorsTyping [in HOU.calculus.terms_extension]
TermsExtension.ListSemanticProperties [in HOU.calculus.terms_extension]
TermsExtension.ListTypingProperties [in HOU.calculus.terms_extension]
TermsExtension.Normality [in HOU.calculus.terms_extension]
TermsExtension.Utilities [in HOU.calculus.terms_extension]
TMT [in HOU.std.ars.confluence]
TypeFunctions [in HOU.calculus.syntax]
Typing [in HOU.second_order.goldfarb.encoding]
Typing [in HOU.calculus.typing]
Typing.Preservation [in HOU.calculus.typing]
U
Unification [in HOU.firstorder]UnificationDefinitions [in HOU.unification.higher_order_unification]
Unification.Completeness [in HOU.firstorder]
Unification.Computability [in HOU.firstorder]
Unification.Decomposition [in HOU.firstorder]
Unification.Equations [in HOU.firstorder]
Unification.Soundness [in HOU.firstorder]
Unification.Unifiability [in HOU.firstorder]
Update [in HOU.firstorder]
V
Variables [in HOU.second_order.goldfarb.encoding]Abbreviation Index
A
a [in HOU.second_order.goldfarb.encoding]B
b [in HOU.second_order.goldfarb.encoding]C
card [in HOU.third_order.pcp]E
Enc [in HOU.third_order.encoding]Enc [in HOU.third_order.encoding]
Eqs [in HOU.second_order.goldfarb.encoding]
Eqs [in HOU.second_order.goldfarb.encoding]
Eqs [in HOU.second_order.dowek.encoding]
Eqs [in HOU.second_order.dowek.encoding]
G
g [in HOU.second_order.goldfarb.encoding]H
hd [in HOU.third_order.pcp]heads [in HOU.third_order.pcp]
N
normal [in HOU.calculus.semantics]normal [in HOU.calculus.semantics]
nth [in HOU.std.lists.advanced]
R
ren [in HOU.calculus.prelim]renL [in HOU.calculus.terms_extension]
S
stack [in HOU.third_order.pcp]succ' [in HOU.second_order.goldfarb.motivation]
symbol [in HOU.third_order.pcp]
T
tails [in HOU.third_order.pcp]tl [in HOU.third_order.pcp]
U
up [in HOU.calculus.prelim]V
var [in HOU.calculus.prelim]Vars [in HOU.calculus.terms_extension]
W
word [in HOU.third_order.pcp]w1 [in HOU.second_order.goldfarb.reduction]
w2 [in HOU.second_order.goldfarb.reduction]
w3 [in HOU.second_order.goldfarb.reduction]
Definition Index
A
abg [in HOU.second_order.goldfarb.encoding]active [in HOU.calculus.normalisation]
add [in HOU.second_order.dowek.encoding]
addEQ [in HOU.second_order.goldfarb.encoding]
addEQ [in HOU.second_order.dowek.encoding]
all_eqs [in HOU.unification.systemunification]
all_terms [in HOU.unification.systemunification]
alpha [in HOU.calculus.prelim]
ap [in HOU.unscoped]
apc [in HOU.unscoped]
AppL [in HOU.calculus.terms_extension]
AppR [in HOU.calculus.terms_extension]
arity [in HOU.calculus.syntax]
Arr [in HOU.calculus.terms_extension]
B
beta [in HOU.calculus.terms]bound [in HOU.firstorder]
C
C [in HOU.calculus.normalisation]cast [in HOU.std.misc]
cfree [in HOU.concon.constants]
charac [in HOU.second_order.goldfarb.motivation]
compRenRen_exp [in HOU.calculus.terms]
compRenSubst_exp [in HOU.calculus.terms]
compSubstRen__exp [in HOU.calculus.terms]
compSubstSubst_exp [in HOU.calculus.terms]
confluent [in HOU.std.ars.confluence]
constEQ [in HOU.second_order.goldfarb.encoding]
constEQ [in HOU.second_order.dowek.encoding]
Consts [in HOU.concon.conservativity]
consts [in HOU.concon.conservativity]
ctx [in HOU.calculus.order]
ctx [in HOU.calculus.typing]
cumulative [in HOU.std.enumerable]
D
decb [in HOU.std.decidable]decb1 [in HOU.std.decidable]
decb2 [in HOU.std.decidable]
decode_subst [in HOU.second_order.goldfarb.reduction]
decomp [in HOU.firstorder]
decomp' [in HOU.firstorder]
decr [in HOU.firstorder]
dec_in [in HOU.std.decidable]
diagId [in HOU.std.countability]
diagStepL [in HOU.std.countability]
diagStepR [in HOU.std.countability]
diagZero [in HOU.std.countability]
diamond [in HOU.std.ars.confluence]
dom [in HOU.calculus.prelim]
E
E [in HOU.calculus.normalisation]E [in HOU.std.ars.evaluator]
enc [in HOU.third_order.encoding]
enc [in HOU.second_order.goldfarb.encoding]
enc [in HOU.second_order.dowek.encoding]
encb [in HOU.third_order.encoding]
encodes [in HOU.second_order.goldfarb.encoding]
encs [in HOU.second_order.dowek.reduction]
enc_sol [in HOU.second_order.goldfarb.reduction]
enum [in HOU.std.enumerable]
enumerable [in HOU.std.enumerable]
enumerable__T [in HOU.std.enumerable]
eq [in HOU.unification.systemunification]
eqs [in HOU.second_order.goldfarb.encoding]
eqs [in HOU.second_order.dowek.encoding]
eqs [in HOU.unification.systemunification]
eqs_ordertyping_strong_ind [in HOU.concon.enumerability]
eqs_typing_strong_ind [in HOU.concon.enumerability]
equiv [in HOU.std.ars.basic]
equi_unifiable [in HOU.firstorder]
eq_ordertyping [in HOU.unification.nth_order_unification]
eq_typing [in HOU.unification.systemunification]
eta [in HOU.calculus.evaluator]
eta₀ [in HOU.calculus.evaluator]
evaluates [in HOU.std.ars.basic]
extRen_exp [in HOU.calculus.terms]
ext_exp [in HOU.calculus.terms]
F
F [in HOU.second_order.goldfarb.encoding]fin [in HOU.unscoped]
find [in HOU.std.lists.advanced]
finst [in HOU.third_order.encoding]
free' [in HOU.firstorder]
Fs [in HOU.second_order.goldfarb.encoding]
func [in HOU.second_order.goldfarb.reduction]
funcomp [in HOU.std.misc]
functional [in HOU.std.ars.basic]
G
G [in HOU.calculus.normalisation]G [in HOU.second_order.goldfarb.encoding]
Gamma__deq [in HOU.second_order.goldfarb.encoding]
Gamma__dwk [in HOU.second_order.dowek.encoding]
ginst [in HOU.third_order.huet]
gonly [in HOU.concon.constants]
Gs [in HOU.second_order.goldfarb.encoding]
GT [in HOU.second_order.goldfarb.reduction]
H
head [in HOU.calculus.syntax]H10 [in HOU.second_order.diophantine_equations]
I
iConsts [in HOU.concon.constants]id [in HOU.unscoped]
idSubst_exp [in HOU.calculus.terms]
inhab [in HOU.concon.conservativity]
isApp [in HOU.calculus.syntax]
isAtom [in HOU.calculus.syntax]
isLam [in HOU.calculus.syntax]
isVar [in HOU.calculus.syntax]
it [in HOU.std.misc]
ith [in HOU.second_order.goldfarb.motivation]
I__S [in HOU.std.countability]
I__P [in HOU.std.countability]
J
joinable [in HOU.std.ars.confluence]L
L [in HOU.std.reductions]Lalt [in HOU.std.reductions]
Lambda [in HOU.calculus.terms_extension]
left_side [in HOU.unification.systemunification]
le_strong_ind [in HOU.concon.enumerability]
lin [in HOU.second_order.goldfarb.encoding]
linearize_terms [in HOU.unification.systemunification]
L_Uextended [in HOU.unification.enumerability]
L_subst [in HOU.unification.enumerability]
L_uni [in HOU.unification.enumerability]
L_typing [in HOU.unification.enumerability]
L_typingT [in HOU.unification.enumerability]
L_type [in HOU.unification.enumerability]
L_exp [in HOU.unification.enumerability]
L_ordsys [in HOU.concon.enumerability]
L_sys [in HOU.concon.enumerability]
L_orduni [in HOU.concon.enumerability]
L_ordertypingT [in HOU.concon.enumerability]
L_le [in HOU.concon.enumerability]
M
morphism [in HOU.std.ars.normalisation]MPCP [in HOU.third_order.pcp]
MPCPsimp [in HOU.third_order.pcp]
MPCP' [in HOU.third_order.simplified]
mul [in HOU.second_order.dowek.encoding]
mulEQ [in HOU.second_order.dowek.encoding]
mulEQ₁ [in HOU.second_order.goldfarb.encoding]
mulEQ₂ [in HOU.second_order.goldfarb.encoding]
mu_enum [in HOU.std.enumerable]
N
nats [in HOU.std.lists.advanced]Neg [in HOU.std.reductions]
Normal [in HOU.std.ars.basic]
NOU [in HOU.unification.nth_order_unification]
NSOU [in HOU.unification.nth_order_unification]
NU [in HOU.unification.higher_order_unification]
O
ofNat [in HOU.std.enumerable]ord [in HOU.calculus.order]
ordertypingSubst [in HOU.calculus.order]
ordertyping_strong_ind [in HOU.concon.enumerability]
ord' [in HOU.calculus.order]
OU [in HOU.unification.nth_order_unification]
P
PCP [in HOU.third_order.pcp]PCPsimp [in HOU.third_order.pcp]
R
redctx [in HOU.third_order.simplified]redtm [in HOU.third_order.simplified]
reduction [in HOU.std.reductions]
red_fun [in HOU.std.ars.evaluator]
ren_closed [in HOU.calculus.normalisation]
ren_exp [in HOU.calculus.terms]
retype_type [in HOU.concon.retyping]
retype_ctx [in HOU.concon.retyping]
rho [in HOU.calculus.confluence]
right_side [in HOU.unification.systemunification]
rinstInst_up_exp_exp [in HOU.calculus.terms]
rinst_inst_exp [in HOU.calculus.terms]
R_nat_nat [in HOU.std.enumerable]
R__S [in HOU.std.countability]
R__P [in HOU.std.countability]
S
sapp [in HOU.calculus.prelim]scons [in HOU.unscoped]
select [in HOU.std.lists.advanced]
semi_confluent [in HOU.std.ars.confluence]
SemType [in HOU.calculus.normalisation]
semtyping [in HOU.calculus.normalisation]
seteq [in HOU.std.lists.basics]
shift [in HOU.unscoped]
size [in HOU.firstorder]
size_exp [in HOU.second_order.goldfarb.reduction]
SNU [in HOU.unification.systemunification]
Sol [in HOU.second_order.diophantine_equations]
SOU [in HOU.unification.nth_order_unification]
strict_incl [in HOU.std.lists.basics]
SU [in HOU.unification.systemunification]
subst_consts [in HOU.concon.conservativity]
subst_exp [in HOU.calculus.terms]
subst_eq [in HOU.unification.systemunification]
subvars [in HOU.firstorder]
sub_sol [in HOU.second_order.dowek.reduction]
Succ [in HOU.second_order.goldfarb.motivation]
succ [in HOU.second_order.goldfarb.motivation]
Sum [in HOU.std.misc]
T
T [in HOU.second_order.goldfarb.reduction]tab [in HOU.std.lists.advanced]
tak_fun [in HOU.std.ars.confluence]
target [in HOU.calculus.syntax]
target' [in HOU.calculus.syntax]
tight [in HOU.std.retracts]
typingRen [in HOU.calculus.typing]
typingSubst [in HOU.calculus.typing]
typing_strong_ind [in HOU.unification.enumerability]
T_list [in HOU.std.enumerable]
T_prod [in HOU.std.enumerable]
T_ [in HOU.std.enumerable]
U
U [in HOU.unification.higher_order_unification]Uextended [in HOU.unification.enumerability]
unif [in HOU.firstorder]
Unifies [in HOU.firstorder]
unifies [in HOU.firstorder]
update [in HOU.firstorder]
upExtRen_exp_exp [in HOU.calculus.terms]
upExt_exp_exp [in HOU.calculus.terms]
upId_exp_exp [in HOU.calculus.terms]
upRen_exp_exp [in HOU.calculus.terms]
up_ren [in HOU.unscoped]
up_subst_subst_exp_exp [in HOU.calculus.terms]
up_subst_ren_exp_exp [in HOU.calculus.terms]
up_ren_subst_exp_exp [in HOU.calculus.terms]
up_exp_exp [in HOU.calculus.terms]
V
V [in HOU.calculus.normalisation]varEQ [in HOU.second_order.goldfarb.encoding]
varEQ [in HOU.second_order.dowek.encoding]
vars [in HOU.calculus.syntax]
Vars__de [in HOU.second_order.diophantine_equations]
vars__de [in HOU.second_order.diophantine_equations]
Vars' [in HOU.unification.systemunification]
vars' [in HOU.unification.systemunification]
var_zero [in HOU.unscoped]
X
xi [in HOU.calculus.evaluator]Record Index
C
Const [in HOU.calculus.terms]D
Dec [in HOU.std.decidable]Dec1 [in HOU.std.decidable]
Dec2 [in HOU.std.decidable]
Dis [in HOU.std.decidable]
E
enumT [in HOU.std.enumerable]O
ordsysuni [in HOU.unification.nth_order_unification]orduni [in HOU.unification.nth_order_unification]
R
retract [in HOU.std.retracts]S
sysuni [in HOU.unification.systemunification]U
uni [in HOU.unification.higher_order_unification]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1863 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 | (80 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 | (255 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 | (51 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 | (798 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 | (67 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 | (33 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 | (28 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 | (152 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 | (137 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 | (29 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 | (222 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 | (11 entries) |