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
AccPAP
Arith_lemmas
B
BadEpsilon2bintree
C
ClassicalEpsilonModifiedclosure
CNF
Critical
D
decidable_setDenumerable
diag
dickson
E
EnumerationEpsilon
EPSILON0
Epsilon_Examples
Equipollence
euclid
E0_ARITH
F
FunctionsG
Gamma0Gamma0_length
Gamma0_prelude
Goodstein
GRelations
G4
H
HydraL
list_permutlist_set
Lub
M
Minusmore_list
More_nat
more_relations
MSE0
N
not_decreasingO
OldEpsilonOrdering_Functions
P
ParadoxicalPartialFix
PartialFun
Plus
R
rpoS
SchroederSchutte
Setminus_fact
Sums
T
termTools
W
Well_Orderswf_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