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 _ (1807 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (50 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 _ (1037 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 _ (159 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 _ (94 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 _ (381 entries)
Module 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 _ (34 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (52 entries)

Global Index

A

A [axiom, in prelude.decidable_set]
A [axiom, in rpo.rpo]
accElim3 [lemma, in prelude.AccP]
AccElim3 [lemma, in prelude.AccP]
AccP [library]
acc_imp [lemma, in prelude.not_decreasing]
Acc_iter_partial [definition, in prelude.PartialFix]
acc_trans [lemma, in prelude.closure]
all_b_relation [lemma, in denumerable.Denumerable]
all_nats [constructor, in hilbert.Enumeration]
all_ord_acc [lemma, in schutte.Schutte]
alpha_A [lemma, in schutte.Ordering_Functions]
alpha_plus_sup [lemma, in schutte.Plus]
alpha_plus_zero [lemma, in schutte.Plus]
alpha_sup [lemma, in schutte.Ordering_Functions]
AP [inductive, in schutte.AP]
ap [inductive, in gamma0.Gamma0_prelude]
ap [inductive, in epsilon0.EPSILON0]
AP [library]
app [definition, in epsilon0.MSE0]
app_equiv_assoc [lemma, in epsilon0.MSE0]
app_equiv_comm [lemma, in epsilon0.MSE0]
AP_closed [lemma, in schutte.AP]
AP_finite_eq_one [lemma, in schutte.AP]
AP_Inc_ordinal [lemma, in schutte.AP]
AP_intro [constructor, in schutte.AP]
ap_intro [constructor, in epsilon0.EPSILON0]
ap_intro [constructor, in gamma0.Gamma0_prelude]
AP_omega [lemma, in schutte.AP]
AP_one [lemma, in schutte.AP]
AP_o_segment [lemma, in schutte.AP]
AP_phi0 [lemma, in schutte.AP]
ap_phi0 [lemma, in epsilon0.EPSILON0]
ap_phi0R [lemma, in epsilon0.EPSILON0]
AP_plus_AP [lemma, in schutte.AP]
AP_plus_closed [lemma, in schutte.AP]
AP_sup [lemma, in schutte.AP]
AP_to_phi0 [lemma, in schutte.AP]
AP_unbounded [lemma, in schutte.AP]
Arith_lemmas [library]
arity [axiom, in rpo.term]
arrow_disj [lemma, in hilbert.OldEpsilon]
au_moins_une_im [definition, in SCHROEDER.Functions]
au_moins_un_ant [definition, in SCHROEDER.Functions]
au_plus_une_im [definition, in SCHROEDER.Functions]
au_plus_un_ant [definition, in SCHROEDER.Functions]
AX2 [axiom, in schutte.Schutte]
AX3 [axiom, in schutte.Schutte]
A1_A2 [lemma, in schutte.Ordering_Functions]
A2_A1 [lemma, in schutte.Ordering_Functions]
A_closed [lemma, in schutte.Ordering_Functions]


B

BadEpsilon2 [library]
bad_two [definition, in hilbert.Epsilon_Examples]
Bells_lemma [lemma, in hilbert.OldEpsilon]
big_number_eq [lemma, in misc.G4]
bij [lemma, in prelude.bintree]
bijection [inductive, in SCHROEDER.Functions]
bijection_fun_rel [lemma, in hilbert.PartialFun]
bijection_rel_fun [lemma, in hilbert.PartialFun]
bijR [lemma, in prelude.bintree]
Bin [constructor, in prelude.bintree]
bintree [inductive, in prelude.bintree]
bintree [library]
B_of [lemma, in schutte.Ordering_Functions]
B_of' [lemma, in schutte.Ordering_Functions]


C

cardinal_subset [axiom, in prelude.list_set]
choice [lemma, in hilbert.ClassicalEpsilonModified]
choice_fun [definition, in hilbert.Epsilon]
choice_fun [definition, in hilbert.OldEpsilon]
choice_fun_e [lemma, in hilbert.OldEpsilon]
choice_fun_e [lemma, in hilbert.Epsilon]
choice_fun_ind [lemma, in hilbert.Epsilon]
choice_fun_ind [lemma, in hilbert.OldEpsilon]
ClassicalEpsilonModified [library]
classical_indefinite_description [lemma, in hilbert.ClassicalEpsilonModified]
classification [lemma, in schutte.Schutte]
closed [inductive, in schutte.Schutte]
closed_intro [constructor, in schutte.Schutte]
closure [library]
CNF [library]
cnf_eq [lemma, in schutte.CNF]
cnf_exists [lemma, in schutte.CNF]
cnf_head_eq [lemma, in schutte.CNF]
cnf_of [inductive, in schutte.CNF]
cnf_of_ap [lemma, in schutte.CNF]
cnf_of_AP [lemma, in schutte.CNF]
cnf_plus [lemma, in schutte.CNF]
cnf_plus1 [lemma, in schutte.CNF]
cnf_plus2 [lemma, in schutte.CNF]
cnf_unicity [lemma, in schutte.CNF]
coeff_lt [constructor, in epsilon0.EPSILON0]
compare [definition, in epsilon0.EPSILON0]
compare [definition, in gamma0.Gamma0]
compare_eq_rw [lemma, in gamma0.Gamma0]
compare_gt_rw [lemma, in gamma0.Gamma0]
compare_lt_rw [lemma, in gamma0.Gamma0]
compare_reflect [lemma, in gamma0.Gamma0]
compare_rw_eq [lemma, in gamma0.Gamma0]
compare_rw_gt [lemma, in gamma0.Gamma0]
compare_rw_lt [lemma, in gamma0.Gamma0]
compose [definition, in prelude.bintree]
compose [definition, in hilbert.Paradoxical]
cons [constructor, in schutte.CNF]
cons [constructor, in epsilon0.EPSILON0]
cons [constructor, in gamma0.Gamma0_prelude]
constructive_definite_description [lemma, in hilbert.ClassicalEpsilonModified]
constructive_indefinite_description [axiom, in hilbert.ClassicalEpsilonModified]
Cons_correct [constructor, in epsilon0.Goodstein]
cons_forall [constructor, in schutte.CNF]
cons_lt_e0 [constructor, in gamma0.Gamma0_prelude]
cons_nf [constructor, in epsilon0.EPSILON0]
cons_nf [constructor, in gamma0.Gamma0_prelude]
continuous [inductive, in schutte.Schutte]
continuous_intro [constructor, in schutte.Schutte]
correct [inductive, in epsilon0.Goodstein]
correct_succ [lemma, in epsilon0.Goodstein]
Cr [definition, in schutte.Critical]
critical [definition, in schutte.Critical]
Critical [library]
critical_e [lemma, in schutte.Critical]
critical_eq [lemma, in schutte.Critical]
critical_extensional [lemma, in schutte.Critical]
critical_fun [definition, in schutte.Critical]
Critical_incl [lemma, in schutte.Critical]
critical_lt [lemma, in schutte.Critical]
critical_ord [lemma, in schutte.Critical]
critical_pos [lemma, in schutte.Critical]
critical_pos_inv [lemma, in schutte.Critical]
critical_zero [lemma, in schutte.Critical]
critical_zero_inv [lemma, in schutte.Critical]
Cr_incl [lemma, in schutte.Critical]
Cr_incl' [lemma, in schutte.Critical]
Cr_pos [lemma, in schutte.Critical]
Cr_rw [lemma, in schutte.Critical]
Cr_zero [lemma, in schutte.Critical]
Cr_zero_AP [lemma, in schutte.Critical]
c_no_pred [lemma, in epsilon0.E0_ARITH]


D

dd' [lemma, in hilbert.OldEpsilon]
dd' [lemma, in hilbert.Epsilon]
dd'' [lemma, in hilbert.Epsilon]
dd'' [lemma, in hilbert.OldEpsilon]
decidable_set [library]
decompose [definition, in prelude.bintree]
DecVar [module, in rpo.term]
denumerable [inductive, in hilbert.Enumeration]
denumerable [definition, in denumerable.Denumerable]
Denumerable [library]
denumerable_add [lemma, in hilbert.Enumeration]
denumerable_add_disj [lemma, in hilbert.Enumeration]
denumerable_bij_fun [lemma, in hilbert.Enumeration]
denumerable_bij_fun [lemma, in denumerable.Denumerable]
denumerable_bij_funR [lemma, in denumerable.Denumerable]
denumerable_bij_funR [lemma, in hilbert.Enumeration]
denumerable_bij_rel [lemma, in hilbert.Enumeration]
denumerable_empty [lemma, in denumerable.Denumerable]
denumerable_empty [lemma, in hilbert.Enumeration]
denumerable_finite [lemma, in denumerable.Denumerable]
denumerable_incl [lemma, in hilbert.Enumeration]
denumerable_inclusion [lemma, in denumerable.Denumerable]
denumerable_inj [lemma, in hilbert.Enumeration]
denumerable_intro [constructor, in hilbert.Enumeration]
denumerable_members [lemma, in schutte.Schutte]
denumerable_not_Unbounded [lemma, in schutte.Schutte]
denumerable_segment_proper [lemma, in schutte.Ordering_Functions]
denumerable_singleton [lemma, in denumerable.Denumerable]
denumerable_surj [lemma, in denumerable.Denumerable]
denumerable_union [lemma, in denumerable.Denumerable]
denumerable_union_qcq [lemma, in denumerable.Denumerable]
depth1 [constructor, in epsilon0.Hydra]
depth2 [constructor, in epsilon0.Hydra]
diag [library]
dickson [library]
div2_double_is_id [lemma, in denumerable.Arith_lemmas]
double_inj [lemma, in denumerable.Arith_lemmas]
double_is_even [lemma, in denumerable.Arith_lemmas]
DS [module, in prelude.list_set]
DS [module, in prelude.list_permut]
D_a [definition, in schutte.Well_Orders]


E

elagage [definition, in hilbert.more_relations]
elagage_choisi [definition, in hilbert.more_relations]
elaguer_mini [definition, in hilbert.more_relations]
empty_enumeration [lemma, in hilbert.Enumeration]
empty_ordering [lemma, in schutte.Ordering_Functions]
empty_subst_is_id [axiom, in rpo.term]
empty_subst_is_id_list [axiom, in rpo.term]
enumerates [inductive, in hilbert.Enumeration]
enumerates_i [constructor, in hilbert.Enumeration]
Enumeration [library]
epsax [axiom, in hilbert.OldEpsilon]
epsilon [definition, in gamma0.Gamma0_prelude]
epsilon [axiom, in hilbert.BadEpsilon2]
epsilon [axiom, in hilbert.OldEpsilon]
epsilon [definition, in hilbert.ClassicalEpsilonModified]
Epsilon [library]
EPSILON0 [definition, in gamma0.Gamma0_prelude]
epsilon0 [definition, in gamma0.Gamma0_prelude]
EPSILON0 [library]
epsilon_e [lemma, in hilbert.OldEpsilon]
epsilon_equiv [lemma, in hilbert.Epsilon]
epsilon_equiv [lemma, in hilbert.OldEpsilon]
Epsilon_Examples [library]
epsilon_extensionality [definition, in hilbert.Epsilon]
epsilon_extensionality [definition, in hilbert.OldEpsilon]
epsilon_ind [lemma, in hilbert.Epsilon]
epsilon_ind [lemma, in hilbert.OldEpsilon]
epsilon_spec [definition, in hilbert.ClassicalEpsilonModified]
Eps0_alg [module, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.ap_plus [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.ap_plusR [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.Cantor_normal_form [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_ok_1 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_reflect [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_reflectR [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_rw1 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_rw2 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_rw3 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.cons_ambiguity [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.cons_unicity [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_compat [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_F [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_fin_omega [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_F_compat [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.get_decomposition [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.le_phi0_phi0 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.le_succ_succ [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_a_phi0_a [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_inc_rpo_0 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_intro [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_phi0_phi0 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_subterm1 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_subterm2 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_le [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_le_R [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_le_2 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_succ [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_assoc [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_comm [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_dec [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_le_1 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_nf [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus_a_a [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus_le [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus_lt [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_a_0 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_a_1 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_compat [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_fin_omega [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_0_a [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_1_a [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nat_lt_cons [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nat_2_term [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nat_2_term_mono [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nf_Wf [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.None [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.omega_exp_rw [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.omega_minus_one [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.omega_term_ambiguity [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_log [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_lt [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_ltR [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_plus_mult [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_a_zero [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_compat [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_cons_cons_rw1 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_cons_cons_rw2 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_cons_cons_rw3 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_fin_omega [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_is_zero [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_nf [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_nf0 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_not_comm [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_to_cons [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_zero [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.pred [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.rpo_trans [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.R_inc_rpo [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_compat [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_is_plus_one [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_nf [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_nf2 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.transfinite_induction [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.transfinite_induction_Q [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.trichotomy [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size1 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size2 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size3 [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_2_term [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.well_founded_rpo [lemma, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [definition, in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [definition, in epsilon0.EPSILON0]
Eps0_prec [module, in epsilon0.EPSILON0]
Eps0_prec.A [definition, in epsilon0.EPSILON0]
Eps0_prec.Lex [constructor, in epsilon0.EPSILON0]
Eps0_prec.Mul [constructor, in epsilon0.EPSILON0]
Eps0_prec.prec [definition, in epsilon0.EPSILON0]
Eps0_prec.prec_antisym [lemma, in epsilon0.EPSILON0]
Eps0_prec.prec_dec [lemma, in epsilon0.EPSILON0]
Eps0_prec.prec_transitive [lemma, in epsilon0.EPSILON0]
Eps0_prec.status [definition, in epsilon0.EPSILON0]
Eps0_prec.status_type [inductive, in epsilon0.EPSILON0]
Eps0_rpo [module, in epsilon0.EPSILON0]
Eps0_sig [module, in epsilon0.EPSILON0]
Eps0_sig.AC [constructor, in epsilon0.EPSILON0]
Eps0_sig.arity [definition, in epsilon0.EPSILON0]
Eps0_sig.arity_type [inductive, in epsilon0.EPSILON0]
Eps0_sig.C [constructor, in epsilon0.EPSILON0]
Eps0_sig.eq_symbol_dec [lemma, in epsilon0.EPSILON0]
Eps0_sig.Free [constructor, in epsilon0.EPSILON0]
Eps0_sig.nat_S [constructor, in epsilon0.EPSILON0]
Eps0_sig.nat_0 [constructor, in epsilon0.EPSILON0]
Eps0_sig.ord_cons [constructor, in epsilon0.EPSILON0]
Eps0_sig.ord_zero [constructor, in epsilon0.EPSILON0]
Eps0_sig.symb [definition, in epsilon0.EPSILON0]
Eps0_sig.symb0 [inductive, in epsilon0.EPSILON0]
eps_extensional_forall_def [lemma, in hilbert.OldEpsilon]
eps_extentional_exm [lemma, in hilbert.OldEpsilon]
equipollence [inductive, in SCHROEDER.Equipollence]
Equipollence [library]
equipollence_intro [constructor, in SCHROEDER.Equipollence]
equiv [definition, in epsilon0.MSE0]
equiv_cong1 [lemma, in epsilon0.MSE0]
equiv_cong2 [lemma, in epsilon0.MSE0]
equiv_cons [lemma, in epsilon0.MSE0]
equiv_perm [lemma, in epsilon0.MSE0]
equiv_refl [lemma, in epsilon0.MSE0]
equiv_sym [lemma, in epsilon0.MSE0]
equiv_tail [lemma, in epsilon0.MSE0]
equiv_trans [lemma, in epsilon0.MSE0]
eq_A_dec [axiom, in prelude.decidable_set]
eq_le [lemma, in schutte.Schutte]
eq_symbol_dec [axiom, in rpo.term]
eq_term_dec [axiom, in rpo.term]
eq_variable_dec [axiom, in rpo.term]
euclid [library]
Euc1 [lemma, in prelude.More_nat]
Euc2 [lemma, in prelude.More_nat]
eval [definition, in schutte.CNF]
eval_bounded [lemma, in schutte.CNF]
eval_ordinal [lemma, in schutte.CNF]
even_prod [lemma, in denumerable.Arith_lemmas]
excluded_middle_informative [lemma, in hilbert.ClassicalEpsilonModified]
exists_map12_without_repetition [lemma, in prelude.more_list]
exists_map_without_repetition [lemma, in prelude.more_list]
exists_sigT [definition, in hilbert.BadEpsilon2]
exist_1_R_a [definition, in hilbert.PartialFun]
exp_nf [lemma, in epsilon0.E0_ARITH]
ex_to_sig [lemma, in hilbert.OldEpsilon]
ex_unic_introduction [lemma, in hilbert.Epsilon]
ex_1 [definition, in hilbert.OldEpsilon]
ex_1_introduction [lemma, in hilbert.OldEpsilon]
E0_ARITH [library]


F

f [definition, in misc.G4]
F [module, in rpo.term]
Final [lemma, in misc.G4]
final [inductive, in misc.G4]
final_intro [constructor, in misc.G4]
final_no_future [lemma, in misc.G4]
find [definition, in prelude.more_list]
find_not_mem [lemma, in prelude.more_list]
finite [definition, in schutte.Schutte]
finite [definition, in gamma0.Gamma0_prelude]
finite [definition, in epsilon0.EPSILON0]
finite_inj [lemma, in schutte.Schutte]
finite_is_finite [lemma, in gamma0.Gamma0]
finite_lt [lemma, in epsilon0.EPSILON0]
finite_ltR [lemma, in epsilon0.EPSILON0]
finite_lt_inv [lemma, in schutte.Schutte]
finite_lt_omega [lemma, in schutte.Schutte]
finite_lt_omega [lemma, in gamma0.Gamma0]
finite_mono [lemma, in schutte.Schutte]
finite_plus_ge_omega [lemma, in schutte.Plus]
fold_left2 [definition, in prelude.more_list]
fonction [inductive, in SCHROEDER.Functions]
forall_def [lemma, in hilbert.OldEpsilon]
forall_def [lemma, in hilbert.Epsilon]
from_E [constructor, in denumerable.Denumerable]
from_F [constructor, in denumerable.Denumerable]
FunctionalChoice [lemma, in hilbert.OldEpsilon]
Functions [library]
fun_bijection [inductive, in hilbert.PartialFun]
fun_bij_i [constructor, in hilbert.PartialFun]
fun_codomain [definition, in hilbert.PartialFun]
fun_eq [definition, in schutte.Ordering_Functions]
fun_eq_gen [definition, in schutte.Ordering_Functions]
fun_eq_refl [lemma, in schutte.Ordering_Functions]
fun_inj [definition, in hilbert.PartialFun]
fun_injection [inductive, in hilbert.PartialFun]
fun_inj_i [constructor, in hilbert.PartialFun]
fun_onto [definition, in hilbert.PartialFun]
fun_rel_same [definition, in hilbert.PartialFun]
fun_restrict [definition, in schutte.Ordering_Functions]
F1 [lemma, in misc.G4]
F2 [lemma, in misc.G4]
F27 [lemma, in misc.G4]
F28 [lemma, in misc.G4]
F3 [lemma, in misc.G4]
F4 [lemma, in misc.G4]
f_beta [definition, in schutte.Ordering_Functions]
f_decreases [lemma, in epsilon0.EPSILON0]
f_not_in_normal_form [lemma, in epsilon0.EPSILON0]
f_Sn [lemma, in misc.G4]
f_sup_commutes [lemma, in schutte.Ordering_Functions]
f_Z [definition, in misc.G4]


G

g [definition, in schutte.Ordering_Functions]
Gamma0 [library]
Gamma0_alg [module, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.cons_lt_epsilon0 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.cons_rw [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.cons_succ [constructor, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.epsilon0_as_lub [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.epsilon_fxp [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.finite_succ [constructor, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.F_not_lim [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.inj_mono [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.inj_monoR [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit [inductive, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_ab [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_cons [constructor, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_cons_inv [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_intro [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_not_succ [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_0 [constructor, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_successor [inductive, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_successor_ok [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_succ_not_lim [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.le_b_phi_ab [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.le_plus_l [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.le_plus_r [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F [inductive, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_cons [constructor, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_inv0 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_lim [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_ok [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_plus [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_0 [constructor, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_a_phi_ab [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_ok [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_okR [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_succ [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_trans [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_inc_rpo_0 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_not_gt [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_rpo_cons_cons [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_subterm1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_T1_injection [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lub [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lub_mono [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lub_unicity [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.ml_psi [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.ml_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.moser_lepper [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_lt_cons [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_lt_psi [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_2_term [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_2_term_mono [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nf_intro [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nf_nat_irrelevance [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nf_Wf [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.no_critical [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_alpha_zero [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_cases [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_cases' [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_cases_aux [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_fix [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_inj_r [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_le [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_le_ge [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_mono_r [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_mono_RR [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_mono_weak_r [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_nf [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_any_cons [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_psi [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_psi_plus_finite [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_psi_succ [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_principal [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_principalR [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_psi [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_spec1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_2 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_3 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_4 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_5 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_6 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_assoc [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_mono_l_weak [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_mono_r [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_nf [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_nf [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_cons [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_cons' [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_limit [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_succ [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.psi_lt_epsilon0 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.psi_principal [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_trans [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_2 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_3 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_4 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_2 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_3 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_4 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_2 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_3 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_4 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_2 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_3 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_4 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_6_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_6_4 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_7_1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.R_inc_rpo [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.succ_as_plus [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.succ_limit_dec [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.succ_nf [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.th_14_5 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.th_14_6 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.transfinite_induction [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.transfinite_induction_Q [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T1_injection [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T1_injection_lt [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size1 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size2 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size3 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size4 [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size_psi [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_2_term [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.well_founded_rpo [lemma, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.zero [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.zero [definition, in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.zero_not_lim [lemma, in gamma0.Gamma0]
Gamma0_length [library]
Gamma0_prec [module, in gamma0.Gamma0]
Gamma0_prec.A [definition, in gamma0.Gamma0]
Gamma0_prec.Lex [constructor, in gamma0.Gamma0]
Gamma0_prec.Mul [constructor, in gamma0.Gamma0]
Gamma0_prec.prec [definition, in gamma0.Gamma0]
Gamma0_prec.prec_antisym [lemma, in gamma0.Gamma0]
Gamma0_prec.prec_dec [lemma, in gamma0.Gamma0]
Gamma0_prec.prec_transitive [lemma, in gamma0.Gamma0]
Gamma0_prec.status [definition, in gamma0.Gamma0]
Gamma0_prec.status_type [inductive, in gamma0.Gamma0]
Gamma0_prelude [library]
Gamma0_rpo [module, in gamma0.Gamma0]
Gamma0_sig [module, in gamma0.Gamma0]
Gamma0_sig.AC [constructor, in gamma0.Gamma0]
Gamma0_sig.arity [definition, in gamma0.Gamma0]
Gamma0_sig.arity_type [inductive, in gamma0.Gamma0]
Gamma0_sig.C [constructor, in gamma0.Gamma0]
Gamma0_sig.eq_symbol_dec [lemma, in gamma0.Gamma0]
Gamma0_sig.Free [constructor, in gamma0.Gamma0]
Gamma0_sig.nat_S [constructor, in gamma0.Gamma0]
Gamma0_sig.nat_0 [constructor, in gamma0.Gamma0]
Gamma0_sig.ord_cons [constructor, in gamma0.Gamma0]
Gamma0_sig.ord_psi [constructor, in gamma0.Gamma0]
Gamma0_sig.ord_zero [constructor, in gamma0.Gamma0]
Gamma0_sig.symb [definition, in gamma0.Gamma0]
Gamma0_sig.symb0 [inductive, in gamma0.Gamma0]
get_predecessor [lemma, in prelude.More_nat]
ge_ordinal [lemma, in schutte.Schutte]
Goodstein [library]
Goodstein_decrease [lemma, in epsilon0.Goodstein]
goodstein_next [definition, in epsilon0.Goodstein]
goodstein_next_ord [definition, in epsilon0.Goodstein]
goodstein_next_ord_correct [lemma, in epsilon0.Goodstein]
goodstein_next_ord_lt [lemma, in epsilon0.Goodstein]
goodstein_next_ord_nf [lemma, in epsilon0.Goodstein]
Goodstein_thm [lemma, in epsilon0.Goodstein]
gpred [definition, in epsilon0.Goodstein]
gpred_lt [lemma, in epsilon0.Goodstein]
Greater [definition, in schutte.Plus]
Greater_inc_ord [lemma, in schutte.Plus]
Greater_o_segment [lemma, in schutte.Plus]
GRelation [definition, in denumerable.GRelations]
GRelations [library]
gt_ordinal [lemma, in schutte.Schutte]
G4 [library]
G4_length [lemma, in misc.G4]
g_bij [lemma, in schutte.Ordering_Functions]
g_def [lemma, in schutte.Ordering_Functions]
g_def1 [lemma, in schutte.Ordering_Functions]
g_domains [lemma, in schutte.Ordering_Functions]
g_lemma [lemma, in schutte.Ordering_Functions]
g_mono [lemma, in schutte.Ordering_Functions]
g_ord [lemma, in schutte.Ordering_Functions]
g_unic [lemma, in schutte.Ordering_Functions]
g_1_bij [lemma, in schutte.Ordering_Functions]
g_1_of [lemma, in schutte.Ordering_Functions]


H

h [inductive, in SCHROEDER.Schroeder]
has_cnf_ordinal [lemma, in schutte.CNF]
hcons [constructor, in epsilon0.Hydra]
head [definition, in epsilon0.Hydra]
head [definition, in epsilon0.Hydra]
head [constructor, in epsilon0.Hydra]
head_at [definition, in epsilon0.Hydra]
head_at_l [definition, in epsilon0.Hydra]
head_at_l_nil [lemma, in epsilon0.Hydra]
head_at_l_O_cons [lemma, in epsilon0.Hydra]
head_at_l_S_cons [lemma, in epsilon0.Hydra]
head_at_l_S_nil [lemma, in epsilon0.Hydra]
head_at_l_zero_nil [lemma, in epsilon0.Hydra]
head_at_nil [lemma, in epsilon0.Hydra]
head_at_O_cons [lemma, in epsilon0.Hydra]
head_at_S_cons [lemma, in epsilon0.Hydra]
head_at_S_nil [lemma, in epsilon0.Hydra]
head_at_zero_nil [lemma, in epsilon0.Hydra]
head_lt [constructor, in epsilon0.EPSILON0]
head_lt_cons [lemma, in epsilon0.EPSILON0]
Hercules_ok [definition, in epsilon0.Hydra]
Hercules_strat [definition, in epsilon0.Hydra]
Hercules_wins [inductive, in epsilon0.Hydra]
hl_intro [constructor, in SCHROEDER.Schroeder]
hr_intro [constructor, in SCHROEDER.Schroeder]
Hydra [inductive, in epsilon0.Hydra]
Hydra [library]
Hydrae [inductive, in epsilon0.Hydra]
Hydra_answers [lemma, in epsilon0.Hydra]
Hydra_answers_nil [lemma, in epsilon0.Hydra]
Hydra_strat [definition, in epsilon0.Hydra]
h2o [definition, in epsilon0.Hydra]
h2ol [definition, in epsilon0.Hydra]
h2ol_nfs [lemma, in epsilon0.Hydra]
h2o_nf [lemma, in epsilon0.Hydra]
h_bij [lemma, in SCHROEDER.Schroeder]


I

Im [inductive, in SCHROEDER.Functions]
image [definition, in hilbert.PartialFun]
Im_intro [constructor, in SCHROEDER.Functions]
Im_stable_par_incl [lemma, in SCHROEDER.Functions]
Inc_elim [lemma, in schutte.Ordering_Functions]
induc [lemma, in hilbert.Paradoxical]
Induction [lemma, in schutte.Schutte]
inductive [definition, in hilbert.Paradoxical]
Infinite_union [definition, in denumerable.Denumerable]
inf_card [inductive, in SCHROEDER.Equipollence]
inf_card_intro [constructor, in SCHROEDER.Equipollence]
inhabited [definition, in hilbert.OldEpsilon]
inhabited [definition, in hilbert.BadEpsilon2]
inh_ens_OT [lemma, in schutte.Critical]
inh_nat [lemma, in schutte.AP]
inh_Ordinal_sets [lemma, in schutte.Ordering_Functions]
inh_OT [axiom, in schutte.Schutte]
inh_OT_OT [lemma, in schutte.Ordering_Functions]
inh_proj [definition, in hilbert.OldEpsilon]
injection [inductive, in SCHROEDER.Functions]
inleft [definition, in epsilon0.EPSILON0]
inv_compose [lemma, in hilbert.PartialFun]
inv_composeR [lemma, in hilbert.PartialFun]
inv_fun [definition, in hilbert.PartialFun]
inv_fun_bij [lemma, in hilbert.PartialFun]
inv_spec_ex [lemma, in hilbert.PartialFun]
inv_spec_func [lemma, in hilbert.PartialFun]
inv_trans [lemma, in prelude.closure]
in_in_map [lemma, in prelude.more_list]
in_map_in [lemma, in prelude.more_list]
in_or_not_in [definition, in SCHROEDER.Schroeder]
in_remove [lemma, in prelude.more_list]
iota [definition, in hilbert.Epsilon]
iota [definition, in hilbert.OldEpsilon]
iota_e [lemma, in hilbert.OldEpsilon]
iota_e [lemma, in hilbert.Epsilon]
iota_fun [definition, in hilbert.Epsilon]
iota_fun [definition, in hilbert.OldEpsilon]
iota_fun_e [lemma, in hilbert.OldEpsilon]
iota_fun_e [lemma, in hilbert.Epsilon]
iota_fun_ind [lemma, in hilbert.Epsilon]
iota_fun_ind [lemma, in hilbert.OldEpsilon]
iota_fun_rw [lemma, in hilbert.Epsilon]
iota_fun_rw [lemma, in hilbert.OldEpsilon]
iota_ind [lemma, in hilbert.OldEpsilon]
iota_ind [lemma, in hilbert.Epsilon]
iota_parameter_rw [lemma, in hilbert.OldEpsilon]
iota_parameter_rw [lemma, in hilbert.Epsilon]
isotonic [definition, in schutte.Well_Orders]
isotonicity_refl [lemma, in schutte.Well_Orders]
isotonicity_sym [lemma, in schutte.Well_Orders]
isotonicity_trans [lemma, in schutte.Well_Orders]
iso_inj [lemma, in schutte.Well_Orders]
is_a_pos_exists_subtem [axiom, in rpo.term]
is_finite [definition, in schutte.Schutte]
is_finite [inductive, in gamma0.Gamma0_prelude]
is_finite_finite [lemma, in gamma0.Gamma0]
is_least_member [definition, in schutte.Well_Orders]
is_limit [definition, in schutte.Schutte]
is_limit_omega [lemma, in schutte.Schutte]
is_limit_ordinal [lemma, in schutte.Schutte]
is_limit_phi0 [lemma, in schutte.AP]
is_limit_sup_members [lemma, in schutte.Schutte]
is_lub [definition, in schutte.Lub]
is_succ [definition, in schutte.Schutte]
is_succ_ordinal [lemma, in schutte.Schutte]
item [inductive, in misc.G4]


K

K [definition, in prelude.bintree]
ksi_plus_beta [lemma, in schutte.AP]
ksi_plus_beta_eq [lemma, in schutte.AP]
ksi_plus_seq_n' [lemma, in schutte.AP]


L

laboureur [definition, in denumerable.Denumerable]
lab_bij [lemma, in denumerable.Denumerable]
lab_rel_wf [lemma, in denumerable.Denumerable]
Later [constructor, in epsilon0.Hydra]
le [definition, in gamma0.Gamma0_prelude]
le [definition, in schutte.Schutte]
le [definition, in epsilon0.EPSILON0]
Le [definition, in schutte.Well_Orders]
Leaf [definition, in prelude.bintree]
Leaf [constructor, in prelude.bintree]
least_AP [lemma, in schutte.AP]
least_member_glb [lemma, in schutte.Well_Orders]
least_member_lower_bound [lemma, in schutte.Well_Orders]
least_member_of_eq [lemma, in schutte.Well_Orders]
least_member_unicity [lemma, in schutte.Well_Orders]
Legend [lemma, in epsilon0.Hydra]
length [definition, in gamma0.Gamma0_length]
length_a [lemma, in gamma0.Gamma0_length]
length_ab [lemma, in gamma0.Gamma0_length]
length_abnc [lemma, in gamma0.Gamma0_length]
length_aux [definition, in gamma0.Gamma0_length]
length_b [lemma, in gamma0.Gamma0_length]
length_c [lemma, in gamma0.Gamma0_length]
length_map [lemma, in prelude.more_list]
length_n [lemma, in gamma0.Gamma0_length]
length_psi [lemma, in gamma0.Gamma0_length]
Lerne [definition, in epsilon0.Hydra]
less_than [constructor, in hilbert.Enumeration]
lex [definition, in rpo.rpo]
lexof_wf [lemma, in denumerable.Denumerable]
lex_trans [lemma, in rpo.rpo]
le_alpha_zero [lemma, in schutte.Schutte]
Le_antisym [lemma, in schutte.Well_Orders]
le_antisym [lemma, in schutte.Schutte]
le_cons_tail [lemma, in gamma0.Gamma0]
le_disj [lemma, in schutte.Schutte]
le_eq_or_lt [lemma, in schutte.Schutte]
le_inv [lemma, in epsilon0.EPSILON0]
le_inv_nc [lemma, in gamma0.Gamma0]
le_lt_trans [lemma, in schutte.Schutte]
le_lt_trans [lemma, in epsilon0.EPSILON0]
le_lt_trans [lemma, in gamma0.Gamma0]
Le_Lt_trans [lemma, in schutte.Well_Orders]
le_not_gt [lemma, in schutte.Schutte]
le_one_cons [lemma, in gamma0.Gamma0]
le_ordinal [lemma, in schutte.Schutte]
le_plus_l [lemma, in schutte.Plus]
le_plus_r [lemma, in schutte.Plus]
le_psi_term_le [lemma, in gamma0.Gamma0]
Le_refl [lemma, in schutte.Well_Orders]
le_refl [lemma, in schutte.Schutte]
le_sup_members [lemma, in schutte.Schutte]
le_tail [lemma, in epsilon0.EPSILON0]
le_trans [lemma, in schutte.Schutte]
Le_trans [lemma, in schutte.Well_Orders]
le_trans [lemma, in gamma0.Gamma0]
le_trans [lemma, in epsilon0.EPSILON0]
le_zero [lemma, in schutte.Schutte]
le_zero_alpha [lemma, in gamma0.Gamma0]
le_zero_inv [lemma, in epsilon0.EPSILON0]
list_app_length [lemma, in prelude.more_list]
list_permut [library]
list_rec2 [definition, in prelude.more_list]
list_rec3 [definition, in prelude.more_list]
list_set [library]
list_size [definition, in prelude.more_list]
list_size_app [lemma, in prelude.more_list]
list_size_fold [lemma, in prelude.more_list]
list_size_size_eq [lemma, in prelude.more_list]
list_size_tl_compat [lemma, in prelude.more_list]
LLL [lemma, in schutte.AP]
log [definition, in schutte.AP]
log [definition, in epsilon0.EPSILON0]
log_nf [lemma, in epsilon0.EPSILON0]
log_ordinal [lemma, in schutte.AP]
LP [module, in rpo.rpo]
lt [inductive, in gamma0.Gamma0_prelude]
lt [definition, in hilbert.Paradoxical]
lt [definition, in schutte.Schutte]
lt [inductive, in epsilon0.EPSILON0]
ltM [definition, in epsilon0.MSE0]
ltM_app [lemma, in epsilon0.MSE0]
ltM_appR [lemma, in epsilon0.MSE0]
ltM_cons [lemma, in epsilon0.MSE0]
ltM_equiv_ltM [lemma, in epsilon0.MSE0]
ltM_equiv_ltMR [lemma, in epsilon0.MSE0]
ltM_head [lemma, in epsilon0.MSE0]
ltM_inv [lemma, in epsilon0.MSE0]
ltM_inv2 [lemma, in epsilon0.MSE0]
ltM_inv3 [lemma, in epsilon0.MSE0]
ltM_lt [lemma, in epsilon0.MSE0]
ltM_tail [lemma, in epsilon0.MSE0]
ltM_trans [lemma, in epsilon0.MSE0]
ltM_trans_1 [lemma, in epsilon0.MSE0]
ltM_trans_2 [lemma, in epsilon0.MSE0]
Lt_a [definition, in schutte.Well_Orders]
lt_a [definition, in schutte.Well_Orders]
lt_alpha_cons [lemma, in gamma0.Gamma0]
lt_alpha_psi [lemma, in gamma0.Gamma0]
lt_beta_cons [lemma, in gamma0.Gamma0]
lt_beta_psi [lemma, in gamma0.Gamma0]
lt_compat [lemma, in gamma0.Gamma0]
lt_compatR [lemma, in gamma0.Gamma0]
Lt_connect [lemma, in schutte.Well_Orders]
lt_cons_omega_inv [lemma, in gamma0.Gamma0]
lt_epsilon0 [inductive, in gamma0.Gamma0_prelude]
lt_ge_dec [definition, in gamma0.Gamma0]
lt_inv [lemma, in epsilon0.EPSILON0]
lt_inv_b [lemma, in epsilon0.EPSILON0]
lt_inv_le [lemma, in epsilon0.EPSILON0]
lt_inv_nb [lemma, in epsilon0.EPSILON0]
lt_irr [lemma, in epsilon0.EPSILON0]
lt_irr [lemma, in gamma0.Gamma0]
lt_irr [lemma, in schutte.Schutte]
lt_le [lemma, in schutte.Schutte]
lt_le_dec [definition, in epsilon0.EPSILON0]
Lt_Le_trans [lemma, in schutte.Well_Orders]
lt_le_trans [lemma, in gamma0.Gamma0]
lt_le_trans [lemma, in epsilon0.EPSILON0]
lt_le_trans [lemma, in schutte.Schutte]
lt_ltM [lemma, in epsilon0.MSE0]
lt_ltM2 [lemma, in epsilon0.MSE0]
lt_lt_Sn [lemma, in prelude.More_nat]
lt_not_gt [lemma, in epsilon0.EPSILON0]
Lt_not_Gt [lemma, in schutte.Well_Orders]
lt_not_le [lemma, in epsilon0.EPSILON0]
lt_not_wf [lemma, in epsilon0.EPSILON0]
lt_omega_finite [lemma, in schutte.Schutte]
lt_omega_inv [lemma, in gamma0.Gamma0]
lt_omega_is_finite [lemma, in gamma0.Gamma0]
lt_omega_limit [lemma, in schutte.Schutte]
lt_omega_limit_lt_exists_lt [lemma, in schutte.Schutte]
lt_one_inv [lemma, in gamma0.Gamma0]
lt_ordinal [lemma, in schutte.Schutte]
lt_or_ge [lemma, in schutte.Schutte]
lt_succ [lemma, in gamma0.Gamma0]
lt_succ [lemma, in schutte.Schutte]
lt_succ_le [lemma, in schutte.Schutte]
lt_succ_le [lemma, in gamma0.Gamma0]
lt_succ_le_2 [lemma, in schutte.Schutte]
lt_succ_lt [lemma, in schutte.Schutte]
lt_sup_exists_leq [lemma, in schutte.Schutte]
lt_sup_exists_lt [lemma, in schutte.Schutte]
lt_tail [lemma, in gamma0.Gamma0]
lt_tail0 [lemma, in gamma0.Gamma0]
lt_than_psi [lemma, in gamma0.Gamma0]
lt_trans [lemma, in epsilon0.EPSILON0]
lt_trans [lemma, in schutte.Schutte]
Lub [library]
L1 [lemma, in misc.G4]
L1 [lemma, in hilbert.more_relations]
L2 [lemma, in hilbert.more_relations]
L2 [lemma, in misc.G4]
L2 [lemma, in hilbert.Paradoxical]
L2' [lemma, in hilbert.Paradoxical]
L3 [lemma, in misc.G4]
L3 [lemma, in schutte.Ordering_Functions]
L3a [lemma, in schutte.Ordering_Functions]
L3' [lemma, in schutte.Ordering_Functions]
L4 [lemma, in misc.G4]
L4 [lemma, in hilbert.Paradoxical]
L5 [lemma, in hilbert.Paradoxical]
L5 [lemma, in misc.G4]
L55 [lemma, in hilbert.Paradoxical]
L66 [lemma, in hilbert.Paradoxical]
L_two_2 [lemma, in hilbert.Epsilon_Examples]
L_two_2' [lemma, in hilbert.Epsilon_Examples]


M

Make [module, in prelude.dickson]
Make [module, in prelude.list_set]
Make [module, in rpo.rpo]
Make [module, in rpo.term]
Make [module, in prelude.list_permut]
Make.context_multiset_extension_step_app1 [lemma, in prelude.dickson]
Make.context_multiset_extension_step_app2 [lemma, in prelude.dickson]
Make.context_trans_clos_multiset_extension_step_app1 [lemma, in prelude.dickson]
Make.dickson [lemma, in prelude.dickson]
Make.dickson_aux1 [lemma, in prelude.dickson]
Make.dickson_aux2 [lemma, in prelude.dickson]
Make.dickson_aux3 [lemma, in prelude.dickson]
Make.list_permut_acc [lemma, in prelude.dickson]
Make.list_permut_multiset_extension_step_1 [lemma, in prelude.dickson]
Make.list_permut_multiset_extension_step_2 [lemma, in prelude.dickson]
Make.multiset_closure [lemma, in prelude.dickson]
Make.multiset_extension_step [inductive, in prelude.dickson]
Make.rmv_case [constructor, in prelude.dickson]
Make.two_cases [lemma, in prelude.dickson]
map12_without_repetition [definition, in prelude.more_list]
map_app [lemma, in prelude.more_list]
map_map [lemma, in prelude.more_list]
map_without_repetition [definition, in prelude.more_list]
max [definition, in epsilon0.EPSILON0]
max' [definition, in epsilon0.EPSILON0]
max_le_regL [lemma, in prelude.More_nat]
max_le_regR [lemma, in prelude.More_nat]
members [definition, in schutte.Schutte]
members_eq [lemma, in schutte.Schutte]
members_omega [lemma, in schutte.Schutte]
members_proper [lemma, in schutte.Ordering_Functions]
minimal [definition, in prelude.wf_minimal]
minimal_exists [lemma, in prelude.wf_minimal]
minus [definition, in schutte.Minus]
Minus [library]
minus_a_a [lemma, in schutte.Minus]
minus_a_zero [lemma, in schutte.Minus]
minus_defined [lemma, in schutte.Minus]
minus_exists [lemma, in schutte.Plus]
minus_le [lemma, in schutte.Minus]
minus_nf [lemma, in epsilon0.E0_ARITH]
mk_cnf_of [constructor, in schutte.CNF]
more_list [library]
More_nat [library]
more_relations [library]
MSE0 [library]
multiplicity [definition, in epsilon0.MSE0]
multiplicity_of_app [lemma, in epsilon0.MSE0]
multiplicity_rw1 [lemma, in epsilon0.MSE0]
multiplicity_rw2 [lemma, in epsilon0.MSE0]
mult_nf [lemma, in epsilon0.E0_ARITH]
my_pred [definition, in hilbert.Epsilon_Examples]


N

nat_double_or_s_double [lemma, in denumerable.Arith_lemmas]
nat_segment [definition, in hilbert.Enumeration]
nbterms [definition, in gamma0.Gamma0_length]
nb_occ [definition, in prelude.more_list]
nb_occ_app [lemma, in prelude.more_list]
next [definition, in misc.G4]
nexts [definition, in misc.G4]
nexts_ok [lemma, in misc.G4]
nexts_ok_R [lemma, in misc.G4]
nexts_plus [lemma, in misc.G4]
next_unicity [lemma, in misc.G4]
nf [inductive, in gamma0.Gamma0_prelude]
nf [inductive, in epsilon0.EPSILON0]
nfs [inductive, in epsilon0.MSE0]
nfs_cons [constructor, in epsilon0.MSE0]
nfs_nil [constructor, in epsilon0.MSE0]
nfs_to_nf [lemma, in epsilon0.MSE0]
nf2 [inductive, in epsilon0.EPSILON0]
nf2_c [constructor, in epsilon0.EPSILON0]
nf2_intro [lemma, in epsilon0.EPSILON0]
nf2_phi0 [lemma, in epsilon0.EPSILON0]
nf2_phi0R [lemma, in epsilon0.EPSILON0]
nf2_z [constructor, in epsilon0.EPSILON0]
nf_a [lemma, in gamma0.Gamma0]
nf_b [lemma, in gamma0.Gamma0]
nf_bounded [lemma, in schutte.CNF]
nf_c [lemma, in gamma0.Gamma0]
nf_coeff_irrelevance [lemma, in epsilon0.EPSILON0]
nf_epsilon [lemma, in gamma0.Gamma0]
nf_epsilon0 [lemma, in gamma0.Gamma0]
nf_finite_inv [lemma, in gamma0.Gamma0]
nf_intro [lemma, in epsilon0.EPSILON0]
nf_inv1 [lemma, in epsilon0.EPSILON0]
nf_inv2 [lemma, in epsilon0.EPSILON0]
nf_inv_tail [lemma, in gamma0.Gamma0]
nf_multiplicity_big [lemma, in epsilon0.MSE0]
nf_multiplicity_head [lemma, in epsilon0.MSE0]
nf_multiplicity_tail [lemma, in epsilon0.MSE0]
nf_nfs [lemma, in epsilon0.MSE0]
nf_of_finite [lemma, in epsilon0.EPSILON0]
nf_omega [lemma, in gamma0.Gamma0]
nf_omega [lemma, in epsilon0.EPSILON0]
nf_phi0 [lemma, in epsilon0.EPSILON0]
nf_rect [definition, in epsilon0.EPSILON0]
nf_subterm [lemma, in gamma0.Gamma0]
nf_tail_lt_nf [lemma, in epsilon0.EPSILON0]
nf_tower [lemma, in epsilon0.EPSILON0]
nf_to_nfs [lemma, in epsilon0.MSE0]
nf_unicity [lemma, in epsilon0.MSE0]
nil [definition, in schutte.CNF]
nil [constructor, in schutte.CNF]
nil_forall [constructor, in schutte.CNF]
node [constructor, in epsilon0.Hydra]
NoneT [constructor, in hilbert.PartialFun]
none_nb_occ_O [lemma, in prelude.more_list]
Non_denum [lemma, in schutte.Schutte]
normal [inductive, in schutte.Ordering_Functions]
normal_intro [constructor, in schutte.Ordering_Functions]
normal_phi0 [lemma, in schutte.AP]
normal_plus_alpha [lemma, in schutte.Plus]
not_acc [lemma, in prelude.not_decreasing]
not_all_not_ex' [lemma, in prelude.wf_minimal]
not_AP_inv [lemma, in schutte.AP]
not_AP_inv2 [lemma, in schutte.AP]
not_decreasing [lemma, in prelude.not_decreasing]
not_decreasing [library]
not_decreasing_aux [lemma, in prelude.not_decreasing]
not_denumerable_unbounded [lemma, in schutte.Schutte]
not_double_is_s_double [lemma, in denumerable.Arith_lemmas]
not_gt_le [lemma, in schutte.Schutte]
not_is_limit_succ [lemma, in schutte.Schutte]
not_is_limit_zero [lemma, in schutte.Schutte]
not_is_succ_limit [lemma, in schutte.Schutte]
not_is_succ_zero [lemma, in schutte.Schutte]
not_lt_zero [lemma, in epsilon0.EPSILON0]
not_lt_zero [lemma, in schutte.Schutte]
not_lt_zero [lemma, in gamma0.Gamma0]
not_lt_zero_0 [lemma, in schutte.Schutte]
Not_Unbounded_bounded [lemma, in schutte.Schutte]
Not_Unbounded_denumerable [lemma, in schutte.Schutte]
Now [constructor, in epsilon0.Hydra]
nth_error_map [lemma, in prelude.more_list]
nth_error_ok_in [lemma, in prelude.more_list]
nth_item [definition, in misc.G4]


O

occurrence [definition, in epsilon0.Hydra]
of_beta' [lemma, in schutte.Ordering_Functions]
of_image [lemma, in schutte.Ordering_Functions]
of_u [lemma, in schutte.Plus]
OldEpsilon [library]
Olist [inductive, in schutte.CNF]
Omega [definition, in hilbert.Paradoxical]
omega [definition, in gamma0.Gamma0_prelude]
omega [definition, in schutte.Schutte]
omega [definition, in epsilon0.EPSILON0]
omega_limit [definition, in schutte.Schutte]
omega_lt_epsilon [lemma, in gamma0.Gamma0]
omega_lt_epsilon0 [lemma, in gamma0.Gamma0]
Omega_not_well_founded [lemma, in hilbert.Paradoxical]
omega_second_AP [lemma, in schutte.AP]
omega_term [definition, in epsilon0.EPSILON0]
omega_tower [definition, in epsilon0.EPSILON0]
Omega_well_founded [lemma, in hilbert.Paradoxical]
ON [axiom, in schutte.Schutte]
one [definition, in gamma0.Gamma0_prelude]
one_le_some_positive [lemma, in hilbert.Epsilon_Examples]
one_le_some_positive' [lemma, in hilbert.Epsilon_Examples]
one_le_some_positive2 [lemma, in hilbert.Epsilon_Examples]
one_plus_ge_omega [lemma, in schutte.Plus]
one_plus_omega [lemma, in schutte.Plus]
optionT [inductive, in hilbert.PartialFun]
opt_bijection [inductive, in hilbert.PartialFun]
opt_bij_i [constructor, in hilbert.PartialFun]
opt_codomain [definition, in hilbert.PartialFun]
opt_domain [definition, in hilbert.PartialFun]
opt_inj [definition, in hilbert.PartialFun]
opt_injection [inductive, in hilbert.PartialFun]
opt_inj_i [constructor, in hilbert.PartialFun]
opt_onto [definition, in hilbert.PartialFun]
opt_rel_same [definition, in hilbert.PartialFun]
Ordering_bijection [lemma, in schutte.Ordering_Functions]
ordering_function [definition, in schutte.Ordering_Functions]
Ordering_Functions [library]
ordering_function_mono [lemma, in schutte.Ordering_Functions]
ordering_function_monoR [lemma, in schutte.Ordering_Functions]
ordering_function_mono_weak [lemma, in schutte.Ordering_Functions]
ordering_function_mono_weakR [lemma, in schutte.Ordering_Functions]
ordering_function_ordA [lemma, in schutte.Ordering_Functions]
ordering_function_ordB [lemma, in schutte.Ordering_Functions]
ordering_function_ordinal_B [lemma, in schutte.Ordering_Functions]
ordering_function_seg [lemma, in schutte.Ordering_Functions]
ordering_function_segment [definition, in schutte.Ordering_Functions]
ordering_function_seg_unicity [lemma, in schutte.Ordering_Functions]
ordering_function_unicity [lemma, in schutte.Ordering_Functions]
ordering_le [lemma, in schutte.Ordering_Functions]
ordering_segment_2_fun [definition, in schutte.Ordering_Functions]
ordering_segment_2_fun_ok [lemma, in schutte.Ordering_Functions]
ordering_unbounded_unbounded [lemma, in schutte.Ordering_Functions]
order_function_least_least [lemma, in schutte.Ordering_Functions]
ordinal [definition, in schutte.Schutte]
ordinal_finite [lemma, in schutte.Schutte]
ordinal_finite [lemma, in gamma0.Gamma0]
ordinal_finite [lemma, in epsilon0.EPSILON0]
ordinal_omega [lemma, in schutte.Schutte]
ordinal_omega_limit [lemma, in schutte.Schutte]
ordinal_O_segment [lemma, in schutte.Ordering_Functions]
ordinal_phi0 [lemma, in schutte.AP]
ordinal_plus [lemma, in schutte.Plus]
ordinal_succ [lemma, in schutte.Schutte]
ordinal_sup_members [lemma, in schutte.Schutte]
ordinal_zero [lemma, in schutte.Schutte]
or_sumbool [definition, in hilbert.BadEpsilon2]
or_to_sum [lemma, in hilbert.OldEpsilon]
or_to_sum [lemma, in hilbert.Epsilon]
OT [definition, in schutte.Schutte]
o_bounded [definition, in schutte.CNF]
o_bounded_leq [definition, in schutte.CNF]
o_forall [inductive, in schutte.CNF]
o_length [definition, in prelude.more_list]
O_segment [definition, in schutte.Ordering_Functions]
O_segment_lt [lemma, in schutte.Ordering_Functions]
O_segment_lt_closed [lemma, in schutte.Ordering_Functions]
O_segment_ordinal [lemma, in schutte.Ordering_Functions]
O_segment_unbounded [lemma, in schutte.Ordering_Functions]


P

P [module, in rpo.rpo]
paradox [lemma, in hilbert.diag]
paradox [lemma, in hilbert.Paradoxical]
Paradoxical [definition, in hilbert.Paradoxical]
Paradoxical [library]
paraphrase [lemma, in hilbert.Paradoxical]
PartialFix [library]
PartialFun [library]
partial_fun_induction [definition, in prelude.PartialFix]
Permut [module, in prelude.list_permut]
Permut.DS.elt [definition, in prelude.list_permut]
Permut.DS.eq_elt_dec [definition, in prelude.list_permut]
Permut.DS.list_permut [definition, in prelude.list_permut]
Permut.DS.list_to_multiset [definition, in prelude.list_permut]
Permut.DS.Make.ac_syntactic [lemma, in prelude.list_permut]
Permut.DS.Make.ac_syntactic_aux [lemma, in prelude.list_permut]
Permut.DS.Make.cons_permut_in [lemma, in prelude.list_permut]
Permut.DS.Make.context_list_permut_app1 [lemma, in prelude.list_permut]
Permut.DS.Make.context_list_permut_app2 [lemma, in prelude.list_permut]
Permut.DS.Make.context_list_permut_cons [lemma, in prelude.list_permut]
Permut.DS.Make.elt [definition, in prelude.list_permut]
Permut.DS.Make.eq_elt_dec [definition, in prelude.list_permut]
Permut.DS.Make.in_mult_S [lemma, in prelude.list_permut]
Permut.DS.Make.in_permut_in [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut [definition, in prelude.list_permut]
Permut.DS.Make.list_permut_add_cons_inside [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_add_inside [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_app_app [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_dec [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_length [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_length_1 [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_length_2 [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_map [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_nil [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_refl [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_remove_hd [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_size [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_sym [lemma, in prelude.list_permut]
Permut.DS.Make.list_permut_trans [lemma, in prelude.list_permut]
Permut.DS.Make.list_to_multiset [definition, in prelude.list_permut]
Permut.DS.Make.multiplicity_app [lemma, in prelude.list_permut]
Permut.DS.Make.out_mult_O [lemma, in prelude.list_permut]
Permut.DS.Make.remove_context_list_permut_app2 [lemma, in prelude.list_permut]
Permut.DS.Make.remove_context_list_permut_cons [lemma, in prelude.list_permut]
PFix [definition, in prelude.PartialFix]
PFix_eq [lemma, in prelude.PartialFix]
PFix_F_eq [lemma, in prelude.PartialFix]
PFix_F_inv [lemma, in prelude.PartialFix]
phi0 [definition, in schutte.AP]
phi0 [definition, in epsilon0.EPSILON0]
phi0_alpha_phi0_beta [lemma, in schutte.AP]
phi0_elim [lemma, in schutte.AP]
phi0_inj [lemma, in schutte.AP]
phi0_log_le [lemma, in schutte.AP]
phi0_mono [lemma, in schutte.AP]
phi0_mono_R [lemma, in schutte.AP]
phi0_mono_R_weak [lemma, in schutte.AP]
phi0_mono_weak [lemma, in schutte.AP]
phi0_of_limit [lemma, in schutte.AP]
phi0_ordering [lemma, in schutte.AP]
phi0_positive [lemma, in schutte.AP]
phi0_sup [lemma, in schutte.AP]
phi0_zero [lemma, in schutte.AP]
plus [definition, in schutte.Plus]
plus [definition, in gamma0.Gamma0]
Plus [library]
plus_alpha_0 [lemma, in gamma0.Gamma0]
plus_assoc [lemma, in schutte.Plus]
plus_assoc [lemma, in epsilon0.E0_ARITH]
plus_assoc' [lemma, in schutte.Plus]
plus_assoc0 [lemma, in epsilon0.E0_ARITH]
plus_assoc1 [lemma, in schutte.Plus]
plus_assoc2 [lemma, in schutte.Plus]
plus_assoc3 [lemma, in schutte.Plus]
plus_elim [lemma, in schutte.Plus]
plus_FF [lemma, in schutte.Plus]
plus_limit [lemma, in schutte.Plus]
plus_lt_phi0 [lemma, in schutte.AP]
plus_minus [lemma, in schutte.Minus]
plus_mono_r [lemma, in schutte.Plus]
plus_mono_r_weak [lemma, in schutte.Plus]
plus_mono_weak_l [lemma, in schutte.Plus]
plus_of_succ [lemma, in schutte.Plus]
plus_ordering [lemma, in schutte.Plus]
plus_reg_r [lemma, in schutte.Plus]
plus_2 [lemma, in denumerable.Arith_lemmas]
power [definition, in misc.G4]
power [definition, in prelude.More_nat]
power_of_1 [lemma, in prelude.More_nat]
ppred [definition, in hilbert.Epsilon_Examples]
prec [axiom, in rpo.rpo]
Precedence [module, in rpo.rpo]
Precedence.Lex [constructor, in rpo.rpo]
Precedence.Mul [constructor, in rpo.rpo]
Precedence.status_type [inductive, in rpo.rpo]
prec_antisym [axiom, in rpo.rpo]
prec_dec [axiom, in rpo.rpo]
prec_transitive [axiom, in rpo.rpo]
pred [definition, in gamma0.Gamma0_prelude]
Pred [definition, in epsilon0.Goodstein]
PredF [definition, in epsilon0.Goodstein]
pred2 [definition, in hilbert.Epsilon_Examples]
pred2_lt [lemma, in hilbert.Epsilon_Examples]
pred_defined [lemma, in epsilon0.E0_ARITH]
pred_nf [lemma, in epsilon0.E0_ARITH]
pred_n_zero [definition, in epsilon0.Goodstein]
pred_of_power [lemma, in prelude.More_nat]
pred_of_succ [lemma, in epsilon0.E0_ARITH]
Pred_omega_a [definition, in epsilon0.Goodstein]
Pred_omega_an [definition, in epsilon0.Goodstein]
Pred_omega_anb [definition, in epsilon0.Goodstein]
pred_spec [definition, in epsilon0.Goodstein]
pred_42 [lemma, in hilbert.Epsilon_Examples]
progressive [definition, in schutte.Schutte]
Proper_A [lemma, in schutte.Ordering_Functions]
proper_members [lemma, in schutte.Ordering_Functions]
proper_O_segment [definition, in schutte.Ordering_Functions]
proper_segment_of [definition, in schutte.Ordering_Functions]
proper_segment_ordinals [lemma, in schutte.Ordering_Functions]
Prop_dec [definition, in hilbert.OldEpsilon]
prop_map12_without_repetition [lemma, in prelude.more_list]
prop_map_without_repetition [lemma, in prelude.more_list]
psi [definition, in gamma0.Gamma0_prelude]
psi_eq [lemma, in gamma0.Gamma0_prelude]
psi_le_cons [lemma, in gamma0.Gamma0]
psi_relevance [lemma, in gamma0.Gamma0]
psi_term [definition, in gamma0.Gamma0_prelude]
P_well_founded_induction_type [definition, in prelude.AccP]


Q

quasi_classic [lemma, in hilbert.OldEpsilon]
quo [definition, in hilbert.euclid]
quo' [definition, in hilbert.euclid]


R

reachable [definition, in misc.G4]
reachable_Rgstar [lemma, in misc.G4]
reduce_assoc_list [lemma, in prelude.more_list]
Rel [inductive, in SCHROEDER.Functions]
rel_bijection [inductive, in hilbert.PartialFun]
rel_bij_i [constructor, in hilbert.PartialFun]
rel_codomain [definition, in hilbert.PartialFun]
rel_domain [definition, in hilbert.PartialFun]
rel_enumerates [definition, in denumerable.Denumerable]
rel_functional [definition, in hilbert.PartialFun]
rel_inj [definition, in hilbert.PartialFun]
rel_injection [inductive, in denumerable.GRelations]
rel_injection [inductive, in hilbert.PartialFun]
rel_inj_i [constructor, in denumerable.GRelations]
rel_inj_i [constructor, in hilbert.PartialFun]
Rel_intro [constructor, in SCHROEDER.Functions]
rel_inv [definition, in hilbert.PartialFun]
rel_inv_bij [lemma, in hilbert.PartialFun]
rel_isotonic [definition, in schutte.Well_Orders]
rel_mono [definition, in schutte.Well_Orders]
rel_numbers [definition, in denumerable.Denumerable]
rel_onto [definition, in hilbert.PartialFun]
rel_surjection [inductive, in denumerable.GRelations]
rel_surj_i [constructor, in denumerable.GRelations]
remove [definition, in prelude.more_list]
remove_list [definition, in prelude.more_list]
replace_at_pos_is_replace_at_pos1 [axiom, in rpo.term]
replace_at_pos_is_replace_at_pos2 [axiom, in rpo.term]
replace_at_pos_list_replace_at_pos_in_subterm [axiom, in rpo.term]
replace_at_pos_unfold [axiom, in rpo.term]
replicate [definition, in epsilon0.Hydra]
restrict [definition, in prelude.AccP]
restrict [definition, in schutte.Well_Orders]
restricted_epsilon_extensionality [definition, in hilbert.OldEpsilon]
restricted_epsilon_extensionality [definition, in hilbert.Epsilon]
Rg [inductive, in epsilon0.Goodstein]
Rg [inductive, in misc.G4]
Rgstar [definition, in misc.G4]
Rg0 [constructor, in misc.G4]
Rg1 [constructor, in misc.G4]
Rg2 [constructor, in misc.G4]
Rg_i [constructor, in epsilon0.Goodstein]
Rh [inductive, in epsilon0.Hydra]
Rh_decrease [lemma, in epsilon0.Hydra]
Rh_head [lemma, in epsilon0.Hydra]
Rn [inductive, in epsilon0.Hydra]
Rnl_rest [constructor, in epsilon0.Hydra]
Rn_decrease [lemma, in epsilon0.Hydra]
Rn_head [lemma, in epsilon0.Hydra]
Rn_here [constructor, in epsilon0.Hydra]
Rn_plus [constructor, in epsilon0.Hydra]
RPO [module, in rpo.rpo]
rpo [library]
RPO.T.P.A [definition, in rpo.rpo]
RPO.T.P.LP.DS [definition, in rpo.rpo]
RPO.T.P.LP.Eq [constructor, in rpo.rpo]
RPO.T.P.LP.List_eq [constructor, in rpo.rpo]
RPO.T.P.LP.List_gt [constructor, in rpo.rpo]
RPO.T.P.LP.List_mul [constructor, in rpo.rpo]
RPO.T.P.LP.Lt [constructor, in rpo.rpo]
RPO.T.P.LP.Make.A [definition, in rpo.rpo]
RPO.T.P.LP.Make.acc_build [lemma, in rpo.rpo]
RPO.T.P.LP.Make.acc_lex_drop_proof [lemma, in rpo.rpo]
RPO.T.P.LP.Make.build_list_of_SN_terms [definition, in rpo.rpo]
RPO.T.P.LP.Make.Eq [constructor, in rpo.rpo]
RPO.T.P.LP.Make.in_sn_sn [lemma, in rpo.rpo]
RPO.T.P.LP.Make.lex1 [lemma, in rpo.rpo]
RPO.T.P.LP.Make.lex1_bis [lemma, in rpo.rpo]
RPO.T.P.LP.Make.lex2 [lemma, in rpo.rpo]
RPO.T.P.LP.Make.lex3 [lemma, in rpo.rpo]
RPO.T.P.LP.Make.List_eq [constructor, in rpo.rpo]
RPO.T.P.LP.Make.List_eq_rest [constructor, in rpo.rpo]
RPO.T.P.LP.Make.List_gt [constructor, in rpo.rpo]
RPO.T.P.LP.Make.List_gt_rest [constructor, in rpo.rpo]
RPO.T.P.LP.Make.List_mul [constructor, in rpo.rpo]
RPO.T.P.LP.Make.List_mul_rest [constructor, in rpo.rpo]
RPO.T.P.LP.Make.List_mul_rest_step [constructor, in rpo.rpo]
RPO.T.P.LP.Make.list_permut_map_acc [lemma, in rpo.rpo]
RPO.T.P.LP.Make.Lt [constructor, in rpo.rpo]
RPO.T.P.LP.Make.o_size [definition, in rpo.rpo]
RPO.T.P.LP.Make.o_size2 [definition, in rpo.rpo]
RPO.T.P.LP.Make.o_size3 [definition, in rpo.rpo]
RPO.T.P.LP.Make.o_size3_trans [lemma, in rpo.rpo]
RPO.T.P.LP.Make.projection_list_of_SN_terms [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo [inductive, in rpo.rpo]
RPO.T.P.LP.Make.rpo_add_context [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo_closure [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo_eq [inductive, in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex [inductive, in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex_rest [inductive, in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex_rest_same_length [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex_same_length [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul [inductive, in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul_rest [inductive, in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul_rest_step [inductive, in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul_trans_clos [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo_rest [definition, in rpo.rpo]
RPO.T.P.LP.Make.rpo_subst [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo_subterm [lemma, in rpo.rpo]
RPO.T.P.LP.Make.rpo_term [definition, in rpo.rpo]
RPO.T.P.LP.Make.rpo_trans [lemma, in rpo.rpo]
RPO.T.P.LP.Make.size2 [definition, in rpo.rpo]
RPO.T.P.LP.Make.size3 [definition, in rpo.rpo]
RPO.T.P.LP.Make.SN_term [inductive, in rpo.rpo]
RPO.T.P.LP.Make.Subterm [constructor, in rpo.rpo]
RPO.T.P.LP.Make.Top_eq_lex [constructor, in rpo.rpo]
RPO.T.P.LP.Make.Top_eq_mul [constructor, in rpo.rpo]
RPO.T.P.LP.Make.Top_gt [constructor, in rpo.rpo]
RPO.T.P.LP.Make.two_cases_rpo [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_on_lex_rest [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_on_mul_rest [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_on_rest [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_rpo [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_rpo_term [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_size [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_size2 [lemma, in rpo.rpo]
RPO.T.P.LP.Make.wf_size3 [lemma, in rpo.rpo]
RPO.T.P.LP.rpo [inductive, in rpo.rpo]
RPO.T.P.LP.rpo_eq [inductive, in rpo.rpo]
RPO.T.P.LP.rpo_lex [inductive, in rpo.rpo]
RPO.T.P.LP.rpo_mul [inductive, in rpo.rpo]
RPO.T.P.LP.Subterm [constructor, in rpo.rpo]
RPO.T.P.LP.Top_eq_lex [constructor, in rpo.rpo]
RPO.T.P.LP.Top_eq_mul [constructor, in rpo.rpo]
RPO.T.P.LP.Top_gt [constructor, in rpo.rpo]
rpo_add_context [axiom, in rpo.rpo]
rpo_closure [axiom, in rpo.rpo]
rpo_subst [axiom, in rpo.rpo]
rpo_trans [axiom, in rpo.rpo]
R1 [definition, in schutte.Ordering_Functions]
R1 [inductive, in epsilon0.Hydra]
R1_decrease [lemma, in epsilon0.Hydra]
R1_head [lemma, in epsilon0.Hydra]
R1_node [constructor, in epsilon0.Hydra]
R1_single [constructor, in epsilon0.Hydra]
R2 [lemma, in hilbert.Paradoxical]
r2f [definition, in hilbert.PartialFun]
r2f_ok [lemma, in hilbert.PartialFun]
r2i [definition, in hilbert.PartialFun]
r2i_ok [lemma, in hilbert.PartialFun]
R_inclusion_codomain [lemma, in denumerable.Denumerable]
R_inclusion_domain [lemma, in denumerable.Denumerable]
R_inclusion_enumerates [lemma, in denumerable.Denumerable]
R_inclusion_inj [lemma, in denumerable.Denumerable]
R_inv [definition, in denumerable.GRelations]
R_inv_inj [lemma, in denumerable.GRelations]
R_inv_surj [lemma, in denumerable.GRelations]
R_nat_elaguee [definition, in denumerable.GRelations]
R_nat_elaguee_domain [lemma, in denumerable.GRelations]
R_nat_elaguee_fun [lemma, in denumerable.GRelations]
R_union [inductive, in denumerable.Denumerable]
R_union_codomain [lemma, in denumerable.Denumerable]
R_union_domain [lemma, in denumerable.Denumerable]
R_union_enumerates [lemma, in denumerable.Denumerable]
R_union_inj [lemma, in denumerable.Denumerable]
R_union_qcq [definition, in denumerable.Denumerable]
R_union_qcq_codomain [lemma, in denumerable.Denumerable]
R_union_qcq_domain [lemma, in denumerable.Denumerable]
R_union_qcq_inj [lemma, in denumerable.Denumerable]
R_union_qcq_numbers [lemma, in denumerable.Denumerable]


S

S [module, in prelude.list_set]
S [module, in prelude.decidable_set]
Schroeder [lemma, in SCHROEDER.Schroeder]
Schroeder [library]
Schutte [library]
segment_bound [inductive, in hilbert.Enumeration]
seq_mono [definition, in schutte.Schutte]
seq_mono_inj [lemma, in schutte.Schutte]
seq_mono_intro [lemma, in schutte.Schutte]
seq_range [definition, in denumerable.Denumerable]
seq_range [definition, in hilbert.Enumeration]
seq_range_denumerable [lemma, in denumerable.Denumerable]
seq_range_denumerable [lemma, in schutte.Schutte]
seq_range_enumeration [lemma, in hilbert.Enumeration]
seq_range_opt [definition, in hilbert.Enumeration]
Setminus_contravariant [lemma, in SCHROEDER.Setminus_fact]
Setminus_fact [library]
set_eq [definition, in schutte.Schutte]
Set_Sum [inductive, in SCHROEDER.Sums]
Set_Sum_intro [constructor, in SCHROEDER.Sums]
Set_Sum_is_majoring [lemma, in SCHROEDER.Sums]
Set_Sum_is_minoring [lemma, in SCHROEDER.Sums]
SF27 [lemma, in misc.G4]
SF3 [lemma, in misc.G4]
Sh [inductive, in epsilon0.Hydra]
shift_n_omega_l [definition, in prelude.bintree]
shift_n_omega_r [definition, in prelude.bintree]
Sh_head [lemma, in epsilon0.Hydra]
Sh_1 [constructor, in epsilon0.Hydra]
Sh_2 [constructor, in epsilon0.Hydra]
Sh_3 [constructor, in epsilon0.Hydra]
Signature [module, in rpo.term]
Signature.AC [constructor, in rpo.term]
Signature.arity_type [inductive, in rpo.term]
Signature.C [constructor, in rpo.term]
Signature.Free [constructor, in rpo.term]
single [constructor, in epsilon0.Hydra]
single [definition, in epsilon0.Hydra]
single [definition, in epsilon0.Hydra]
single_nf [constructor, in epsilon0.EPSILON0]
single_nf [constructor, in gamma0.Gamma0_prelude]
size_direct_subterm [axiom, in rpo.term]
size_ge_one [axiom, in rpo.term]
size_subterm_at_pos [axiom, in rpo.term]
size_unfold [axiom, in rpo.term]
Sn [inductive, in epsilon0.Hydra]
Sn_first [constructor, in epsilon0.Hydra]
Sn_single [constructor, in epsilon0.Hydra]
some [definition, in hilbert.Epsilon]
some [definition, in hilbert.OldEpsilon]
Some [definition, in gamma0.Gamma0_prelude]
SomeT [constructor, in hilbert.PartialFun]
some_e [lemma, in hilbert.OldEpsilon]
some_e [lemma, in hilbert.Epsilon]
some_fun [definition, in hilbert.OldEpsilon]
some_fun [definition, in hilbert.Epsilon]
some_fun_e [lemma, in hilbert.OldEpsilon]
some_fun_e [lemma, in hilbert.Epsilon]
some_fun_ind [lemma, in hilbert.Epsilon]
some_fun_ind [lemma, in hilbert.OldEpsilon]
some_ind [lemma, in hilbert.Epsilon]
some_ind [lemma, in hilbert.OldEpsilon]
some_lt [definition, in hilbert.Epsilon_Examples]
some_nb_occ_Sn [lemma, in prelude.more_list]
some_positive [definition, in hilbert.Epsilon_Examples]
sort [definition, in epsilon0.MSE0]
sorted [inductive, in schutte.CNF]
sortedn [constructor, in schutte.CNF]
sorted0 [constructor, in schutte.CNF]
sorted1 [constructor, in schutte.CNF]
sorted_lt [lemma, in schutte.CNF]
sorted_lt_lt [lemma, in schutte.CNF]
sorted_lt_lt_2 [lemma, in schutte.CNF]
sorted_tail [lemma, in schutte.CNF]
sort_aux [definition, in epsilon0.MSE0]
sort_aux_equiv [lemma, in epsilon0.MSE0]
sort_aux_nf [lemma, in epsilon0.MSE0]
sort_equiv [lemma, in epsilon0.MSE0]
sort_nf [lemma, in epsilon0.MSE0]
split_list [definition, in prelude.more_list]
split_list_app_cons [lemma, in prelude.more_list]
star [definition, in hilbert.Paradoxical]
star_com [lemma, in hilbert.Paradoxical]
status [axiom, in rpo.rpo]
subst_comp_is_subst_comp [axiom, in rpo.term]
subst_comp_is_subst_comp_aux1 [axiom, in rpo.term]
subterm [inductive, in gamma0.Gamma0]
subterm_a [constructor, in gamma0.Gamma0]
subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [axiom, in rpo.term]
subterm_b [constructor, in gamma0.Gamma0]
subterm_c [constructor, in gamma0.Gamma0]
subterm_lt [lemma, in gamma0.Gamma0]
subterm_trans [constructor, in gamma0.Gamma0]
succ [definition, in gamma0.Gamma0_prelude]
succ [definition, in schutte.Schutte]
succ_finite [constructor, in gamma0.Gamma0_prelude]
succ_injection [lemma, in schutte.Schutte]
succ_lt_le [lemma, in gamma0.Gamma0]
succ_mono [lemma, in schutte.Schutte]
succ_monoR [lemma, in schutte.Schutte]
succ_of_cons [lemma, in gamma0.Gamma0]
succ_rw [lemma, in schutte.Schutte]
succ_spec [definition, in schutte.Schutte]
succ_zero_diff [lemma, in schutte.Schutte]
Sums [library]
sup [definition, in schutte.Schutte]
sup_eq_intro [lemma, in schutte.Schutte]
sup_exists [lemma, in schutte.Schutte]
sup_least_upper_bound [lemma, in schutte.Schutte]
sup_members_disj [lemma, in schutte.Schutte]
sup_members_not_succ [lemma, in schutte.Schutte]
sup_members_succ [lemma, in schutte.Schutte]
sup_mono [lemma, in schutte.Schutte]
sup_M_in_B [lemma, in schutte.Ordering_Functions]
sup_of_leq [lemma, in schutte.Schutte]
sup_ordinal [lemma, in schutte.Schutte]
sup_spec [definition, in schutte.Schutte]
sup_unicity [lemma, in schutte.Schutte]
sup_upper_bound [lemma, in schutte.Schutte]
surjection [inductive, in SCHROEDER.Functions]
symb [axiom, in rpo.term]
S.DS.cardinal [definition, in prelude.list_set]
S.DS.elt [definition, in prelude.list_set]
S.DS.eq_elt_dec [definition, in prelude.list_set]
S.DS.Make.add [definition, in prelude.list_set]
S.DS.Make.add_comm [lemma, in prelude.list_set]
S.DS.Make.add_prf [lemma, in prelude.list_set]
S.DS.Make.add_without_red [definition, in prelude.list_set]
S.DS.Make.add_1 [lemma, in prelude.list_set]
S.DS.Make.add_12 [lemma, in prelude.list_set]
S.DS.Make.add_2 [lemma, in prelude.list_set]
S.DS.Make.cardinal [definition, in prelude.list_set]
S.DS.Make.cardinal_eq_set [lemma, in prelude.list_set]
S.DS.Make.cardinal_subset [lemma, in prelude.list_set]
S.DS.Make.cardinal_union [lemma, in prelude.list_set]
S.DS.Make.cardinal_union_inter_12 [lemma, in prelude.list_set]
S.DS.Make.cardinal_union_1 [lemma, in prelude.list_set]
S.DS.Make.cardinal_union_2 [lemma, in prelude.list_set]
S.DS.Make.elt [definition, in prelude.list_set]
S.DS.Make.empty [definition, in prelude.list_set]
S.DS.Make.eq_elt_dec [definition, in prelude.list_set]
S.DS.Make.eq_set [definition, in prelude.list_set]
S.DS.Make.eq_set_dec [lemma, in prelude.list_set]
S.DS.Make.eq_set_list_permut_support [lemma, in prelude.list_set]
S.DS.Make.eq_set_refl [lemma, in prelude.list_set]
S.DS.Make.eq_set_sym [lemma, in prelude.list_set]
S.DS.Make.eq_set_trans [lemma, in prelude.list_set]
S.DS.Make.filter [definition, in prelude.list_set]
S.DS.Make.filter_aux [definition, in prelude.list_set]
S.DS.Make.filter_union [lemma, in prelude.list_set]
S.DS.Make.filter_1 [lemma, in prelude.list_set]
S.DS.Make.filter_1_list [lemma, in prelude.list_set]
S.DS.Make.filter_2 [lemma, in prelude.list_set]
S.DS.Make.filter_2_list [lemma, in prelude.list_set]
S.DS.Make.included_filter_aux [lemma, in prelude.list_set]
S.DS.Make.included_remove_red [lemma, in prelude.list_set]
S.DS.Make.inter [definition, in prelude.list_set]
S.DS.Make.inter_1 [lemma, in prelude.list_set]
S.DS.Make.inter_12 [lemma, in prelude.list_set]
S.DS.Make.inter_12_aux [lemma, in prelude.list_set]
S.DS.Make.inter_1_aux [lemma, in prelude.list_set]
S.DS.Make.inter_2 [lemma, in prelude.list_set]
S.DS.Make.inter_2_aux [lemma, in prelude.list_set]
S.DS.Make.make_set [definition, in prelude.list_set]
S.DS.Make.mem [definition, in prelude.list_set]
S.DS.Make.mem_dec [lemma, in prelude.list_set]
S.DS.Make.remove_not_common [definition, in prelude.list_set]
S.DS.Make.remove_red [definition, in prelude.list_set]
S.DS.Make.remove_red_included [lemma, in prelude.list_set]
S.DS.Make.singleton [definition, in prelude.list_set]
S.DS.Make.subset [definition, in prelude.list_set]
S.DS.Make.subset_cardinal_not_eq_not_eq_set [lemma, in prelude.list_set]
S.DS.Make.subset_compat [lemma, in prelude.list_set]
S.DS.Make.subset_compat_1 [lemma, in prelude.list_set]
S.DS.Make.subset_compat_2 [lemma, in prelude.list_set]
S.DS.Make.subset_dec [lemma, in prelude.list_set]
S.DS.Make.subset_filter [lemma, in prelude.list_set]
S.DS.Make.subset_inter_1 [lemma, in prelude.list_set]
S.DS.Make.subset_inter_2 [lemma, in prelude.list_set]
S.DS.Make.subset_subset_union [lemma, in prelude.list_set]
S.DS.Make.subset_union_1 [lemma, in prelude.list_set]
S.DS.Make.subset_union_2 [lemma, in prelude.list_set]
S.DS.Make.t [inductive, in prelude.list_set]
S.DS.Make.union [definition, in prelude.list_set]
S.DS.Make.union_assoc [lemma, in prelude.list_set]
S.DS.Make.union_comm [lemma, in prelude.list_set]
S.DS.Make.union_compat_eq_set [lemma, in prelude.list_set]
S.DS.Make.union_compat_subset_1 [lemma, in prelude.list_set]
S.DS.Make.union_compat_subset_2 [lemma, in prelude.list_set]
S.DS.Make.union_empty_1 [lemma, in prelude.list_set]
S.DS.Make.union_empty_2 [lemma, in prelude.list_set]
S.DS.Make.union_1 [lemma, in prelude.list_set]
S.DS.Make.union_12 [lemma, in prelude.list_set]
S.DS.Make.union_12_aux [lemma, in prelude.list_set]
S.DS.Make.union_1_aux [lemma, in prelude.list_set]
S.DS.Make.union_2 [lemma, in prelude.list_set]
S.DS.Make.union_2_aux [lemma, in prelude.list_set]
S.DS.Make.without_red [definition, in prelude.list_set]
S.DS.Make.without_red_add [lemma, in prelude.list_set]
S.DS.Make.without_red_add_without_red [lemma, in prelude.list_set]
S.DS.Make.without_red_filter_aux [lemma, in prelude.list_set]
S.DS.Make.without_red_nil [lemma, in prelude.list_set]
S.DS.Make.without_red_permut [lemma, in prelude.list_set]
S.DS.Make.without_red_remove [lemma, in prelude.list_set]
S.DS.Make.without_red_remove_not_common [lemma, in prelude.list_set]
S.DS.Make.without_red_remove_not_common_aux [lemma, in prelude.list_set]
S.DS.Make.without_red_remove_red [lemma, in prelude.list_set]
S.DS.Make.without_red_singleton [lemma, in prelude.list_set]
S.DS.subset [definition, in prelude.list_set]
S.DS.t [inductive, in prelude.list_set]
S.DS.without_red [definition, in prelude.list_set]
S1 [inductive, in epsilon0.Hydra]
S1_decrease [lemma, in epsilon0.Hydra]
S1_first [constructor, in epsilon0.Hydra]
S1_head [lemma, in epsilon0.Hydra]
S1_last [constructor, in epsilon0.Hydra]
S1_rest [constructor, in epsilon0.Hydra]
S2 [inductive, in epsilon0.Hydra]
S2_decrease [lemma, in epsilon0.Hydra]
S2_first [constructor, in epsilon0.Hydra]
S2_head [lemma, in epsilon0.Hydra]
S2_rest [constructor, in epsilon0.Hydra]
S2_single [constructor, in epsilon0.Hydra]


T

T [module, in rpo.rpo]
tail [definition, in gamma0.Gamma0_prelude]
tail_lt [constructor, in epsilon0.EPSILON0]
tail_lt_cons [lemma, in epsilon0.EPSILON0]
tau [definition, in hilbert.Epsilon]
Term [module, in rpo.term]
term [library]
Term.F.X.direct_subterm [definition, in rpo.term]
Term.F.X.size [definition, in rpo.term]
Term.F.X.symbol [definition, in rpo.term]
Term.F.X.term [inductive, in rpo.term]
Term.F.X.Term [constructor, in rpo.term]
Term.F.X.Term_eq_dec.A [definition, in rpo.term]
Term.F.X.Term_eq_dec.apply_subst [definition, in rpo.term]
Term.F.X.Term_eq_dec.eq_A_dec [definition, in rpo.term]
Term.F.X.Term_eq_dec.is_a_pos [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.DecVar.A [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.DecVar.eq_A_dec [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.symbol [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.variable [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.apply_subst [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.direct_subterm [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.DS [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.empty_subst_is_id [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.empty_subst_is_id_list [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.eq_term_dec [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.is_a_pos [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.is_a_pos_exists_subtem [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.map_subst [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_is_replace_at_pos1 [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_is_replace_at_pos2 [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_list [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_list_replace_at_pos_in_subterm [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_unfold [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_direct_subterm [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_ge_one [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_subterm_at_pos [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_unfold [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.substitution [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp_is_subst_comp [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp_is_subst_comp_aux1 [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp_is_subst_comp_aux2 [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subterm_at_pos [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term [inductive, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term [constructor, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.A [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.A [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.eq_A_dec [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.eq_A_dec [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec2 [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec3 [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec4 [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec7 [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec8 [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Var [constructor, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_apply_subst [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_fold [lemma, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_list [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_subst [definition, in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_unfold [lemma, in rpo.term]
Term.F.X.Term_eq_dec.map_subst [definition, in rpo.term]
Term.F.X.Term_eq_dec.replace_at_pos [definition, in rpo.term]
Term.F.X.Term_eq_dec.replace_at_pos_list [definition, in rpo.term]
Term.F.X.Term_eq_dec.substitution [definition, in rpo.term]
Term.F.X.Term_eq_dec.subst_comp [definition, in rpo.term]
Term.F.X.Term_eq_dec.subterm_at_pos [definition, in rpo.term]
Term.F.X.Term_eq_dec.well_formed [definition, in rpo.term]
Term.F.X.Term_eq_dec.well_formed_list [definition, in rpo.term]
Term.F.X.Term_eq_dec.well_formed_subst [definition, in rpo.term]
Term.F.X.Var [constructor, in rpo.term]
Term.F.X.variable [definition, in rpo.term]
Term_eq_dec [module, in rpo.term]
Term_eq_dec [module, in rpo.term]
term_rec2 [axiom, in rpo.term]
term_rec3 [axiom, in rpo.term]
term_rec4 [axiom, in rpo.term]
term_rec7 [axiom, in rpo.term]
term_rec8 [axiom, in rpo.term]
the [definition, in hilbert.OldEpsilon]
the [definition, in hilbert.Epsilon]
the_e [lemma, in hilbert.OldEpsilon]
the_e [lemma, in hilbert.Epsilon]
the_fun [definition, in hilbert.OldEpsilon]
the_fun [definition, in hilbert.Epsilon]
the_fun_e [lemma, in hilbert.Epsilon]
the_fun_e [lemma, in hilbert.OldEpsilon]
the_fun_ind [lemma, in hilbert.Epsilon]
the_fun_ind [lemma, in hilbert.OldEpsilon]
the_fun_rw [lemma, in hilbert.OldEpsilon]
the_fun_rw [lemma, in hilbert.Epsilon]
the_ind [lemma, in hilbert.Epsilon]
the_ind [lemma, in hilbert.OldEpsilon]
the_least [definition, in schutte.Schutte]
the_least_ok [lemma, in schutte.Schutte]
the_least_ordinal [lemma, in schutte.Schutte]
the_ordering_function [definition, in schutte.Ordering_Functions]
the_ordering_function_eq [lemma, in schutte.Ordering_Functions]
the_ordering_function_ok [lemma, in schutte.Ordering_Functions]
the_ordering_segment [definition, in schutte.Ordering_Functions]
the_rw [lemma, in hilbert.Epsilon]
the_rw [lemma, in hilbert.OldEpsilon]
Th_13_5_1 [lemma, in schutte.Ordering_Functions]
Th_13_5_2 [lemma, in schutte.Ordering_Functions]
TH_13_6 [lemma, in schutte.Ordering_Functions]
TH_13_6R [lemma, in schutte.Ordering_Functions]
Tools [library]
transitivity [lemma, in gamma0.Gamma0]
transitivity0 [lemma, in gamma0.Gamma0]
trans_aux [lemma, in gamma0.Gamma0]
trans_clos [inductive, in prelude.closure]
trans_clos_is_trans [lemma, in prelude.closure]
tree_nat [definition, in prelude.bintree]
trichotomy [lemma, in schutte.Schutte]
trichotomy_inf [definition, in epsilon0.EPSILON0]
trichotomy_inf [definition, in gamma0.Gamma0]
tricho_aux [lemma, in gamma0.Gamma0]
tricho_lt_2 [lemma, in gamma0.Gamma0]
tricho_lt_2' [lemma, in gamma0.Gamma0]
tricho_lt_3 [lemma, in gamma0.Gamma0]
tricho_lt_4 [lemma, in gamma0.Gamma0]
tricho_lt_4' [lemma, in gamma0.Gamma0]
tricho_lt_5 [lemma, in gamma0.Gamma0]
tricho_lt_7 [lemma, in gamma0.Gamma0]
two [definition, in hilbert.Epsilon_Examples]
T1 [inductive, in epsilon0.EPSILON0]
T1_eq_dec [definition, in epsilon0.EPSILON0]
T1_inj [definition, in gamma0.Gamma0_prelude]
T2 [inductive, in gamma0.Gamma0_prelude]
t_step [constructor, in prelude.closure]
t_trans [constructor, in prelude.closure]


U

Unbounded [definition, in schutte.Schutte]
unbounded [lemma, in schutte.Schutte]
Unbounded_Greater [lemma, in schutte.Plus]
Unbounded_not_denumerable [lemma, in schutte.Schutte]
unit [inductive, in prelude.bintree]
upper_bound [definition, in schutte.Lub]


V

val [definition, in epsilon0.Goodstein]
val_positive [lemma, in epsilon0.Goodstein]
var [axiom, in rpo.term]
Variables [module, in rpo.term]
Vars [module, in gamma0.Gamma0]
Vars [module, in epsilon0.EPSILON0]
Vars.empty_set [constructor, in epsilon0.EPSILON0]
Vars.empty_set [constructor, in gamma0.Gamma0]
Vars.empty_set [inductive, in epsilon0.EPSILON0]
Vars.empty_set [inductive, in gamma0.Gamma0]
Vars.eq_variable_dec [lemma, in epsilon0.EPSILON0]
Vars.eq_variable_dec [lemma, in gamma0.Gamma0]
void [constructor, in prelude.bintree]
VSet [module, in rpo.term]


W

well_formed_apply_subst [axiom, in rpo.term]
well_formed_fold [axiom, in rpo.term]
well_formed_unfold [axiom, in rpo.term]
well_founded [definition, in hilbert.Paradoxical]
well_founded_length [lemma, in prelude.more_list]
well_founded_P [definition, in prelude.AccP]
Well_Orders [library]
wf_lex [lemma, in rpo.rpo]
wf_minimal [library]
wf_rpo [axiom, in rpo.rpo]
wf_trans [lemma, in prelude.closure]
Winner [lemma, in epsilon0.Hydra]
WO [inductive, in schutte.Well_Orders]
WO_lt [inductive, in schutte.Well_Orders]
WO_lt_i [constructor, in schutte.Well_Orders]


X

X [module, in rpo.term]


Z

zero [definition, in gamma0.Gamma0_prelude]
zero [definition, in epsilon0.MSE0]
zero [definition, in gamma0.Gamma0_length]
zero [definition, in epsilon0.EPSILON0]
zero [definition, in hilbert.Epsilon_Examples]
zero [definition, in epsilon0.MSE0]
zero [constructor, in epsilon0.EPSILON0]
zero [definition, in gamma0.Gamma0_length]
zero [constructor, in gamma0.Gamma0_prelude]
zero [definition, in gamma0.Gamma0_length]
zero [definition, in schutte.Schutte]
zero [definition, in gamma0.Gamma0_prelude]
Zero_correct [constructor, in epsilon0.Goodstein]
zero_eq_0 [lemma, in hilbert.Epsilon_Examples]
zero_finite [constructor, in gamma0.Gamma0_prelude]
zero_le [lemma, in epsilon0.EPSILON0]
zero_lt [constructor, in epsilon0.EPSILON0]
zero_lt_e0 [constructor, in gamma0.Gamma0_prelude]
zero_lt_omega [lemma, in schutte.AP]
zero_lt_succ [lemma, in gamma0.Gamma0]
zero_lt_succ [lemma, in schutte.Schutte]
zero_nf [constructor, in gamma0.Gamma0_prelude]
zero_nf [constructor, in epsilon0.EPSILON0]
zero_or_greater [lemma, in schutte.Schutte]
zero_or_positive [lemma, in schutte.Schutte]
zero_plus_alpha [lemma, in schutte.Plus]
zero_spec [definition, in schutte.Schutte]


_

_A [definition, in schutte.Ordering_Functions]



Axiom Index

A

A [in prelude.decidable_set]
A [in rpo.rpo]
arity [in rpo.term]
AX2 [in schutte.Schutte]
AX3 [in schutte.Schutte]


C

cardinal_subset [in prelude.list_set]
constructive_indefinite_description [in hilbert.ClassicalEpsilonModified]


E

empty_subst_is_id [in rpo.term]
empty_subst_is_id_list [in rpo.term]
epsax [in hilbert.OldEpsilon]
epsilon [in hilbert.BadEpsilon2]
epsilon [in hilbert.OldEpsilon]
eq_A_dec [in prelude.decidable_set]
eq_symbol_dec [in rpo.term]
eq_term_dec [in rpo.term]
eq_variable_dec [in rpo.term]


I

inh_OT [in schutte.Schutte]
is_a_pos_exists_subtem [in rpo.term]


O

ON [in schutte.Schutte]


P

prec [in rpo.rpo]
prec_antisym [in rpo.rpo]
prec_dec [in rpo.rpo]
prec_transitive [in rpo.rpo]


R

replace_at_pos_is_replace_at_pos1 [in rpo.term]
replace_at_pos_is_replace_at_pos2 [in rpo.term]
replace_at_pos_list_replace_at_pos_in_subterm [in rpo.term]
replace_at_pos_unfold [in rpo.term]
rpo_add_context [in rpo.rpo]
rpo_closure [in rpo.rpo]
rpo_subst [in rpo.rpo]
rpo_trans [in rpo.rpo]


S

size_direct_subterm [in rpo.term]
size_ge_one [in rpo.term]
size_subterm_at_pos [in rpo.term]
size_unfold [in rpo.term]
status [in rpo.rpo]
subst_comp_is_subst_comp [in rpo.term]
subst_comp_is_subst_comp_aux1 [in rpo.term]
subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [in rpo.term]
symb [in rpo.term]


T

term_rec2 [in rpo.term]
term_rec3 [in rpo.term]
term_rec4 [in rpo.term]
term_rec7 [in rpo.term]
term_rec8 [in rpo.term]


V

var [in rpo.term]


W

well_formed_apply_subst [in rpo.term]
well_formed_fold [in rpo.term]
well_formed_unfold [in rpo.term]
wf_rpo [in rpo.rpo]



Lemma Index

A

accElim3 [in prelude.AccP]
AccElim3 [in prelude.AccP]
acc_imp [in prelude.not_decreasing]
acc_trans [in prelude.closure]
all_b_relation [in denumerable.Denumerable]
all_ord_acc [in schutte.Schutte]
alpha_A [in schutte.Ordering_Functions]
alpha_plus_sup [in schutte.Plus]
alpha_plus_zero [in schutte.Plus]
alpha_sup [in schutte.Ordering_Functions]
app_equiv_assoc [in epsilon0.MSE0]
app_equiv_comm [in epsilon0.MSE0]
AP_closed [in schutte.AP]
AP_finite_eq_one [in schutte.AP]
AP_Inc_ordinal [in schutte.AP]
AP_omega [in schutte.AP]
AP_one [in schutte.AP]
AP_o_segment [in schutte.AP]
AP_phi0 [in schutte.AP]
ap_phi0 [in epsilon0.EPSILON0]
ap_phi0R [in epsilon0.EPSILON0]
AP_plus_AP [in schutte.AP]
AP_plus_closed [in schutte.AP]
AP_sup [in schutte.AP]
AP_to_phi0 [in schutte.AP]
AP_unbounded [in schutte.AP]
arrow_disj [in hilbert.OldEpsilon]
A1_A2 [in schutte.Ordering_Functions]
A2_A1 [in schutte.Ordering_Functions]
A_closed [in schutte.Ordering_Functions]


B

Bells_lemma [in hilbert.OldEpsilon]
big_number_eq [in misc.G4]
bij [in prelude.bintree]
bijection_fun_rel [in hilbert.PartialFun]
bijection_rel_fun [in hilbert.PartialFun]
bijR [in prelude.bintree]
B_of [in schutte.Ordering_Functions]
B_of' [in schutte.Ordering_Functions]


C

choice [in hilbert.ClassicalEpsilonModified]
choice_fun_e [in hilbert.OldEpsilon]
choice_fun_e [in hilbert.Epsilon]
choice_fun_ind [in hilbert.Epsilon]
choice_fun_ind [in hilbert.OldEpsilon]
classical_indefinite_description [in hilbert.ClassicalEpsilonModified]
classification [in schutte.Schutte]
cnf_eq [in schutte.CNF]
cnf_exists [in schutte.CNF]
cnf_head_eq [in schutte.CNF]
cnf_of_ap [in schutte.CNF]
cnf_of_AP [in schutte.CNF]
cnf_plus [in schutte.CNF]
cnf_plus1 [in schutte.CNF]
cnf_plus2 [in schutte.CNF]
cnf_unicity [in schutte.CNF]
compare_eq_rw [in gamma0.Gamma0]
compare_gt_rw [in gamma0.Gamma0]
compare_lt_rw [in gamma0.Gamma0]
compare_reflect [in gamma0.Gamma0]
compare_rw_eq [in gamma0.Gamma0]
compare_rw_gt [in gamma0.Gamma0]
compare_rw_lt [in gamma0.Gamma0]
constructive_definite_description [in hilbert.ClassicalEpsilonModified]
correct_succ [in epsilon0.Goodstein]
critical_e [in schutte.Critical]
critical_eq [in schutte.Critical]
critical_extensional [in schutte.Critical]
Critical_incl [in schutte.Critical]
critical_lt [in schutte.Critical]
critical_ord [in schutte.Critical]
critical_pos [in schutte.Critical]
critical_pos_inv [in schutte.Critical]
critical_zero [in schutte.Critical]
critical_zero_inv [in schutte.Critical]
Cr_incl [in schutte.Critical]
Cr_incl' [in schutte.Critical]
Cr_pos [in schutte.Critical]
Cr_rw [in schutte.Critical]
Cr_zero [in schutte.Critical]
Cr_zero_AP [in schutte.Critical]
c_no_pred [in epsilon0.E0_ARITH]


D

dd' [in hilbert.OldEpsilon]
dd' [in hilbert.Epsilon]
dd'' [in hilbert.Epsilon]
dd'' [in hilbert.OldEpsilon]
denumerable_add [in hilbert.Enumeration]
denumerable_add_disj [in hilbert.Enumeration]
denumerable_bij_fun [in hilbert.Enumeration]
denumerable_bij_fun [in denumerable.Denumerable]
denumerable_bij_funR [in denumerable.Denumerable]
denumerable_bij_funR [in hilbert.Enumeration]
denumerable_bij_rel [in hilbert.Enumeration]
denumerable_empty [in denumerable.Denumerable]
denumerable_empty [in hilbert.Enumeration]
denumerable_finite [in denumerable.Denumerable]
denumerable_incl [in hilbert.Enumeration]
denumerable_inclusion [in denumerable.Denumerable]
denumerable_inj [in hilbert.Enumeration]
denumerable_members [in schutte.Schutte]
denumerable_not_Unbounded [in schutte.Schutte]
denumerable_segment_proper [in schutte.Ordering_Functions]
denumerable_singleton [in denumerable.Denumerable]
denumerable_surj [in denumerable.Denumerable]
denumerable_union [in denumerable.Denumerable]
denumerable_union_qcq [in denumerable.Denumerable]
div2_double_is_id [in denumerable.Arith_lemmas]
double_inj [in denumerable.Arith_lemmas]
double_is_even [in denumerable.Arith_lemmas]


E

empty_enumeration [in hilbert.Enumeration]
empty_ordering [in schutte.Ordering_Functions]
epsilon_e [in hilbert.OldEpsilon]
epsilon_equiv [in hilbert.Epsilon]
epsilon_equiv [in hilbert.OldEpsilon]
epsilon_ind [in hilbert.Epsilon]
epsilon_ind [in hilbert.OldEpsilon]
Eps0_alg.Eps0_rpo.ap_plus [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.ap_plusR [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.Cantor_normal_form [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_ok_1 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_reflect [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_reflectR [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_rw1 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_rw2 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.compare_rw3 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.cons_ambiguity [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.cons_unicity [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_compat [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_fin_omega [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_F_compat [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.le_phi0_phi0 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.le_succ_succ [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_a_phi0_a [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_inc_rpo_0 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_intro [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_phi0_phi0 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_subterm1 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_subterm2 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_le [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_le_R [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_le_2 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.lt_succ_succ [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_assoc [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_comm [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_dec [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_le_1 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.max_nf [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus_a_a [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus_le [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus_lt [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_a_0 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_a_1 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_compat [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_fin_omega [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_0_a [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult_1_a [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nat_lt_cons [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nat_2_term_mono [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nf_Wf [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.omega_exp_rw [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.omega_minus_one [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.omega_term_ambiguity [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_log [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_lt [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_ltR [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.phi0_plus_mult [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_a_zero [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_compat [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_cons_cons_rw1 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_cons_cons_rw2 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_cons_cons_rw3 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_fin_omega [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_is_zero [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_nf [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_nf0 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_not_comm [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_to_cons [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus_zero [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.rpo_trans [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.R_inc_rpo [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_compat [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_is_plus_one [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_nf [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ_nf2 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.trichotomy [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size1 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size2 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size3 [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.well_founded_rpo [in epsilon0.EPSILON0]
Eps0_prec.prec_antisym [in epsilon0.EPSILON0]
Eps0_prec.prec_dec [in epsilon0.EPSILON0]
Eps0_prec.prec_transitive [in epsilon0.EPSILON0]
Eps0_sig.eq_symbol_dec [in epsilon0.EPSILON0]
eps_extensional_forall_def [in hilbert.OldEpsilon]
eps_extentional_exm [in hilbert.OldEpsilon]
equiv_cong1 [in epsilon0.MSE0]
equiv_cong2 [in epsilon0.MSE0]
equiv_cons [in epsilon0.MSE0]
equiv_perm [in epsilon0.MSE0]
equiv_refl [in epsilon0.MSE0]
equiv_sym [in epsilon0.MSE0]
equiv_tail [in epsilon0.MSE0]
equiv_trans [in epsilon0.MSE0]
eq_le [in schutte.Schutte]
Euc1 [in prelude.More_nat]
Euc2 [in prelude.More_nat]
eval_bounded [in schutte.CNF]
eval_ordinal [in schutte.CNF]
even_prod [in denumerable.Arith_lemmas]
excluded_middle_informative [in hilbert.ClassicalEpsilonModified]
exists_map12_without_repetition [in prelude.more_list]
exists_map_without_repetition [in prelude.more_list]
exp_nf [in epsilon0.E0_ARITH]
ex_to_sig [in hilbert.OldEpsilon]
ex_unic_introduction [in hilbert.Epsilon]
ex_1_introduction [in hilbert.OldEpsilon]


F

Final [in misc.G4]
final_no_future [in misc.G4]
find_not_mem [in prelude.more_list]
finite_inj [in schutte.Schutte]
finite_is_finite [in gamma0.Gamma0]
finite_lt [in epsilon0.EPSILON0]
finite_ltR [in epsilon0.EPSILON0]
finite_lt_inv [in schutte.Schutte]
finite_lt_omega [in schutte.Schutte]
finite_lt_omega [in gamma0.Gamma0]
finite_mono [in schutte.Schutte]
finite_plus_ge_omega [in schutte.Plus]
forall_def [in hilbert.OldEpsilon]
forall_def [in hilbert.Epsilon]
FunctionalChoice [in hilbert.OldEpsilon]
fun_eq_refl [in schutte.Ordering_Functions]
F1 [in misc.G4]
F2 [in misc.G4]
F27 [in misc.G4]
F28 [in misc.G4]
F3 [in misc.G4]
F4 [in misc.G4]
f_decreases [in epsilon0.EPSILON0]
f_not_in_normal_form [in epsilon0.EPSILON0]
f_Sn [in misc.G4]
f_sup_commutes [in schutte.Ordering_Functions]


G

Gamma0_alg.Gamma0_rpo.cons_lt_epsilon0 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.cons_rw [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.epsilon0_as_lub [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.epsilon_fxp [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.F_not_lim [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.inj_mono [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.inj_monoR [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_ab [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_cons_inv [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_intro [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_not_succ [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_successor_ok [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_succ_not_lim [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.le_b_phi_ab [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.le_plus_l [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.le_plus_r [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_inv0 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_lim [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_ok [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_plus [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_a_phi_ab [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_ok [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_okR [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_succ [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_epsilon0_trans [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_inc_rpo_0 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_not_gt [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_rpo_cons_cons [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lt_subterm1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lub_mono [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lub_unicity [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.ml_psi [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.ml_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_lt_cons [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_lt_psi [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_2_term_mono [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nf_intro [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nf_nat_irrelevance [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nf_Wf [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.no_critical [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_alpha_zero [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_cases [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_cases' [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_cases_aux [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_fix [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_inj_r [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_le [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_le_ge [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_mono_r [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_mono_RR [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_mono_weak_r [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_nf [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_any_cons [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_psi [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_psi_plus_finite [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_of_psi_succ [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_principal [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_principalR [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_psi [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_spec1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_2 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_3 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_4 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_5 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi_to_psi_6 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_assoc [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_mono_l_weak [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_mono_r [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.plus_nf [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_nf [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_cons [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_cons' [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_limit [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.pred_of_succ [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.psi_lt_epsilon0 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.psi_principal [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_trans [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_2 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_3 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_2_4 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_2 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_3 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_3_4 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_2 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_3 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_4_4 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_2 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_3 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_5_4 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_6_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_6_4 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.rpo_7_1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.R_inc_rpo [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.succ_as_plus [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.succ_limit_dec [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.succ_nf [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.th_14_5 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.th_14_6 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T1_injection [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T1_injection_lt [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size1 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size2 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size3 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size4 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size_psi [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.well_founded_rpo [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.zero_not_lim [in gamma0.Gamma0]
Gamma0_prec.prec_antisym [in gamma0.Gamma0]
Gamma0_prec.prec_dec [in gamma0.Gamma0]
Gamma0_prec.prec_transitive [in gamma0.Gamma0]
Gamma0_sig.eq_symbol_dec [in gamma0.Gamma0]
get_predecessor [in prelude.More_nat]
ge_ordinal [in schutte.Schutte]
Goodstein_decrease [in epsilon0.Goodstein]
goodstein_next_ord_correct [in epsilon0.Goodstein]
goodstein_next_ord_lt [in epsilon0.Goodstein]
goodstein_next_ord_nf [in epsilon0.Goodstein]
Goodstein_thm [in epsilon0.Goodstein]
gpred_lt [in epsilon0.Goodstein]
Greater_inc_ord [in schutte.Plus]
Greater_o_segment [in schutte.Plus]
gt_ordinal [in schutte.Schutte]
G4_length [in misc.G4]
g_bij [in schutte.Ordering_Functions]
g_def [in schutte.Ordering_Functions]
g_def1 [in schutte.Ordering_Functions]
g_domains [in schutte.Ordering_Functions]
g_lemma [in schutte.Ordering_Functions]
g_mono [in schutte.Ordering_Functions]
g_ord [in schutte.Ordering_Functions]
g_unic [in schutte.Ordering_Functions]
g_1_bij [in schutte.Ordering_Functions]
g_1_of [in schutte.Ordering_Functions]


H

has_cnf_ordinal [in schutte.CNF]
head_at_l_nil [in epsilon0.Hydra]
head_at_l_O_cons [in epsilon0.Hydra]
head_at_l_S_cons [in epsilon0.Hydra]
head_at_l_S_nil [in epsilon0.Hydra]
head_at_l_zero_nil [in epsilon0.Hydra]
head_at_nil [in epsilon0.Hydra]
head_at_O_cons [in epsilon0.Hydra]
head_at_S_cons [in epsilon0.Hydra]
head_at_S_nil [in epsilon0.Hydra]
head_at_zero_nil [in epsilon0.Hydra]
head_lt_cons [in epsilon0.EPSILON0]
Hydra_answers [in epsilon0.Hydra]
Hydra_answers_nil [in epsilon0.Hydra]
h2ol_nfs [in epsilon0.Hydra]
h2o_nf [in epsilon0.Hydra]
h_bij [in SCHROEDER.Schroeder]


I

Im_stable_par_incl [in SCHROEDER.Functions]
Inc_elim [in schutte.Ordering_Functions]
induc [in hilbert.Paradoxical]
Induction [in schutte.Schutte]
inh_ens_OT [in schutte.Critical]
inh_nat [in schutte.AP]
inh_Ordinal_sets [in schutte.Ordering_Functions]
inh_OT_OT [in schutte.Ordering_Functions]
inv_compose [in hilbert.PartialFun]
inv_composeR [in hilbert.PartialFun]
inv_fun_bij [in hilbert.PartialFun]
inv_spec_ex [in hilbert.PartialFun]
inv_spec_func [in hilbert.PartialFun]
inv_trans [in prelude.closure]
in_in_map [in prelude.more_list]
in_map_in [in prelude.more_list]
in_remove [in prelude.more_list]
iota_e [in hilbert.OldEpsilon]
iota_e [in hilbert.Epsilon]
iota_fun_e [in hilbert.OldEpsilon]
iota_fun_e [in hilbert.Epsilon]
iota_fun_ind [in hilbert.Epsilon]
iota_fun_ind [in hilbert.OldEpsilon]
iota_fun_rw [in hilbert.Epsilon]
iota_fun_rw [in hilbert.OldEpsilon]
iota_ind [in hilbert.OldEpsilon]
iota_ind [in hilbert.Epsilon]
iota_parameter_rw [in hilbert.OldEpsilon]
iota_parameter_rw [in hilbert.Epsilon]
isotonicity_refl [in schutte.Well_Orders]
isotonicity_sym [in schutte.Well_Orders]
isotonicity_trans [in schutte.Well_Orders]
iso_inj [in schutte.Well_Orders]
is_finite_finite [in gamma0.Gamma0]
is_limit_omega [in schutte.Schutte]
is_limit_ordinal [in schutte.Schutte]
is_limit_phi0 [in schutte.AP]
is_limit_sup_members [in schutte.Schutte]
is_succ_ordinal [in schutte.Schutte]


K

ksi_plus_beta [in schutte.AP]
ksi_plus_beta_eq [in schutte.AP]
ksi_plus_seq_n' [in schutte.AP]


L

lab_bij [in denumerable.Denumerable]
lab_rel_wf [in denumerable.Denumerable]
least_AP [in schutte.AP]
least_member_glb [in schutte.Well_Orders]
least_member_lower_bound [in schutte.Well_Orders]
least_member_of_eq [in schutte.Well_Orders]
least_member_unicity [in schutte.Well_Orders]
Legend [in epsilon0.Hydra]
length_a [in gamma0.Gamma0_length]
length_ab [in gamma0.Gamma0_length]
length_abnc [in gamma0.Gamma0_length]
length_b [in gamma0.Gamma0_length]
length_c [in gamma0.Gamma0_length]
length_map [in prelude.more_list]
length_n [in gamma0.Gamma0_length]
length_psi [in gamma0.Gamma0_length]
lexof_wf [in denumerable.Denumerable]
lex_trans [in rpo.rpo]
le_alpha_zero [in schutte.Schutte]
Le_antisym [in schutte.Well_Orders]
le_antisym [in schutte.Schutte]
le_cons_tail [in gamma0.Gamma0]
le_disj [in schutte.Schutte]
le_eq_or_lt [in schutte.Schutte]
le_inv [in epsilon0.EPSILON0]
le_inv_nc [in gamma0.Gamma0]
le_lt_trans [in schutte.Schutte]
le_lt_trans [in epsilon0.EPSILON0]
le_lt_trans [in gamma0.Gamma0]
Le_Lt_trans [in schutte.Well_Orders]
le_not_gt [in schutte.Schutte]
le_one_cons [in gamma0.Gamma0]
le_ordinal [in schutte.Schutte]
le_plus_l [in schutte.Plus]
le_plus_r [in schutte.Plus]
le_psi_term_le [in gamma0.Gamma0]
Le_refl [in schutte.Well_Orders]
le_refl [in schutte.Schutte]
le_sup_members [in schutte.Schutte]
le_tail [in epsilon0.EPSILON0]
le_trans [in schutte.Schutte]
Le_trans [in schutte.Well_Orders]
le_trans [in gamma0.Gamma0]
le_trans [in epsilon0.EPSILON0]
le_zero [in schutte.Schutte]
le_zero_alpha [in gamma0.Gamma0]
le_zero_inv [in epsilon0.EPSILON0]
list_app_length [in prelude.more_list]
list_size_app [in prelude.more_list]
list_size_fold [in prelude.more_list]
list_size_size_eq [in prelude.more_list]
list_size_tl_compat [in prelude.more_list]
LLL [in schutte.AP]
log_nf [in epsilon0.EPSILON0]
log_ordinal [in schutte.AP]
ltM_app [in epsilon0.MSE0]
ltM_appR [in epsilon0.MSE0]
ltM_cons [in epsilon0.MSE0]
ltM_equiv_ltM [in epsilon0.MSE0]
ltM_equiv_ltMR [in epsilon0.MSE0]
ltM_head [in epsilon0.MSE0]
ltM_inv [in epsilon0.MSE0]
ltM_inv2 [in epsilon0.MSE0]
ltM_inv3 [in epsilon0.MSE0]
ltM_lt [in epsilon0.MSE0]
ltM_tail [in epsilon0.MSE0]
ltM_trans [in epsilon0.MSE0]
ltM_trans_1 [in epsilon0.MSE0]
ltM_trans_2 [in epsilon0.MSE0]
lt_alpha_cons [in gamma0.Gamma0]
lt_alpha_psi [in gamma0.Gamma0]
lt_beta_cons [in gamma0.Gamma0]
lt_beta_psi [in gamma0.Gamma0]
lt_compat [in gamma0.Gamma0]
lt_compatR [in gamma0.Gamma0]
Lt_connect [in schutte.Well_Orders]
lt_cons_omega_inv [in gamma0.Gamma0]
lt_inv [in epsilon0.EPSILON0]
lt_inv_b [in epsilon0.EPSILON0]
lt_inv_le [in epsilon0.EPSILON0]
lt_inv_nb [in epsilon0.EPSILON0]
lt_irr [in epsilon0.EPSILON0]
lt_irr [in gamma0.Gamma0]
lt_irr [in schutte.Schutte]
lt_le [in schutte.Schutte]
Lt_Le_trans [in schutte.Well_Orders]
lt_le_trans [in gamma0.Gamma0]
lt_le_trans [in epsilon0.EPSILON0]
lt_le_trans [in schutte.Schutte]
lt_ltM [in epsilon0.MSE0]
lt_ltM2 [in epsilon0.MSE0]
lt_lt_Sn [in prelude.More_nat]
lt_not_gt [in epsilon0.EPSILON0]
Lt_not_Gt [in schutte.Well_Orders]
lt_not_le [in epsilon0.EPSILON0]
lt_not_wf [in epsilon0.EPSILON0]
lt_omega_finite [in schutte.Schutte]
lt_omega_inv [in gamma0.Gamma0]
lt_omega_is_finite [in gamma0.Gamma0]
lt_omega_limit [in schutte.Schutte]
lt_omega_limit_lt_exists_lt [in schutte.Schutte]
lt_one_inv [in gamma0.Gamma0]
lt_ordinal [in schutte.Schutte]
lt_or_ge [in schutte.Schutte]
lt_succ [in gamma0.Gamma0]
lt_succ [in schutte.Schutte]
lt_succ_le [in schutte.Schutte]
lt_succ_le [in gamma0.Gamma0]
lt_succ_le_2 [in schutte.Schutte]
lt_succ_lt [in schutte.Schutte]
lt_sup_exists_leq [in schutte.Schutte]
lt_sup_exists_lt [in schutte.Schutte]
lt_tail [in gamma0.Gamma0]
lt_tail0 [in gamma0.Gamma0]
lt_than_psi [in gamma0.Gamma0]
lt_trans [in epsilon0.EPSILON0]
lt_trans [in schutte.Schutte]
L1 [in misc.G4]
L1 [in hilbert.more_relations]
L2 [in hilbert.more_relations]
L2 [in misc.G4]
L2 [in hilbert.Paradoxical]
L2' [in hilbert.Paradoxical]
L3 [in misc.G4]
L3 [in schutte.Ordering_Functions]
L3a [in schutte.Ordering_Functions]
L3' [in schutte.Ordering_Functions]
L4 [in misc.G4]
L4 [in hilbert.Paradoxical]
L5 [in hilbert.Paradoxical]
L5 [in misc.G4]
L55 [in hilbert.Paradoxical]
L66 [in hilbert.Paradoxical]
L_two_2 [in hilbert.Epsilon_Examples]
L_two_2' [in hilbert.Epsilon_Examples]


M

Make.context_multiset_extension_step_app1 [in prelude.dickson]
Make.context_multiset_extension_step_app2 [in prelude.dickson]
Make.context_trans_clos_multiset_extension_step_app1 [in prelude.dickson]
Make.dickson [in prelude.dickson]
Make.dickson_aux1 [in prelude.dickson]
Make.dickson_aux2 [in prelude.dickson]
Make.dickson_aux3 [in prelude.dickson]
Make.list_permut_acc [in prelude.dickson]
Make.list_permut_multiset_extension_step_1 [in prelude.dickson]
Make.list_permut_multiset_extension_step_2 [in prelude.dickson]
Make.multiset_closure [in prelude.dickson]
Make.two_cases [in prelude.dickson]
map_app [in prelude.more_list]
map_map [in prelude.more_list]
max_le_regL [in prelude.More_nat]
max_le_regR [in prelude.More_nat]
members_eq [in schutte.Schutte]
members_omega [in schutte.Schutte]
members_proper [in schutte.Ordering_Functions]
minimal_exists [in prelude.wf_minimal]
minus_a_a [in schutte.Minus]
minus_a_zero [in schutte.Minus]
minus_defined [in schutte.Minus]
minus_exists [in schutte.Plus]
minus_le [in schutte.Minus]
minus_nf [in epsilon0.E0_ARITH]
multiplicity_of_app [in epsilon0.MSE0]
multiplicity_rw1 [in epsilon0.MSE0]
multiplicity_rw2 [in epsilon0.MSE0]
mult_nf [in epsilon0.E0_ARITH]


N

nat_double_or_s_double [in denumerable.Arith_lemmas]
nb_occ_app [in prelude.more_list]
nexts_ok [in misc.G4]
nexts_ok_R [in misc.G4]
nexts_plus [in misc.G4]
next_unicity [in misc.G4]
nfs_to_nf [in epsilon0.MSE0]
nf2_intro [in epsilon0.EPSILON0]
nf2_phi0 [in epsilon0.EPSILON0]
nf2_phi0R [in epsilon0.EPSILON0]
nf_a [in gamma0.Gamma0]
nf_b [in gamma0.Gamma0]
nf_bounded [in schutte.CNF]
nf_c [in gamma0.Gamma0]
nf_coeff_irrelevance [in epsilon0.EPSILON0]
nf_epsilon [in gamma0.Gamma0]
nf_epsilon0 [in gamma0.Gamma0]
nf_finite_inv [in gamma0.Gamma0]
nf_intro [in epsilon0.EPSILON0]
nf_inv1 [in epsilon0.EPSILON0]
nf_inv2 [in epsilon0.EPSILON0]
nf_inv_tail [in gamma0.Gamma0]
nf_multiplicity_big [in epsilon0.MSE0]
nf_multiplicity_head [in epsilon0.MSE0]
nf_multiplicity_tail [in epsilon0.MSE0]
nf_nfs [in epsilon0.MSE0]
nf_of_finite [in epsilon0.EPSILON0]
nf_omega [in gamma0.Gamma0]
nf_omega [in epsilon0.EPSILON0]
nf_phi0 [in epsilon0.EPSILON0]
nf_subterm [in gamma0.Gamma0]
nf_tail_lt_nf [in epsilon0.EPSILON0]
nf_tower [in epsilon0.EPSILON0]
nf_to_nfs [in epsilon0.MSE0]
nf_unicity [in epsilon0.MSE0]
none_nb_occ_O [in prelude.more_list]
Non_denum [in schutte.Schutte]
normal_phi0 [in schutte.AP]
normal_plus_alpha [in schutte.Plus]
not_acc [in prelude.not_decreasing]
not_all_not_ex' [in prelude.wf_minimal]
not_AP_inv [in schutte.AP]
not_AP_inv2 [in schutte.AP]
not_decreasing [in prelude.not_decreasing]
not_decreasing_aux [in prelude.not_decreasing]
not_denumerable_unbounded [in schutte.Schutte]
not_double_is_s_double [in denumerable.Arith_lemmas]
not_gt_le [in schutte.Schutte]
not_is_limit_succ [in schutte.Schutte]
not_is_limit_zero [in schutte.Schutte]
not_is_succ_limit [in schutte.Schutte]
not_is_succ_zero [in schutte.Schutte]
not_lt_zero [in epsilon0.EPSILON0]
not_lt_zero [in schutte.Schutte]
not_lt_zero [in gamma0.Gamma0]
not_lt_zero_0 [in schutte.Schutte]
Not_Unbounded_bounded [in schutte.Schutte]
Not_Unbounded_denumerable [in schutte.Schutte]
nth_error_map [in prelude.more_list]
nth_error_ok_in [in prelude.more_list]


O

of_beta' [in schutte.Ordering_Functions]
of_image [in schutte.Ordering_Functions]
of_u [in schutte.Plus]
omega_lt_epsilon [in gamma0.Gamma0]
omega_lt_epsilon0 [in gamma0.Gamma0]
Omega_not_well_founded [in hilbert.Paradoxical]
omega_second_AP [in schutte.AP]
Omega_well_founded [in hilbert.Paradoxical]
one_le_some_positive [in hilbert.Epsilon_Examples]
one_le_some_positive' [in hilbert.Epsilon_Examples]
one_le_some_positive2 [in hilbert.Epsilon_Examples]
one_plus_ge_omega [in schutte.Plus]
one_plus_omega [in schutte.Plus]
Ordering_bijection [in schutte.Ordering_Functions]
ordering_function_mono [in schutte.Ordering_Functions]
ordering_function_monoR [in schutte.Ordering_Functions]
ordering_function_mono_weak [in schutte.Ordering_Functions]
ordering_function_mono_weakR [in schutte.Ordering_Functions]
ordering_function_ordA [in schutte.Ordering_Functions]
ordering_function_ordB [in schutte.Ordering_Functions]
ordering_function_ordinal_B [in schutte.Ordering_Functions]
ordering_function_seg [in schutte.Ordering_Functions]
ordering_function_seg_unicity [in schutte.Ordering_Functions]
ordering_function_unicity [in schutte.Ordering_Functions]
ordering_le [in schutte.Ordering_Functions]
ordering_segment_2_fun_ok [in schutte.Ordering_Functions]
ordering_unbounded_unbounded [in schutte.Ordering_Functions]
order_function_least_least [in schutte.Ordering_Functions]
ordinal_finite [in schutte.Schutte]
ordinal_finite [in gamma0.Gamma0]
ordinal_finite [in epsilon0.EPSILON0]
ordinal_omega [in schutte.Schutte]
ordinal_omega_limit [in schutte.Schutte]
ordinal_O_segment [in schutte.Ordering_Functions]
ordinal_phi0 [in schutte.AP]
ordinal_plus [in schutte.Plus]
ordinal_succ [in schutte.Schutte]
ordinal_sup_members [in schutte.Schutte]
ordinal_zero [in schutte.Schutte]
or_to_sum [in hilbert.OldEpsilon]
or_to_sum [in hilbert.Epsilon]
O_segment_lt [in schutte.Ordering_Functions]
O_segment_lt_closed [in schutte.Ordering_Functions]
O_segment_ordinal [in schutte.Ordering_Functions]
O_segment_unbounded [in schutte.Ordering_Functions]


P

paradox [in hilbert.diag]
paradox [in hilbert.Paradoxical]
paraphrase [in hilbert.Paradoxical]
Permut.DS.Make.ac_syntactic [in prelude.list_permut]
Permut.DS.Make.ac_syntactic_aux [in prelude.list_permut]
Permut.DS.Make.cons_permut_in [in prelude.list_permut]
Permut.DS.Make.context_list_permut_app1 [in prelude.list_permut]
Permut.DS.Make.context_list_permut_app2 [in prelude.list_permut]
Permut.DS.Make.context_list_permut_cons [in prelude.list_permut]
Permut.DS.Make.in_mult_S [in prelude.list_permut]
Permut.DS.Make.in_permut_in [in prelude.list_permut]
Permut.DS.Make.list_permut_add_cons_inside [in prelude.list_permut]
Permut.DS.Make.list_permut_add_inside [in prelude.list_permut]
Permut.DS.Make.list_permut_app_app [in prelude.list_permut]
Permut.DS.Make.list_permut_dec [in prelude.list_permut]
Permut.DS.Make.list_permut_length [in prelude.list_permut]
Permut.DS.Make.list_permut_length_1 [in prelude.list_permut]
Permut.DS.Make.list_permut_length_2 [in prelude.list_permut]
Permut.DS.Make.list_permut_map [in prelude.list_permut]
Permut.DS.Make.list_permut_nil [in prelude.list_permut]
Permut.DS.Make.list_permut_refl [in prelude.list_permut]
Permut.DS.Make.list_permut_remove_hd [in prelude.list_permut]
Permut.DS.Make.list_permut_size [in prelude.list_permut]
Permut.DS.Make.list_permut_sym [in prelude.list_permut]
Permut.DS.Make.list_permut_trans [in prelude.list_permut]
Permut.DS.Make.multiplicity_app [in prelude.list_permut]
Permut.DS.Make.out_mult_O [in prelude.list_permut]
Permut.DS.Make.remove_context_list_permut_app2 [in prelude.list_permut]
Permut.DS.Make.remove_context_list_permut_cons [in prelude.list_permut]
PFix_eq [in prelude.PartialFix]
PFix_F_eq [in prelude.PartialFix]
PFix_F_inv [in prelude.PartialFix]
phi0_alpha_phi0_beta [in schutte.AP]
phi0_elim [in schutte.AP]
phi0_inj [in schutte.AP]
phi0_log_le [in schutte.AP]
phi0_mono [in schutte.AP]
phi0_mono_R [in schutte.AP]
phi0_mono_R_weak [in schutte.AP]
phi0_mono_weak [in schutte.AP]
phi0_of_limit [in schutte.AP]
phi0_ordering [in schutte.AP]
phi0_positive [in schutte.AP]
phi0_sup [in schutte.AP]
phi0_zero [in schutte.AP]
plus_alpha_0 [in gamma0.Gamma0]
plus_assoc [in schutte.Plus]
plus_assoc [in epsilon0.E0_ARITH]
plus_assoc' [in schutte.Plus]
plus_assoc0 [in epsilon0.E0_ARITH]
plus_assoc1 [in schutte.Plus]
plus_assoc2 [in schutte.Plus]
plus_assoc3 [in schutte.Plus]
plus_elim [in schutte.Plus]
plus_FF [in schutte.Plus]
plus_limit [in schutte.Plus]
plus_lt_phi0 [in schutte.AP]
plus_minus [in schutte.Minus]
plus_mono_r [in schutte.Plus]
plus_mono_r_weak [in schutte.Plus]
plus_mono_weak_l [in schutte.Plus]
plus_of_succ [in schutte.Plus]
plus_ordering [in schutte.Plus]
plus_reg_r [in schutte.Plus]
plus_2 [in denumerable.Arith_lemmas]
power_of_1 [in prelude.More_nat]
pred2_lt [in hilbert.Epsilon_Examples]
pred_defined [in epsilon0.E0_ARITH]
pred_nf [in epsilon0.E0_ARITH]
pred_of_power [in prelude.More_nat]
pred_of_succ [in epsilon0.E0_ARITH]
pred_42 [in hilbert.Epsilon_Examples]
Proper_A [in schutte.Ordering_Functions]
proper_members [in schutte.Ordering_Functions]
proper_segment_ordinals [in schutte.Ordering_Functions]
prop_map12_without_repetition [in prelude.more_list]
prop_map_without_repetition [in prelude.more_list]
psi_eq [in gamma0.Gamma0_prelude]
psi_le_cons [in gamma0.Gamma0]
psi_relevance [in gamma0.Gamma0]


Q

quasi_classic [in hilbert.OldEpsilon]


R

reachable_Rgstar [in misc.G4]
reduce_assoc_list [in prelude.more_list]
rel_inv_bij [in hilbert.PartialFun]
Rh_decrease [in epsilon0.Hydra]
Rh_head [in epsilon0.Hydra]
Rn_decrease [in epsilon0.Hydra]
Rn_head [in epsilon0.Hydra]
RPO.T.P.LP.Make.acc_build [in rpo.rpo]
RPO.T.P.LP.Make.acc_lex_drop_proof [in rpo.rpo]
RPO.T.P.LP.Make.in_sn_sn [in rpo.rpo]
RPO.T.P.LP.Make.lex1 [in rpo.rpo]
RPO.T.P.LP.Make.lex1_bis [in rpo.rpo]
RPO.T.P.LP.Make.lex2 [in rpo.rpo]
RPO.T.P.LP.Make.lex3 [in rpo.rpo]
RPO.T.P.LP.Make.list_permut_map_acc [in rpo.rpo]
RPO.T.P.LP.Make.o_size3_trans [in rpo.rpo]
RPO.T.P.LP.Make.projection_list_of_SN_terms [in rpo.rpo]
RPO.T.P.LP.Make.rpo_add_context [in rpo.rpo]
RPO.T.P.LP.Make.rpo_closure [in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex_rest_same_length [in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex_same_length [in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul_trans_clos [in rpo.rpo]
RPO.T.P.LP.Make.rpo_subst [in rpo.rpo]
RPO.T.P.LP.Make.rpo_subterm [in rpo.rpo]
RPO.T.P.LP.Make.rpo_trans [in rpo.rpo]
RPO.T.P.LP.Make.two_cases_rpo [in rpo.rpo]
RPO.T.P.LP.Make.wf_on_lex_rest [in rpo.rpo]
RPO.T.P.LP.Make.wf_on_mul_rest [in rpo.rpo]
RPO.T.P.LP.Make.wf_on_rest [in rpo.rpo]
RPO.T.P.LP.Make.wf_rpo [in rpo.rpo]
RPO.T.P.LP.Make.wf_rpo_term [in rpo.rpo]
RPO.T.P.LP.Make.wf_size [in rpo.rpo]
RPO.T.P.LP.Make.wf_size2 [in rpo.rpo]
RPO.T.P.LP.Make.wf_size3 [in rpo.rpo]
R1_decrease [in epsilon0.Hydra]
R1_head [in epsilon0.Hydra]
R2 [in hilbert.Paradoxical]
r2f_ok [in hilbert.PartialFun]
r2i_ok [in hilbert.PartialFun]
R_inclusion_codomain [in denumerable.Denumerable]
R_inclusion_domain [in denumerable.Denumerable]
R_inclusion_enumerates [in denumerable.Denumerable]
R_inclusion_inj [in denumerable.Denumerable]
R_inv_inj [in denumerable.GRelations]
R_inv_surj [in denumerable.GRelations]
R_nat_elaguee_domain [in denumerable.GRelations]
R_nat_elaguee_fun [in denumerable.GRelations]
R_union_codomain [in denumerable.Denumerable]
R_union_domain [in denumerable.Denumerable]
R_union_enumerates [in denumerable.Denumerable]
R_union_inj [in denumerable.Denumerable]
R_union_qcq_codomain [in denumerable.Denumerable]
R_union_qcq_domain [in denumerable.Denumerable]
R_union_qcq_inj [in denumerable.Denumerable]
R_union_qcq_numbers [in denumerable.Denumerable]


S

Schroeder [in SCHROEDER.Schroeder]
seq_mono_inj [in schutte.Schutte]
seq_mono_intro [in schutte.Schutte]
seq_range_denumerable [in denumerable.Denumerable]
seq_range_denumerable [in schutte.Schutte]
seq_range_enumeration [in hilbert.Enumeration]
Setminus_contravariant [in SCHROEDER.Setminus_fact]
Set_Sum_is_majoring [in SCHROEDER.Sums]
Set_Sum_is_minoring [in SCHROEDER.Sums]
SF27 [in misc.G4]
SF3 [in misc.G4]
Sh_head [in epsilon0.Hydra]
some_e [in hilbert.OldEpsilon]
some_e [in hilbert.Epsilon]
some_fun_e [in hilbert.OldEpsilon]
some_fun_e [in hilbert.Epsilon]
some_fun_ind [in hilbert.Epsilon]
some_fun_ind [in hilbert.OldEpsilon]
some_ind [in hilbert.Epsilon]
some_ind [in hilbert.OldEpsilon]
some_nb_occ_Sn [in prelude.more_list]
sorted_lt [in schutte.CNF]
sorted_lt_lt [in schutte.CNF]
sorted_lt_lt_2 [in schutte.CNF]
sorted_tail [in schutte.CNF]
sort_aux_equiv [in epsilon0.MSE0]
sort_aux_nf [in epsilon0.MSE0]
sort_equiv [in epsilon0.MSE0]
sort_nf [in epsilon0.MSE0]
split_list_app_cons [in prelude.more_list]
star_com [in hilbert.Paradoxical]
subterm_lt [in gamma0.Gamma0]
succ_injection [in schutte.Schutte]
succ_lt_le [in gamma0.Gamma0]
succ_mono [in schutte.Schutte]
succ_monoR [in schutte.Schutte]
succ_of_cons [in gamma0.Gamma0]
succ_rw [in schutte.Schutte]
succ_zero_diff [in schutte.Schutte]
sup_eq_intro [in schutte.Schutte]
sup_exists [in schutte.Schutte]
sup_least_upper_bound [in schutte.Schutte]
sup_members_disj [in schutte.Schutte]
sup_members_not_succ [in schutte.Schutte]
sup_members_succ [in schutte.Schutte]
sup_mono [in schutte.Schutte]
sup_M_in_B [in schutte.Ordering_Functions]
sup_of_leq [in schutte.Schutte]
sup_ordinal [in schutte.Schutte]
sup_unicity [in schutte.Schutte]
sup_upper_bound [in schutte.Schutte]
S.DS.Make.add_comm [in prelude.list_set]
S.DS.Make.add_prf [in prelude.list_set]
S.DS.Make.add_1 [in prelude.list_set]
S.DS.Make.add_12 [in prelude.list_set]
S.DS.Make.add_2 [in prelude.list_set]
S.DS.Make.cardinal_eq_set [in prelude.list_set]
S.DS.Make.cardinal_subset [in prelude.list_set]
S.DS.Make.cardinal_union [in prelude.list_set]
S.DS.Make.cardinal_union_inter_12 [in prelude.list_set]
S.DS.Make.cardinal_union_1 [in prelude.list_set]
S.DS.Make.cardinal_union_2 [in prelude.list_set]
S.DS.Make.eq_set_dec [in prelude.list_set]
S.DS.Make.eq_set_list_permut_support [in prelude.list_set]
S.DS.Make.eq_set_refl [in prelude.list_set]
S.DS.Make.eq_set_sym [in prelude.list_set]
S.DS.Make.eq_set_trans [in prelude.list_set]
S.DS.Make.filter_union [in prelude.list_set]
S.DS.Make.filter_1 [in prelude.list_set]
S.DS.Make.filter_1_list [in prelude.list_set]
S.DS.Make.filter_2 [in prelude.list_set]
S.DS.Make.filter_2_list [in prelude.list_set]
S.DS.Make.included_filter_aux [in prelude.list_set]
S.DS.Make.included_remove_red [in prelude.list_set]
S.DS.Make.inter_1 [in prelude.list_set]
S.DS.Make.inter_12 [in prelude.list_set]
S.DS.Make.inter_12_aux [in prelude.list_set]
S.DS.Make.inter_1_aux [in prelude.list_set]
S.DS.Make.inter_2 [in prelude.list_set]
S.DS.Make.inter_2_aux [in prelude.list_set]
S.DS.Make.mem_dec [in prelude.list_set]
S.DS.Make.remove_red_included [in prelude.list_set]
S.DS.Make.subset_cardinal_not_eq_not_eq_set [in prelude.list_set]
S.DS.Make.subset_compat [in prelude.list_set]
S.DS.Make.subset_compat_1 [in prelude.list_set]
S.DS.Make.subset_compat_2 [in prelude.list_set]
S.DS.Make.subset_dec [in prelude.list_set]
S.DS.Make.subset_filter [in prelude.list_set]
S.DS.Make.subset_inter_1 [in prelude.list_set]
S.DS.Make.subset_inter_2 [in prelude.list_set]
S.DS.Make.subset_subset_union [in prelude.list_set]
S.DS.Make.subset_union_1 [in prelude.list_set]
S.DS.Make.subset_union_2 [in prelude.list_set]
S.DS.Make.union_assoc [in prelude.list_set]
S.DS.Make.union_comm [in prelude.list_set]
S.DS.Make.union_compat_eq_set [in prelude.list_set]
S.DS.Make.union_compat_subset_1 [in prelude.list_set]
S.DS.Make.union_compat_subset_2 [in prelude.list_set]
S.DS.Make.union_empty_1 [in prelude.list_set]
S.DS.Make.union_empty_2 [in prelude.list_set]
S.DS.Make.union_1 [in prelude.list_set]
S.DS.Make.union_12 [in prelude.list_set]
S.DS.Make.union_12_aux [in prelude.list_set]
S.DS.Make.union_1_aux [in prelude.list_set]
S.DS.Make.union_2 [in prelude.list_set]
S.DS.Make.union_2_aux [in prelude.list_set]
S.DS.Make.without_red_add [in prelude.list_set]
S.DS.Make.without_red_add_without_red [in prelude.list_set]
S.DS.Make.without_red_filter_aux [in prelude.list_set]
S.DS.Make.without_red_nil [in prelude.list_set]
S.DS.Make.without_red_permut [in prelude.list_set]
S.DS.Make.without_red_remove [in prelude.list_set]
S.DS.Make.without_red_remove_not_common [in prelude.list_set]
S.DS.Make.without_red_remove_not_common_aux [in prelude.list_set]
S.DS.Make.without_red_remove_red [in prelude.list_set]
S.DS.Make.without_red_singleton [in prelude.list_set]
S1_decrease [in epsilon0.Hydra]
S1_head [in epsilon0.Hydra]
S2_decrease [in epsilon0.Hydra]
S2_head [in epsilon0.Hydra]


T

tail_lt_cons [in epsilon0.EPSILON0]
Term.F.X.Term_eq_dec.Make.DecVar.eq_A_dec [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.empty_subst_is_id [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.empty_subst_is_id_list [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.eq_term_dec [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.is_a_pos_exists_subtem [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_is_replace_at_pos1 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_is_replace_at_pos2 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_list_replace_at_pos_in_subterm [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_unfold [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_direct_subterm [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_ge_one [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_subterm_at_pos [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size_unfold [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp_is_subst_comp [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp_is_subst_comp_aux1 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp_is_subst_comp_aux2 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_apply_subst [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_fold [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_unfold [in rpo.term]
the_e [in hilbert.OldEpsilon]
the_e [in hilbert.Epsilon]
the_fun_e [in hilbert.Epsilon]
the_fun_e [in hilbert.OldEpsilon]
the_fun_ind [in hilbert.Epsilon]
the_fun_ind [in hilbert.OldEpsilon]
the_fun_rw [in hilbert.OldEpsilon]
the_fun_rw [in hilbert.Epsilon]
the_ind [in hilbert.Epsilon]
the_ind [in hilbert.OldEpsilon]
the_least_ok [in schutte.Schutte]
the_least_ordinal [in schutte.Schutte]
the_ordering_function_eq [in schutte.Ordering_Functions]
the_ordering_function_ok [in schutte.Ordering_Functions]
the_rw [in hilbert.Epsilon]
the_rw [in hilbert.OldEpsilon]
Th_13_5_1 [in schutte.Ordering_Functions]
Th_13_5_2 [in schutte.Ordering_Functions]
TH_13_6 [in schutte.Ordering_Functions]
TH_13_6R [in schutte.Ordering_Functions]
transitivity [in gamma0.Gamma0]
transitivity0 [in gamma0.Gamma0]
trans_aux [in gamma0.Gamma0]
trans_clos_is_trans [in prelude.closure]
trichotomy [in schutte.Schutte]
tricho_aux [in gamma0.Gamma0]
tricho_lt_2 [in gamma0.Gamma0]
tricho_lt_2' [in gamma0.Gamma0]
tricho_lt_3 [in gamma0.Gamma0]
tricho_lt_4 [in gamma0.Gamma0]
tricho_lt_4' [in gamma0.Gamma0]
tricho_lt_5 [in gamma0.Gamma0]
tricho_lt_7 [in gamma0.Gamma0]


U

unbounded [in schutte.Schutte]
Unbounded_Greater [in schutte.Plus]
Unbounded_not_denumerable [in schutte.Schutte]


V

val_positive [in epsilon0.Goodstein]
Vars.eq_variable_dec [in epsilon0.EPSILON0]
Vars.eq_variable_dec [in gamma0.Gamma0]


W

well_founded_length [in prelude.more_list]
wf_lex [in rpo.rpo]
wf_trans [in prelude.closure]
Winner [in epsilon0.Hydra]


Z

zero_eq_0 [in hilbert.Epsilon_Examples]
zero_le [in epsilon0.EPSILON0]
zero_lt_omega [in schutte.AP]
zero_lt_succ [in gamma0.Gamma0]
zero_lt_succ [in schutte.Schutte]
zero_or_greater [in schutte.Schutte]
zero_or_positive [in schutte.Schutte]
zero_plus_alpha [in schutte.Plus]



Constructor Index

A

all_nats [in hilbert.Enumeration]
AP_intro [in schutte.AP]
ap_intro [in epsilon0.EPSILON0]
ap_intro [in gamma0.Gamma0_prelude]


B

Bin [in prelude.bintree]


C

closed_intro [in schutte.Schutte]
coeff_lt [in epsilon0.EPSILON0]
cons [in schutte.CNF]
cons [in epsilon0.EPSILON0]
cons [in gamma0.Gamma0_prelude]
Cons_correct [in epsilon0.Goodstein]
cons_forall [in schutte.CNF]
cons_lt_e0 [in gamma0.Gamma0_prelude]
cons_nf [in epsilon0.EPSILON0]
cons_nf [in gamma0.Gamma0_prelude]
continuous_intro [in schutte.Schutte]


D

denumerable_intro [in hilbert.Enumeration]
depth1 [in epsilon0.Hydra]
depth2 [in epsilon0.Hydra]


E

enumerates_i [in hilbert.Enumeration]
Eps0_prec.Lex [in epsilon0.EPSILON0]
Eps0_prec.Mul [in epsilon0.EPSILON0]
Eps0_sig.AC [in epsilon0.EPSILON0]
Eps0_sig.C [in epsilon0.EPSILON0]
Eps0_sig.Free [in epsilon0.EPSILON0]
Eps0_sig.nat_S [in epsilon0.EPSILON0]
Eps0_sig.nat_0 [in epsilon0.EPSILON0]
Eps0_sig.ord_cons [in epsilon0.EPSILON0]
Eps0_sig.ord_zero [in epsilon0.EPSILON0]
equipollence_intro [in SCHROEDER.Equipollence]


F

final_intro [in misc.G4]
from_E [in denumerable.Denumerable]
from_F [in denumerable.Denumerable]
fun_bij_i [in hilbert.PartialFun]
fun_inj_i [in hilbert.PartialFun]


G

Gamma0_alg.Gamma0_rpo.cons_succ [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.finite_succ [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_cons [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_limit_0 [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_cons [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F_0 [in gamma0.Gamma0]
Gamma0_prec.Lex [in gamma0.Gamma0]
Gamma0_prec.Mul [in gamma0.Gamma0]
Gamma0_sig.AC [in gamma0.Gamma0]
Gamma0_sig.C [in gamma0.Gamma0]
Gamma0_sig.Free [in gamma0.Gamma0]
Gamma0_sig.nat_S [in gamma0.Gamma0]
Gamma0_sig.nat_0 [in gamma0.Gamma0]
Gamma0_sig.ord_cons [in gamma0.Gamma0]
Gamma0_sig.ord_psi [in gamma0.Gamma0]
Gamma0_sig.ord_zero [in gamma0.Gamma0]


H

hcons [in epsilon0.Hydra]
head [in epsilon0.Hydra]
head_lt [in epsilon0.EPSILON0]
hl_intro [in SCHROEDER.Schroeder]
hr_intro [in SCHROEDER.Schroeder]


I

Im_intro [in SCHROEDER.Functions]
inf_card_intro [in SCHROEDER.Equipollence]


L

Later [in epsilon0.Hydra]
Leaf [in prelude.bintree]
less_than [in hilbert.Enumeration]


M

Make.rmv_case [in prelude.dickson]
mk_cnf_of [in schutte.CNF]


N

nfs_cons [in epsilon0.MSE0]
nfs_nil [in epsilon0.MSE0]
nf2_c [in epsilon0.EPSILON0]
nf2_z [in epsilon0.EPSILON0]
nil [in schutte.CNF]
nil_forall [in schutte.CNF]
node [in epsilon0.Hydra]
NoneT [in hilbert.PartialFun]
normal_intro [in schutte.Ordering_Functions]
Now [in epsilon0.Hydra]


O

opt_bij_i [in hilbert.PartialFun]
opt_inj_i [in hilbert.PartialFun]


P

Precedence.Lex [in rpo.rpo]
Precedence.Mul [in rpo.rpo]


R

rel_bij_i [in hilbert.PartialFun]
rel_inj_i [in denumerable.GRelations]
rel_inj_i [in hilbert.PartialFun]
Rel_intro [in SCHROEDER.Functions]
rel_surj_i [in denumerable.GRelations]
Rg0 [in misc.G4]
Rg1 [in misc.G4]
Rg2 [in misc.G4]
Rg_i [in epsilon0.Goodstein]
Rnl_rest [in epsilon0.Hydra]
Rn_here [in epsilon0.Hydra]
Rn_plus [in epsilon0.Hydra]
RPO.T.P.LP.Eq [in rpo.rpo]
RPO.T.P.LP.List_eq [in rpo.rpo]
RPO.T.P.LP.List_gt [in rpo.rpo]
RPO.T.P.LP.List_mul [in rpo.rpo]
RPO.T.P.LP.Lt [in rpo.rpo]
RPO.T.P.LP.Make.Eq [in rpo.rpo]
RPO.T.P.LP.Make.List_eq [in rpo.rpo]
RPO.T.P.LP.Make.List_eq_rest [in rpo.rpo]
RPO.T.P.LP.Make.List_gt [in rpo.rpo]
RPO.T.P.LP.Make.List_gt_rest [in rpo.rpo]
RPO.T.P.LP.Make.List_mul [in rpo.rpo]
RPO.T.P.LP.Make.List_mul_rest [in rpo.rpo]
RPO.T.P.LP.Make.List_mul_rest_step [in rpo.rpo]
RPO.T.P.LP.Make.Lt [in rpo.rpo]
RPO.T.P.LP.Make.Subterm [in rpo.rpo]
RPO.T.P.LP.Make.Top_eq_lex [in rpo.rpo]
RPO.T.P.LP.Make.Top_eq_mul [in rpo.rpo]
RPO.T.P.LP.Make.Top_gt [in rpo.rpo]
RPO.T.P.LP.Subterm [in rpo.rpo]
RPO.T.P.LP.Top_eq_lex [in rpo.rpo]
RPO.T.P.LP.Top_eq_mul [in rpo.rpo]
RPO.T.P.LP.Top_gt [in rpo.rpo]
R1_node [in epsilon0.Hydra]
R1_single [in epsilon0.Hydra]


S

Set_Sum_intro [in SCHROEDER.Sums]
Sh_1 [in epsilon0.Hydra]
Sh_2 [in epsilon0.Hydra]
Sh_3 [in epsilon0.Hydra]
Signature.AC [in rpo.term]
Signature.C [in rpo.term]
Signature.Free [in rpo.term]
single [in epsilon0.Hydra]
single_nf [in epsilon0.EPSILON0]
single_nf [in gamma0.Gamma0_prelude]
Sn_first [in epsilon0.Hydra]
Sn_single [in epsilon0.Hydra]
SomeT [in hilbert.PartialFun]
sortedn [in schutte.CNF]
sorted0 [in schutte.CNF]
sorted1 [in schutte.CNF]
subterm_a [in gamma0.Gamma0]
subterm_b [in gamma0.Gamma0]
subterm_c [in gamma0.Gamma0]
subterm_trans [in gamma0.Gamma0]
succ_finite [in gamma0.Gamma0_prelude]
S1_first [in epsilon0.Hydra]
S1_last [in epsilon0.Hydra]
S1_rest [in epsilon0.Hydra]
S2_first [in epsilon0.Hydra]
S2_rest [in epsilon0.Hydra]
S2_single [in epsilon0.Hydra]


T

tail_lt [in epsilon0.EPSILON0]
Term.F.X.Term [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Var [in rpo.term]
Term.F.X.Var [in rpo.term]
t_step [in prelude.closure]
t_trans [in prelude.closure]


V

Vars.empty_set [in epsilon0.EPSILON0]
Vars.empty_set [in gamma0.Gamma0]
void [in prelude.bintree]


W

WO_lt_i [in schutte.Well_Orders]


Z

zero [in epsilon0.EPSILON0]
zero [in gamma0.Gamma0_prelude]
Zero_correct [in epsilon0.Goodstein]
zero_finite [in gamma0.Gamma0_prelude]
zero_lt [in epsilon0.EPSILON0]
zero_lt_e0 [in gamma0.Gamma0_prelude]
zero_nf [in gamma0.Gamma0_prelude]
zero_nf [in epsilon0.EPSILON0]



Inductive Index

A

AP [in schutte.AP]
ap [in gamma0.Gamma0_prelude]
ap [in epsilon0.EPSILON0]


B

bijection [in SCHROEDER.Functions]
bintree [in prelude.bintree]


C

closed [in schutte.Schutte]
cnf_of [in schutte.CNF]
continuous [in schutte.Schutte]
correct [in epsilon0.Goodstein]


D

denumerable [in hilbert.Enumeration]


E

enumerates [in hilbert.Enumeration]
Eps0_prec.status_type [in epsilon0.EPSILON0]
Eps0_sig.arity_type [in epsilon0.EPSILON0]
Eps0_sig.symb0 [in epsilon0.EPSILON0]
equipollence [in SCHROEDER.Equipollence]


F

final [in misc.G4]
fonction [in SCHROEDER.Functions]
fun_bijection [in hilbert.PartialFun]
fun_injection [in hilbert.PartialFun]


G

Gamma0_alg.Gamma0_rpo.is_limit [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.is_successor [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.limit_plus_F [in gamma0.Gamma0]
Gamma0_prec.status_type [in gamma0.Gamma0]
Gamma0_sig.arity_type [in gamma0.Gamma0]
Gamma0_sig.symb0 [in gamma0.Gamma0]


H

h [in SCHROEDER.Schroeder]
Hercules_wins [in epsilon0.Hydra]
Hydra [in epsilon0.Hydra]
Hydrae [in epsilon0.Hydra]


I

Im [in SCHROEDER.Functions]
inf_card [in SCHROEDER.Equipollence]
injection [in SCHROEDER.Functions]
is_finite [in gamma0.Gamma0_prelude]
item [in misc.G4]


L

lt [in gamma0.Gamma0_prelude]
lt [in epsilon0.EPSILON0]
lt_epsilon0 [in gamma0.Gamma0_prelude]


M

Make.multiset_extension_step [in prelude.dickson]


N

nf [in gamma0.Gamma0_prelude]
nf [in epsilon0.EPSILON0]
nfs [in epsilon0.MSE0]
nf2 [in epsilon0.EPSILON0]
normal [in schutte.Ordering_Functions]


O

Olist [in schutte.CNF]
optionT [in hilbert.PartialFun]
opt_bijection [in hilbert.PartialFun]
opt_injection [in hilbert.PartialFun]
o_forall [in schutte.CNF]


P

Precedence.status_type [in rpo.rpo]


R

Rel [in SCHROEDER.Functions]
rel_bijection [in hilbert.PartialFun]
rel_injection [in denumerable.GRelations]
rel_injection [in hilbert.PartialFun]
rel_surjection [in denumerable.GRelations]
Rg [in epsilon0.Goodstein]
Rg [in misc.G4]
Rh [in epsilon0.Hydra]
Rn [in epsilon0.Hydra]
RPO.T.P.LP.Make.rpo [in rpo.rpo]
RPO.T.P.LP.Make.rpo_eq [in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex [in rpo.rpo]
RPO.T.P.LP.Make.rpo_lex_rest [in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul [in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul_rest [in rpo.rpo]
RPO.T.P.LP.Make.rpo_mul_rest_step [in rpo.rpo]
RPO.T.P.LP.Make.SN_term [in rpo.rpo]
RPO.T.P.LP.rpo [in rpo.rpo]
RPO.T.P.LP.rpo_eq [in rpo.rpo]
RPO.T.P.LP.rpo_lex [in rpo.rpo]
RPO.T.P.LP.rpo_mul [in rpo.rpo]
R1 [in epsilon0.Hydra]
R_union [in denumerable.Denumerable]


S

segment_bound [in hilbert.Enumeration]
Set_Sum [in SCHROEDER.Sums]
Sh [in epsilon0.Hydra]
Signature.arity_type [in rpo.term]
Sn [in epsilon0.Hydra]
sorted [in schutte.CNF]
subterm [in gamma0.Gamma0]
surjection [in SCHROEDER.Functions]
S.DS.Make.t [in prelude.list_set]
S.DS.t [in prelude.list_set]
S1 [in epsilon0.Hydra]
S2 [in epsilon0.Hydra]


T

Term.F.X.term [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term [in rpo.term]
trans_clos [in prelude.closure]
T1 [in epsilon0.EPSILON0]
T2 [in gamma0.Gamma0_prelude]


U

unit [in prelude.bintree]


V

Vars.empty_set [in epsilon0.EPSILON0]
Vars.empty_set [in gamma0.Gamma0]


W

WO [in schutte.Well_Orders]
WO_lt [in schutte.Well_Orders]



Definition Index

A

Acc_iter_partial [in prelude.PartialFix]
app [in epsilon0.MSE0]
au_moins_une_im [in SCHROEDER.Functions]
au_moins_un_ant [in SCHROEDER.Functions]
au_plus_une_im [in SCHROEDER.Functions]
au_plus_un_ant [in SCHROEDER.Functions]


B

bad_two [in hilbert.Epsilon_Examples]


C

choice_fun [in hilbert.Epsilon]
choice_fun [in hilbert.OldEpsilon]
compare [in epsilon0.EPSILON0]
compare [in gamma0.Gamma0]
compose [in prelude.bintree]
compose [in hilbert.Paradoxical]
Cr [in schutte.Critical]
critical [in schutte.Critical]
critical_fun [in schutte.Critical]


D

decompose [in prelude.bintree]
denumerable [in denumerable.Denumerable]
D_a [in schutte.Well_Orders]


E

elagage [in hilbert.more_relations]
elagage_choisi [in hilbert.more_relations]
elaguer_mini [in hilbert.more_relations]
epsilon [in gamma0.Gamma0_prelude]
epsilon [in hilbert.ClassicalEpsilonModified]
EPSILON0 [in gamma0.Gamma0_prelude]
epsilon0 [in gamma0.Gamma0_prelude]
epsilon_extensionality [in hilbert.Epsilon]
epsilon_extensionality [in hilbert.OldEpsilon]
epsilon_spec [in hilbert.ClassicalEpsilonModified]
Eps0_alg.Eps0_rpo.exp [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.exp_F [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.get_decomposition [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.minus [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.mult [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.nat_2_term [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.None [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.plus [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.pred [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.succ [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.transfinite_induction [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.transfinite_induction_Q [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_size [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.T1_2_term [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [in epsilon0.EPSILON0]
Eps0_alg.Eps0_rpo.zero [in epsilon0.EPSILON0]
Eps0_prec.A [in epsilon0.EPSILON0]
Eps0_prec.prec [in epsilon0.EPSILON0]
Eps0_prec.status [in epsilon0.EPSILON0]
Eps0_sig.arity [in epsilon0.EPSILON0]
Eps0_sig.symb [in epsilon0.EPSILON0]
equiv [in epsilon0.MSE0]
eval [in schutte.CNF]
exists_sigT [in hilbert.BadEpsilon2]
exist_1_R_a [in hilbert.PartialFun]
ex_1 [in hilbert.OldEpsilon]


F

f [in misc.G4]
find [in prelude.more_list]
finite [in schutte.Schutte]
finite [in gamma0.Gamma0_prelude]
finite [in epsilon0.EPSILON0]
fold_left2 [in prelude.more_list]
fun_codomain [in hilbert.PartialFun]
fun_eq [in schutte.Ordering_Functions]
fun_eq_gen [in schutte.Ordering_Functions]
fun_inj [in hilbert.PartialFun]
fun_onto [in hilbert.PartialFun]
fun_rel_same [in hilbert.PartialFun]
fun_restrict [in schutte.Ordering_Functions]
f_beta [in schutte.Ordering_Functions]
f_Z [in misc.G4]


G

g [in schutte.Ordering_Functions]
Gamma0_alg.Gamma0_rpo.lt_T1_injection [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.lub [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.moser_lepper [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.nat_2_term [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.phi [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.transfinite_induction [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.transfinite_induction_Q [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_size [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.T2_2_term [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.zero [in gamma0.Gamma0]
Gamma0_alg.Gamma0_rpo.zero [in gamma0.Gamma0]
Gamma0_prec.A [in gamma0.Gamma0]
Gamma0_prec.prec [in gamma0.Gamma0]
Gamma0_prec.status [in gamma0.Gamma0]
Gamma0_sig.arity [in gamma0.Gamma0]
Gamma0_sig.symb [in gamma0.Gamma0]
goodstein_next [in epsilon0.Goodstein]
goodstein_next_ord [in epsilon0.Goodstein]
gpred [in epsilon0.Goodstein]
Greater [in schutte.Plus]
GRelation [in denumerable.GRelations]


H

head [in epsilon0.Hydra]
head [in epsilon0.Hydra]
head_at [in epsilon0.Hydra]
head_at_l [in epsilon0.Hydra]
Hercules_ok [in epsilon0.Hydra]
Hercules_strat [in epsilon0.Hydra]
Hydra_strat [in epsilon0.Hydra]
h2o [in epsilon0.Hydra]
h2ol [in epsilon0.Hydra]


I

image [in hilbert.PartialFun]
inductive [in hilbert.Paradoxical]
Infinite_union [in denumerable.Denumerable]
inhabited [in hilbert.OldEpsilon]
inhabited [in hilbert.BadEpsilon2]
inh_proj [in hilbert.OldEpsilon]
inleft [in epsilon0.EPSILON0]
inv_fun [in hilbert.PartialFun]
in_or_not_in [in SCHROEDER.Schroeder]
iota [in hilbert.Epsilon]
iota [in hilbert.OldEpsilon]
iota_fun [in hilbert.Epsilon]
iota_fun [in hilbert.OldEpsilon]
isotonic [in schutte.Well_Orders]
is_finite [in schutte.Schutte]
is_least_member [in schutte.Well_Orders]
is_limit [in schutte.Schutte]
is_lub [in schutte.Lub]
is_succ [in schutte.Schutte]


K

K [in prelude.bintree]


L

laboureur [in denumerable.Denumerable]
le [in gamma0.Gamma0_prelude]
le [in schutte.Schutte]
le [in epsilon0.EPSILON0]
Le [in schutte.Well_Orders]
Leaf [in prelude.bintree]
length [in gamma0.Gamma0_length]
length_aux [in gamma0.Gamma0_length]
Lerne [in epsilon0.Hydra]
lex [in rpo.rpo]
list_rec2 [in prelude.more_list]
list_rec3 [in prelude.more_list]
list_size [in prelude.more_list]
log [in schutte.AP]
log [in epsilon0.EPSILON0]
lt [in hilbert.Paradoxical]
lt [in schutte.Schutte]
ltM [in epsilon0.MSE0]
Lt_a [in schutte.Well_Orders]
lt_a [in schutte.Well_Orders]
lt_ge_dec [in gamma0.Gamma0]
lt_le_dec [in epsilon0.EPSILON0]


M

map12_without_repetition [in prelude.more_list]
map_without_repetition [in prelude.more_list]
max [in epsilon0.EPSILON0]
max' [in epsilon0.EPSILON0]
members [in schutte.Schutte]
minimal [in prelude.wf_minimal]
minus [in schutte.Minus]
multiplicity [in epsilon0.MSE0]
my_pred [in hilbert.Epsilon_Examples]


N

nat_segment [in hilbert.Enumeration]
nbterms [in gamma0.Gamma0_length]
nb_occ [in prelude.more_list]
next [in misc.G4]
nexts [in misc.G4]
nf_rect [in epsilon0.EPSILON0]
nil [in schutte.CNF]
nth_item [in misc.G4]


O

occurrence [in epsilon0.Hydra]
Omega [in hilbert.Paradoxical]
omega [in gamma0.Gamma0_prelude]
omega [in schutte.Schutte]
omega [in epsilon0.EPSILON0]
omega_limit [in schutte.Schutte]
omega_term [in epsilon0.EPSILON0]
omega_tower [in epsilon0.EPSILON0]
one [in gamma0.Gamma0_prelude]
opt_codomain [in hilbert.PartialFun]
opt_domain [in hilbert.PartialFun]
opt_inj [in hilbert.PartialFun]
opt_onto [in hilbert.PartialFun]
opt_rel_same [in hilbert.PartialFun]
ordering_function [in schutte.Ordering_Functions]
ordering_function_segment [in schutte.Ordering_Functions]
ordering_segment_2_fun [in schutte.Ordering_Functions]
ordinal [in schutte.Schutte]
or_sumbool [in hilbert.BadEpsilon2]
OT [in schutte.Schutte]
o_bounded [in schutte.CNF]
o_bounded_leq [in schutte.CNF]
o_length [in prelude.more_list]
O_segment [in schutte.Ordering_Functions]


P

Paradoxical [in hilbert.Paradoxical]
partial_fun_induction [in prelude.PartialFix]
Permut.DS.elt [in prelude.list_permut]
Permut.DS.eq_elt_dec [in prelude.list_permut]
Permut.DS.list_permut [in prelude.list_permut]
Permut.DS.list_to_multiset [in prelude.list_permut]
Permut.DS.Make.elt [in prelude.list_permut]
Permut.DS.Make.eq_elt_dec [in prelude.list_permut]
Permut.DS.Make.list_permut [in prelude.list_permut]
Permut.DS.Make.list_to_multiset [in prelude.list_permut]
PFix [in prelude.PartialFix]
phi0 [in schutte.AP]
phi0 [in epsilon0.EPSILON0]
plus [in schutte.Plus]
plus [in gamma0.Gamma0]
power [in misc.G4]
power [in prelude.More_nat]
ppred [in hilbert.Epsilon_Examples]
pred [in gamma0.Gamma0_prelude]
Pred [in epsilon0.Goodstein]
PredF [in epsilon0.Goodstein]
pred2 [in hilbert.Epsilon_Examples]
pred_n_zero [in epsilon0.Goodstein]
Pred_omega_a [in epsilon0.Goodstein]
Pred_omega_an [in epsilon0.Goodstein]
Pred_omega_anb [in epsilon0.Goodstein]
pred_spec [in epsilon0.Goodstein]
progressive [in schutte.Schutte]
proper_O_segment [in schutte.Ordering_Functions]
proper_segment_of [in schutte.Ordering_Functions]
Prop_dec [in hilbert.OldEpsilon]
psi [in gamma0.Gamma0_prelude]
psi_term [in gamma0.Gamma0_prelude]
P_well_founded_induction_type [in prelude.AccP]


Q

quo [in hilbert.euclid]
quo' [in hilbert.euclid]


R

reachable [in misc.G4]
rel_codomain [in hilbert.PartialFun]
rel_domain [in hilbert.PartialFun]
rel_enumerates [in denumerable.Denumerable]
rel_functional [in hilbert.PartialFun]
rel_inj [in hilbert.PartialFun]
rel_inv [in hilbert.PartialFun]
rel_isotonic [in schutte.Well_Orders]
rel_mono [in schutte.Well_Orders]
rel_numbers [in denumerable.Denumerable]
rel_onto [in hilbert.PartialFun]
remove [in prelude.more_list]
remove_list [in prelude.more_list]
replicate [in epsilon0.Hydra]
restrict [in prelude.AccP]
restrict [in schutte.Well_Orders]
restricted_epsilon_extensionality [in hilbert.OldEpsilon]
restricted_epsilon_extensionality [in hilbert.Epsilon]
Rgstar [in misc.G4]
RPO.T.P.A [in rpo.rpo]
RPO.T.P.LP.DS [in rpo.rpo]
RPO.T.P.LP.Make.A [in rpo.rpo]
RPO.T.P.LP.Make.build_list_of_SN_terms [in rpo.rpo]
RPO.T.P.LP.Make.o_size [in rpo.rpo]
RPO.T.P.LP.Make.o_size2 [in rpo.rpo]
RPO.T.P.LP.Make.o_size3 [in rpo.rpo]
RPO.T.P.LP.Make.rpo_rest [in rpo.rpo]
RPO.T.P.LP.Make.rpo_term [in rpo.rpo]
RPO.T.P.LP.Make.size2 [in rpo.rpo]
RPO.T.P.LP.Make.size3 [in rpo.rpo]
R1 [in schutte.Ordering_Functions]
r2f [in hilbert.PartialFun]
r2i [in hilbert.PartialFun]
R_inv [in denumerable.GRelations]
R_nat_elaguee [in denumerable.GRelations]
R_union_qcq [in denumerable.Denumerable]


S

seq_mono [in schutte.Schutte]
seq_range [in denumerable.Denumerable]
seq_range [in hilbert.Enumeration]
seq_range_opt [in hilbert.Enumeration]
set_eq [in schutte.Schutte]
shift_n_omega_l [in prelude.bintree]
shift_n_omega_r [in prelude.bintree]
single [in epsilon0.Hydra]
single [in epsilon0.Hydra]
some [in hilbert.Epsilon]
some [in hilbert.OldEpsilon]
Some [in gamma0.Gamma0_prelude]
some_fun [in hilbert.OldEpsilon]
some_fun [in hilbert.Epsilon]
some_lt [in hilbert.Epsilon_Examples]
some_positive [in hilbert.Epsilon_Examples]
sort [in epsilon0.MSE0]
sort_aux [in epsilon0.MSE0]
split_list [in prelude.more_list]
star [in hilbert.Paradoxical]
succ [in gamma0.Gamma0_prelude]
succ [in schutte.Schutte]
succ_spec [in schutte.Schutte]
sup [in schutte.Schutte]
sup_spec [in schutte.Schutte]
S.DS.cardinal [in prelude.list_set]
S.DS.elt [in prelude.list_set]
S.DS.eq_elt_dec [in prelude.list_set]
S.DS.Make.add [in prelude.list_set]
S.DS.Make.add_without_red [in prelude.list_set]
S.DS.Make.cardinal [in prelude.list_set]
S.DS.Make.elt [in prelude.list_set]
S.DS.Make.empty [in prelude.list_set]
S.DS.Make.eq_elt_dec [in prelude.list_set]
S.DS.Make.eq_set [in prelude.list_set]
S.DS.Make.filter [in prelude.list_set]
S.DS.Make.filter_aux [in prelude.list_set]
S.DS.Make.inter [in prelude.list_set]
S.DS.Make.make_set [in prelude.list_set]
S.DS.Make.mem [in prelude.list_set]
S.DS.Make.remove_not_common [in prelude.list_set]
S.DS.Make.remove_red [in prelude.list_set]
S.DS.Make.singleton [in prelude.list_set]
S.DS.Make.subset [in prelude.list_set]
S.DS.Make.union [in prelude.list_set]
S.DS.Make.without_red [in prelude.list_set]
S.DS.subset [in prelude.list_set]
S.DS.without_red [in prelude.list_set]


T

tail [in gamma0.Gamma0_prelude]
tau [in hilbert.Epsilon]
Term.F.X.direct_subterm [in rpo.term]
Term.F.X.size [in rpo.term]
Term.F.X.symbol [in rpo.term]
Term.F.X.Term_eq_dec.A [in rpo.term]
Term.F.X.Term_eq_dec.apply_subst [in rpo.term]
Term.F.X.Term_eq_dec.eq_A_dec [in rpo.term]
Term.F.X.Term_eq_dec.is_a_pos [in rpo.term]
Term.F.X.Term_eq_dec.Make.DecVar.A [in rpo.term]
Term.F.X.Term_eq_dec.Make.symbol [in rpo.term]
Term.F.X.Term_eq_dec.Make.variable [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.apply_subst [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.direct_subterm [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.DS [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.is_a_pos [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.map_subst [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.replace_at_pos_list [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.size [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.substitution [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subst_comp [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.subterm_at_pos [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.A [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.A [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.eq_A_dec [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.Term_eq_dec.eq_A_dec [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec2 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec3 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec4 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec7 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.term_rec8 [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_list [in rpo.term]
Term.F.X.Term_eq_dec.Make.VSet.well_formed_subst [in rpo.term]
Term.F.X.Term_eq_dec.map_subst [in rpo.term]
Term.F.X.Term_eq_dec.replace_at_pos [in rpo.term]
Term.F.X.Term_eq_dec.replace_at_pos_list [in rpo.term]
Term.F.X.Term_eq_dec.substitution [in rpo.term]
Term.F.X.Term_eq_dec.subst_comp [in rpo.term]
Term.F.X.Term_eq_dec.subterm_at_pos [in rpo.term]
Term.F.X.Term_eq_dec.well_formed [in rpo.term]
Term.F.X.Term_eq_dec.well_formed_list [in rpo.term]
Term.F.X.Term_eq_dec.well_formed_subst [in rpo.term]
Term.F.X.variable [in rpo.term]
the [in hilbert.OldEpsilon]
the [in hilbert.Epsilon]
the_fun [in hilbert.OldEpsilon]
the_fun [in hilbert.Epsilon]
the_least [in schutte.Schutte]
the_ordering_function [in schutte.Ordering_Functions]
the_ordering_segment [in schutte.Ordering_Functions]
tree_nat [in prelude.bintree]
trichotomy_inf [in epsilon0.EPSILON0]
trichotomy_inf [in gamma0.Gamma0]
two [in hilbert.Epsilon_Examples]
T1_eq_dec [in epsilon0.EPSILON0]
T1_inj [in gamma0.Gamma0_prelude]


U

Unbounded [in schutte.Schutte]
upper_bound [in schutte.Lub]


V

val [in epsilon0.Goodstein]


W

well_founded [in hilbert.Paradoxical]
well_founded_P [in prelude.AccP]


Z

zero [in gamma0.Gamma0_prelude]
zero [in epsilon0.MSE0]
zero [in gamma0.Gamma0_length]
zero [in epsilon0.EPSILON0]
zero [in hilbert.Epsilon_Examples]
zero [in epsilon0.MSE0]
zero [in gamma0.Gamma0_length]
zero [in gamma0.Gamma0_length]
zero [in schutte.Schutte]
zero [in gamma0.Gamma0_prelude]
zero_spec [in schutte.Schutte]


_

_A [in schutte.Ordering_Functions]



Module Index

D

DecVar [in rpo.term]
DS [in prelude.list_set]
DS [in prelude.list_permut]


E

Eps0_alg [in epsilon0.EPSILON0]
Eps0_prec [in epsilon0.EPSILON0]
Eps0_rpo [in epsilon0.EPSILON0]
Eps0_sig [in epsilon0.EPSILON0]


F

F [in rpo.term]


G

Gamma0_alg [in gamma0.Gamma0]
Gamma0_prec [in gamma0.Gamma0]
Gamma0_rpo [in gamma0.Gamma0]
Gamma0_sig [in gamma0.Gamma0]


L

LP [in rpo.rpo]


M

Make [in prelude.dickson]
Make [in prelude.list_set]
Make [in rpo.rpo]
Make [in rpo.term]
Make [in prelude.list_permut]


P

P [in rpo.rpo]
Permut [in prelude.list_permut]
Precedence [in rpo.rpo]


R

RPO [in rpo.rpo]


S

S [in prelude.list_set]
S [in prelude.decidable_set]
Signature [in rpo.term]


T

T [in rpo.rpo]
Term [in rpo.term]
Term_eq_dec [in rpo.term]
Term_eq_dec [in rpo.term]


V

Variables [in rpo.term]
Vars [in gamma0.Gamma0]
Vars [in epsilon0.EPSILON0]
VSet [in rpo.term]


X

X [in rpo.term]



Library Index

A

AccP
AP
Arith_lemmas


B

BadEpsilon2
bintree


C

ClassicalEpsilonModified
closure
CNF
Critical


D

decidable_set
Denumerable
diag
dickson


E

Enumeration
Epsilon
EPSILON0
Epsilon_Examples
Equipollence
euclid
E0_ARITH


F

Functions


G

Gamma0
Gamma0_length
Gamma0_prelude
Goodstein
GRelations
G4


H

Hydra


L

list_permut
list_set
Lub


M

Minus
more_list
More_nat
more_relations
MSE0


N

not_decreasing


O

OldEpsilon
Ordering_Functions


P

Paradoxical
PartialFix
PartialFun
Plus


R

rpo


S

Schroeder
Schutte
Setminus_fact
Sums


T

term
Tools


W

Well_Orders
wf_minimal



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 _ (1807 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (50 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 _ (1037 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 _ (159 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 _ (94 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 _ (381 entries)
Module 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 _ (34 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (52 entries)

This page has been generated by coqdoc